English
The integral of condExpL1CLM over s equals the integral of f over s for f in L1(μ).
Русский
Интеграл по s от condExpL1CLM равен интегралу f по s для f ∈ L1(μ).
LaTeX
$$$ \int x in s, condExpL1CLM F' hm μ f x \\partial μ = \int x in s, f x \\partial μ,$$
Lean4
/-- The integral of the conditional expectation `condExpL1CLM` over an `m`-measurable set is equal
to the integral of `f` on that set. See also `setIntegral_condExp`, the similar statement for
`condExp`. -/
theorem setIntegral_condExpL1CLM (f : α →₁[μ] F') (hs : MeasurableSet[m] s) :
∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ :=
by
let S := spanningSets (μ.trim hm)
have hS_meas : ∀ i, MeasurableSet[m] (S i) := measurableSet_spanningSets (μ.trim hm)
have hS_meas0 : ∀ i, MeasurableSet (S i) := fun i => hm _ (hS_meas i)
have hs_eq : s = ⋃ i, S i ∩ s := by
simp_rw [Set.inter_comm]
rw [← Set.inter_iUnion, iUnion_spanningSets (μ.trim hm), Set.inter_univ]
have hS_finite : ∀ i, μ (S i ∩ s) < ∞ :=
by
refine fun i => (measure_mono Set.inter_subset_left).trans_lt ?_
have hS_finite_trim := measure_spanningSets_lt_top (μ.trim hm) i
rwa [trim_measurableSet_eq hm (hS_meas i)] at hS_finite_trim
have h_mono : Monotone fun i => S i ∩ s := by
intro i j hij x
simp_rw [Set.mem_inter_iff]
exact fun h => ⟨monotone_spanningSets (μ.trim hm) hij h.1, h.2⟩
have h_eq_forall : (fun i => ∫ x in S i ∩ s, condExpL1CLM F' hm μ f x ∂μ) = fun i => ∫ x in S i ∩ s, f x ∂μ :=
funext fun i =>
setIntegral_condExpL1CLM_of_measure_ne_top f (@MeasurableSet.inter α m _ _ (hS_meas i) hs) (hS_finite i).ne
have h_right : Tendsto (fun i => ∫ x in S i ∩ s, f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ)) :=
by
have h :=
tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
(L1.integrable_coeFn f).integrableOn
rwa [← hs_eq] at h
have h_left :
Tendsto (fun i => ∫ x in S i ∩ s, condExpL1CLM F' hm μ f x ∂μ) atTop (𝓝 (∫ x in s, condExpL1CLM F' hm μ f x ∂μ)) :=
by
have h :=
tendsto_setIntegral_of_monotone (fun i => (hS_meas0 i).inter (hm s hs)) h_mono
(L1.integrable_coeFn (condExpL1CLM F' hm μ f)).integrableOn
rwa [← hs_eq] at h
rw [h_eq_forall] at h_left
exact tendsto_nhds_unique h_left h_right
