Mathlib.Measure­Theory.Integral

theorem finite_diagonal_square_integral {ι Ω : Type*} [Fintype ι] [DecidableEq ι] [MeasurableSpace Ω] (μ : Measure Ω) (A : ℝ) (f : ι → Ω → ℝ) (c : ι → ℝ) (hi : ∀ a b, Integrable (fun x => f a x * f b x) μ) (ho : ∀ a b, (∫ x, f a x * f b x ∂μ) = if a = b then A else 0) : (∫ x, (∑ a, c a * f a x) ^ 2 ∂μ) = A * ∑ a, c a ^ 2 := by classical have he (x : Ω) : (∑ a, c a * f a x) ^ 2 = ∑ a, ∑ b, (c a * c b) * (f a x * f b x) := by rw [pow_two, Finset.sum_mul] apply Finset.sum_congr rfl intro a _ rw [Finset.mul_sum] apply Finset.sum_congr rfl intro b _ ring simp_rw [he] rw [integral_finsetSum _ (fun a _ => integrable_finsetSum _ (fun b _ => (hi a b).const_mul _))] simp_rw [integral_finsetSum _ (fun b _ => (hi _ b).const_mul _), integral_const_mul, ho] simp only [mul_ite, mul_zero, Finset.sum_ite_eq, Finset.mem_univ, ↓reduceIte] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro a _ ring

