chore(Probability): shorten proof of condExp_indep_eq (leanprover-community#37731)

This PR golfs three proofs by replacing bespoke local calculations with existing lemmas and `simp`.

* In `Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean`, simplify the `ℝ ≃L[ℝ] ℝ¹` bookkeeping in `integral_eq_of_hasDerivAt_off_countable_of_le` and replace two local `rfl` helpers with `simp [F', e]`.
* In `Mathlib/Probability/ConditionalExpectation.lean`, replace two hand-written `funext` equalities with direct continuity statements obtained by composing `continuous_integral` and `continuous_setIntegral` with `Submodule.subtypeL`.
* In `Mathlib/MeasureTheory/Integral/MeanInequalities.lean`, replace a manual proof of the pointwise bound used in `lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top` with the existing lemma `ENNReal.rpow_add_le_mul_rpow_add_rpow`.

All changes are proof golfing only; theorem statements are unchanged.

No theorem statements are changed.

Author: yuanyi-350

Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

@@ -376,9 +376,7 @@ theorem integral_eq_of_hasDerivAt_off_countable_of_le [CompleteSpace E] (f f' :
     (Hd : ∀ x ∈ Ioo a b \ s, HasDerivAt f (f' x) x) (Hi : IntervalIntegrable f' volume a b) :
     ∫ x in a..b, f' x = f b - f a := by
   set e : ℝ ≃L[ℝ] ℝ¹ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm
-  have e_symm : ∀ x, e.symm x = x 0 := fun x => rfl
   set F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight (1 : ℝ →L[ℝ] ℝ) (f' x)
-  have hF' : ∀ x y, F' x y = y • f' x := fun x y => rfl
   calc
     ∫ x in a..b, f' x = ∫ x in Icc a b, f' x := by
       rw [intervalIntegral.integral_of_le hle, setIntegral_congr_set Ioc_ae_eq_Icc]
@@ -393,7 +391,7 @@ theorem integral_eq_of_hasDerivAt_off_countable_of_le [CompleteSpace E] (f f' :
           (fun _ => F') s hs a b hle (fun _ => Hc) (fun x hx _ => Hd x hx) _ ?_ ?_
       · exact fun x y => (OrderIso.funUnique (Fin 1) ℝ).symm.le_iff_le
       · exact (volume_preserving_funUnique (Fin 1) ℝ).symm _
-      · intro x; rw [Fin.sum_univ_one, hF', e_symm, Pi.single_eq_same, one_smul]
+      · simp [F', e]
       · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi
         exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm
     _ = f b - f a := by

Mathlib/MeasureTheory/Integral/MeanInequalities.lean

@@ -263,29 +263,11 @@ theorem lintegral_mul_prod_norm_pow_le {α ι : Type*} [MeasurableSpace α] {μ
 theorem lintegral_rpow_add_lt_top_of_lintegral_rpow_lt_top {p : ℝ} {f g : α → ℝ≥0∞}
     (hf : AEMeasurable f μ) (hf_top : (∫⁻ a, f a ^ p ∂μ) < ⊤) (hg_top : (∫⁻ a, g a ^ p ∂μ) < ⊤)
     (hp1 : 1 ≤ p) : (∫⁻ a, (f + g) a ^ p ∂μ) < ⊤ := by
-  have hp0_lt : 0 < p := lt_of_lt_of_le zero_lt_one hp1
-  have hp0 : 0 ≤ p := le_of_lt hp0_lt
   calc
     (∫⁻ a : α, (f a + g a) ^ p ∂μ) ≤
         ∫⁻ a, (2 : ℝ≥0∞) ^ (p - 1) * f a ^ p + (2 : ℝ≥0∞) ^ (p - 1) * g a ^ p ∂μ := by
       refine lintegral_mono fun a => ?_
-      dsimp only
-      have h_zero_lt_half_rpow : (0 : ℝ≥0∞) < (1 / 2 : ℝ≥0∞) ^ p := by
-        rw [← ENNReal.zero_rpow_of_pos hp0_lt]
-        exact ENNReal.rpow_lt_rpow (by simp) hp0_lt
-      have h_rw : (1 / 2 : ℝ≥0∞) ^ p * (2 : ℝ≥0∞) ^ (p - 1) = 1 / 2 := by
-        rw [sub_eq_add_neg, ENNReal.rpow_add _ _ two_ne_zero ENNReal.coe_ne_top, ← mul_assoc, ←
-          ENNReal.mul_rpow_of_nonneg _ _ hp0, one_div,
-          ENNReal.inv_mul_cancel two_ne_zero ENNReal.coe_ne_top, ENNReal.one_rpow, one_mul,
-          ENNReal.rpow_neg_one]
-      rw [← ENNReal.mul_le_mul_iff_right h_zero_lt_half_rpow.ne']
-      · rw [mul_add, ← mul_assoc, ← mul_assoc, h_rw, ← ENNReal.mul_rpow_of_nonneg _ _ hp0, mul_add]
-        refine
-          ENNReal.rpow_arith_mean_le_arith_mean2_rpow (1 / 2 : ℝ≥0∞) (1 / 2 : ℝ≥0∞) (f a) (g a) ?_
-            hp1
-        rw [ENNReal.div_add_div_same, one_add_one_eq_two,
-          ENNReal.div_self two_ne_zero ENNReal.coe_ne_top]
-      · finiteness
+      simpa [mul_add] using ENNReal.rpow_add_le_mul_rpow_add_rpow (f a) (g a) hp1
     _ < ⊤ := by
       rw [lintegral_add_left', lintegral_const_mul'' _ (hf.pow_const p),
         lintegral_const_mul' _ _ (by finiteness), ENNReal.add_lt_top]

Mathlib/Probability/ConditionalExpectation.lean

@@ -60,20 +60,12 @@ theorem condExp_indep_eq (hle₁ : m₁ ≤ m) (hle₂ : m₂ ≤ m) [SigmaFinit
     rw [memLp_one_iff_integrable] at huint hvint
     rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq,
       integral_add' huint.integrableOn hvint.integrableOn]
-  · have heq₁ : (fun f : lpMeas E ℝ m₁ 1 μ => ∫ x, (f : Ω → E) x ∂μ) =
-        (fun f : Lp E 1 μ => ∫ x, f x ∂μ) ∘ Submodule.subtypeL _ := by
-      refine funext fun f => integral_congr_ae ?_
-      simp_rw [Submodule.coe_subtypeL', Submodule.coe_subtype]; norm_cast
-    have heq₂ : (fun f : lpMeas E ℝ m₁ 1 μ => ∫ x in s, (f : Ω → E) x ∂μ) =
-        (fun f : Lp E 1 μ => ∫ x in s, f x ∂μ) ∘ Submodule.subtypeL _ := by
-      refine funext fun f => integral_congr_ae (ae_restrict_of_ae ?_)
-      simp_rw [Submodule.coe_subtypeL', Submodule.coe_subtype]
-      exact Eventually.of_forall fun _ => (by trivial)
-    refine isClosed_eq (Continuous.const_smul ?_ _) ?_
-    · rw [heq₁]
-      exact continuous_integral.comp (ContinuousLinearMap.continuous _)
-    · rw [heq₂]
-      exact (continuous_setIntegral _).comp (ContinuousLinearMap.continuous _)
+  · have h_integral : Continuous fun f : lpMeas E ℝ m₁ 1 μ => ∫ x, (f : Ω → E) x ∂μ := by
+      simpa using continuous_integral.comp (ContinuousLinearMap.continuous (Submodule.subtypeL _))
+    have h_setIntegral : Continuous fun f : lpMeas E ℝ m₁ 1 μ => ∫ x in s, (f : Ω → E) x ∂μ := by
+      simpa using (continuous_setIntegral s).comp
+        (ContinuousLinearMap.continuous (Submodule.subtypeL _))
+    exact isClosed_eq (Continuous.const_smul h_integral _) h_setIntegral
   · intro u v huv _ hueq
     rwa [← integral_congr_ae huv, ←
       (setIntegral_congr_ae (hle₂ _ hms) _ : ∫ x in s, u x ∂μ = ∫ x in s, v x ∂μ)]