theorem finite_orthogonal_sum_integral_sq {ι Ω : Type*} [DecidableEq ι] [MeasurableSpace Ω] (μ : Measure Ω) (s : Finset ι) (u : ι → Ω → ℝ) (e : ι → ℝ) (hi : ∀ i ∈ s, ∀ j ∈ s, Integrable (fun x => u i x * u j x) μ) (ho : ∀ i ∈ s, ∀ j ∈ s, (∫ x, u i x * u j x ∂μ) = if i = j then e i else 0) : (∫ x, (∑ i ∈ s, u i x) ^ 2 ∂μ) = ∑ i ∈ s, e i := by simp_rw [sq, Finset.sum_mul, Finset.mul_sum] rw [integral_finsetSum s (fun i hi' => integrable_finsetSum _ (fun j hj => hi i hi' j hj))] apply Finset.sum_congr rfl intro i hi' rw [integral_finsetSum s (fun j hj => hi i hi' j hj)] rw [Finset.sum_congr rfl (fun j hj => ho i hi' j hj)] simp [hi']

theorem finite_orthonormal_pythagoras {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] (μ : Measure Ω) (b : ι → Ω → ℝ) (hb : ∀ i, MemLp (b i) 2 μ) (hortho : ∀ i j, (∫ x, b i x * b j x ∂μ) = if i = j then 1 else 0) (f : Ω → ℝ) (hf : MemLp f 2 μ) : let g := fun x => ∑ i, b i x * (∫ y, b i y * f y ∂μ) (∫ x, f x^2 ∂μ) = (∫ x, g x^2 ∂μ) + (∫ x, (f x-g x)^2 ∂μ) := by classical let c := fun i => ∫ y, b i y * f y ∂μ let g := fun x => ∑ i, b i x * c i change (∫ x, f x^2 ∂μ) = (∫ x, g x^2 ∂μ) + (∫ x, (f x-g x)^2 ∂μ) have hg : MemLp g 2 μ := memLp_finsetSum _ (fun i _ => (hb i).mul_const (c i)) have hgb (j : ι) : (∫ x, g x * b j x ∂μ) = c j := by simp only [g, Finset.sum_mul] simp_rw [show ∀ i x, b i x * c i * b j x = (b i x * b j x) * c i by intros; ring] rw [integral_finsetSum (f := fun i x => (b i x * b j x) * c i) univ (fun i _ => ((hb i).integrable_mul (hb j)).mul_const (c i))] simp_rw [integral_mul_const, hortho] simp have hfg : (∫ x, f x * g x ∂μ) = ∑ i, c i^2 := by simp only [g, Finset.mul_sum] simp_rw [show ∀ i x, f x * (b i x * c i) = (b i x * f x) * c i by intros; ring] rw [integral_finsetSum (f := fun i x => (b i x * f x) * c i) univ (fun i _ => ((hb i).integrable_mul hf).mul_const (c i))] simp_rw [integral_mul_const] change (∑ i, c i * c i) = ∑ i, c i^2 simp only [pow_two] have hgg : (∫ x, g x^2 ∂μ) = ∑ i, c i^2 := by simp_rw [pow_two] conv_lhs => arg 2; ext x; rhs; change ∑ i, b i x * c i simp_rw [Finset.mul_sum] simp_rw [show ∀ i x, g x * (b i x * c i) = (g x * b i x) * c i by intros; ring] rw [integral_finsetSum (f := fun i x => (g x * b i x) * c i) univ (fun i _ => (hg.integrable_mul (hb i)).mul_const (c i))] simp_rw [integral_mul_const, hgb] have hres : (∫ x, (f x-g x)^2 ∂μ) = (∫ x, f x^2 ∂μ) - 2*(∫ x, f x*g x ∂μ) + (∫ x, g x^2 ∂μ) := by simp_rw [show ∀ x, (f x-g x)^2 = f x^2 - 2*(f x*g x) + g x^2 by intro x; ring] have hprod : Integrable (fun x => f x*g x) μ := hf.integrable_mul hg have hsub : Integrable (fun x => f x^2 - 2*(f x*g x)) μ := hf.integrable_sq.sub (hprod.const_mul 2) rw [integral_add hsub hg.integrable_sq, integral_sub hf.integrable_sq (hprod.const_mul 2), integral_const_mul] rw [hres, hfg, hgg] ring

theorem subset_product_integral_orthogonality {ι : Type*} [Fintype ι] [DecidableEq ι] {Ω : ι → Type*} [∀ i, MeasurableSpace (Ω i)] (μ : ∀ i, Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] (w : ∀ i, Ω i → ℝ) (hzero : ∀ i, ∫ x, w i x ∂μ i = 0) (γ : ι → ℝ) (hsecond : ∀ i, ∫ x, w i x ^ 2 ∂μ i = γ i) (S T : Finset ι) : (∫ x : ∀ i, Ω i, (∏ i ∈ S, w i (x i)) * (∏ i ∈ T, w i (x i)) ∂Measure.pi μ) = if S = T then ∏ i ∈ S, γ i else 0 := by have hprod (x : ∀ i, Ω i) : (∏ i ∈ S, w i (x i)) * (∏ i ∈ T, w i (x i)) = ∏ i : ι, (if i ∈ S then w i (x i) else 1) * (if i ∈ T then w i (x i) else 1) := by rw [Finset.prod_mul_distrib, Finset.prod_ite_mem_eq, Finset.prod_ite_mem_eq] simp_rw [hprod] rw [integral_fintype_prod_eq_prod (fun i x => (if i ∈ S then w i x else 1) * (if i ∈ T then w i x else 1))] by_cases hST : S = T · subst T rw [if_pos rfl] have hfactor (i : ι) : (∫ x, (if i ∈ S then w i x else 1) * (if i ∈ S then w i x else 1) ∂μ i) = if i ∈ S then γ i else 1 := by by_cases hi : i ∈ S · simp only [hi, ↓reduceIte, ← sq] exact hsecond i · simp [hi] simp_rw [hfactor] rw [Finset.prod_ite_mem_eq] · rw [if_neg hST] obtain ⟨i, hi⟩ : ∃ i, ¬ (i ∈ S ↔ i ∈ T) := by by_contra h apply hST ext i exact not_not.mp (not_exists.mp h i) apply Finset.prod_eq_zero (Finset.mem_univ i) by_cases hS : i ∈ S <;> by_cases hT : i ∈ T · exact False.elim (hi (by simp [hS, hT])) · simpa only [hS, hT, ↓reduceIte, mul_one] using hzero i · simpa only [hS, hT, ↓reduceIte, one_mul] using hzero i · exact False.elim (hi (by simp [hS, hT]))

lemma setIntegral_eq_setIntegral_mul_of_likelihoodRatio_swap {Ω : Type*} {m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ) {μ : Measure Ω} [IsFiniteMeasure μ] (s t : Set Ω) (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t) {L f : Ω → ℝ} (hprod_m : AEStronglyMeasurable[m] (fun ω => f ω * L ω) μ) (hf_m : AEStronglyMeasurable[m] f μ) (hint : IntegrableOn f t μ) (hint' : IntegrableOn (fun ω => f ω * L ω) s μ) (hSpec : (fun ω => (μ[indicator s (fun _ => (1 : ℝ)) | m]) ω * L ω) =ᵐ[μ] (μ[indicator t (fun _ => (1 : ℝ)) | m])) : ∫ ω in t, f ω ∂μ = ∫ ω in s, f ω * L ω ∂μ := by -- Set up the indicator notations (as functions, not via `set`, to avoid -- definitional unfolding issues with `condExp_mul_of_aestronglyMeasurable_left`). let Ia : Ω → ℝ := indicator s (fun _ => (1 : ℝ)) let Ia' : Ω → ℝ := indicator t (fun _ => (1 : ℝ)) have hIa_meas : Measurable Ia := by fun_prop have hIa'_meas : Measurable Ia' := by fun_prop have hIa_le : ∀ ω, ‖Ia ω‖ ≤ 1 := by intro ω; by_cases h : ω ∈ s · simp [Ia, Set.indicator_of_mem h] · simp [Ia, Set.indicator_of_notMem h] have hIa'_le : ∀ ω, ‖Ia' ω‖ ≤ 1 := by intro ω; by_cases h : ω ∈ t · simp [Ia', Set.indicator_of_mem h] · simp [Ia', Set.indicator_of_notMem h] -- σ-finiteness of the trim, needed for `integral_condExp`. have : IsFiniteMeasure (μ.trim hm) := isFiniteMeasure_trim hm have : SigmaFinite (μ.trim hm) := inferInstance -- Integrability of indicators (against μ). have hIa_int : Integrable Ia μ := by refine (integrable_const (1 : ℝ)).mono' hIa_meas.aestronglyMeasurable ?_ exact Filter.Eventually.of_forall (by intro ω; simpa using hIa_le ω) have hIa'_int : Integrable Ia' μ := by refine (integrable_const (1 : ℝ)).mono' hIa'_meas.aestronglyMeasurable ?_ exact Filter.Eventually.of_forall (by intro ω; simpa using hIa'_le ω) -- Step A: `∫ₜ f dμ = ∫ f · Ia' dμ`. have hStepA : ∫ ω in t, f ω ∂μ = ∫ ω, f ω * Ia' ω ∂μ := by rw [← integral_indicator (μ := μ) ht_meas] refine integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω; by_cases h : ω ∈ t · simp [Ia', Set.indicator_of_mem h] · simp [Ia', Set.indicator_of_notMem h] -- Step B (symmetric): `∫ₛ f · L dμ = ∫ (f · L) · Ia dμ`. have hStepB : ∫ ω in s, f ω * L ω ∂μ = ∫ ω, (f ω * L ω) * Ia ω ∂μ := by rw [← integral_indicator (μ := μ) hs_meas] refine integral_congr_ae (Filter.Eventually.of_forall ?_) intro ω; by_cases h : ω ∈ s · simp [Ia, Set.indicator_of_mem h] · simp [Ia, Set.indicator_of_notMem h] -- Integrability of pointwise products (f * Ia') and ((f*L) * Ia). -- These equal the indicator-times-f and indicator-times-(f·L) functions, so -- IntegrableOn-on-t (resp. s) gives global integrability. have hint_f_Ia' : Integrable (fun ω => f ω * Ia' ω) μ := by have h_eq : (fun ω => f ω * Ia' ω) = t.indicator f := by funext ω by_cases h : ω ∈ t · simp [Ia', Set.indicator_of_mem h] · simp [Ia', Set.indicator_of_notMem h] rw [h_eq] exact hint.integrable_indicator ht_meas have hint_fL_Ia : Integrable (fun ω => (f ω * L ω) * Ia ω) μ := by have h_eq : (fun ω => (f ω * L ω) * Ia ω) = s.indicator (fun ω => f ω * L ω) := by funext ω by_cases h : ω ∈ s · simp [Ia, Set.indicator_of_mem h] · simp [Ia, Set.indicator_of_notMem h] rw [h_eq] exact hint'.integrable_indicator hs_meas -- Pull-out: `μ[f * Ia' | m] =ᵐ f · μ[Ia' | m]`. have hpull' : (μ[fun ω => f ω * Ia' ω | m]) =ᵐ[μ] (fun ω => f ω * (μ[Ia' | m]) ω) := by have h := condExp_mul_of_aestronglyMeasurable_left (μ := μ) (m := m) (f := f) (g := Ia') hf_m hint_f_Ia' hIa'_int -- h : μ[f * Ia' | m] =ᵐ f * μ[Ia' | m] (Pi product) exact h -- Pull-out: `μ[(f*L) * Ia | m] =ᵐ (f·L) · μ[Ia | m]`. have hpull : (μ[fun ω => (f ω * L ω) * Ia ω | m]) =ᵐ[μ] (fun ω => (f ω * L ω) * (μ[Ia | m]) ω) := by have h := condExp_mul_of_aestronglyMeasurable_left (μ := μ) (m := m) (f := fun ω => f ω * L ω) (g := Ia) hprod_m hint_fL_Ia hIa_int exact h -- Compute LHS: lift indicator integral, then condExp tower, then pull-out. have hLHS : ∫ ω in t, f ω ∂μ = ∫ ω, f ω * (μ[Ia' | m]) ω ∂μ := by rw [hStepA, ← integral_condExp hm (f := fun ω => f ω * Ia' ω)] exact integral_congr_ae hpull' -- Compute RHS. have hRHS : ∫ ω in s, f ω * L ω ∂μ = ∫ ω, (f ω * L ω) * (μ[Ia | m]) ω ∂μ := by rw [hStepB, ← integral_condExp hm (f := fun ω => (f ω * L ω) * Ia ω)] exact integral_congr_ae hpull -- Identify the two integrands via `hSpec`. rw [hLHS, hRHS] refine integral_congr_ae ?_ filter_upwards [hSpec] with ω hω -- hω : (μ[Ia | m]) ω * L ω = (μ[Ia' | m]) ω -- Goal: f ω * (μ[Ia' | m]) ω = (f ω * L ω) * (μ[Ia | m]) ω rw [← hω]; ring

lemma continuous_setIntegral_of_continuous_uniformOn {X Y E : Type*} [TopologicalSpace X] [MeasurableSpace Y] [NormedAddCommGroup E] [NormedSpace ℝ E] (mu : Measure Y) (K : Set Y) (hmu : mu K < ⊤) (F : X → Y → E) (hF : Continuous (fun x ↦ ofFun {K} (F x))) (hInt : ∀ x, IntegrableOn (F x) K mu) : Continuous (fun x ↦ ∫ y in K, F x y ∂mu) := by rw [continuous_iff_continuousAt] intro x rw [ContinuousAt, Metric.tendsto_nhds] intro epsilon hepsilon let delta := epsilon / (mu.real K + 1) have hdelta : 0 < delta := div_pos hepsilon (by positivity) have hgen : {g : UniformOnFun Y E {K} | ∀ y ∈ K, dist (UniformOnFun.toFun {K} (ofFun {K} (F x)) y) (UniformOnFun.toFun {K} g y) < delta} ∈ nhds (ofFun {K} (F x)) := by apply UniformOnFun.gen_mem_nhds E {K} (ofFun {K} (F x)) (s := K) (V := {p : E × E | dist p.1 p.2 < delta}) (by simp) exact Metric.uniformity_basis_dist.mem_iff.mpr ⟨delta, hdelta, by simp⟩ have hev := hF.continuousAt hgen filter_upwards [hev] with z hz rw [dist_eq_norm, ← integral_sub (hInt z) (hInt x)] calc ‖∫ y in K, F z y - F x y ∂mu‖ ≤ delta * mu.real K := norm_setIntegral_le_of_norm_le_const hmu fun y hy ↦ by exact (show ‖F z y - F x y‖ < delta by simpa only [UniformOnFun.toFun_ofFun, dist_eq_norm, norm_sub_rev] using hz y hy).le _ < epsilon := by dsimp [delta] have hm : 0 ≤ mu.real K := measureReal_nonneg calc epsilon / (mu.real K + 1) * mu.real K < epsilon / (mu.real K + 1) * (mu.real K + 1) := mul_lt_mul_of_pos_left (lt_add_of_pos_right _ zero_lt_one) (div_pos hepsilon (by positivity)) _ = epsilon := by field_simp