English
For f ∈ L1 and measurable s with μ(s) finite, the integral over s of condExpL1CLM f equals the integral over s of f.
Русский
Для f ∈ L1 и измеримого s с μ(s) конечной, интеграл condExpL1CLM f по s равен интегралу f по s.
LaTeX
$$$ \int x in s, condExpL1CLM F' hm μ f x \partial μ = \int x in s, f x \partial μ,$$
Lean4
/-- Auxiliary lemma used in the proof of `setIntegral_condExpL1CLM`. -/
theorem setIntegral_condExpL1CLM_of_measure_ne_top (f : α →₁[μ] F') (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) :
∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ :=
by
refine
@Lp.induction _ _ _ _ _ _ _ ENNReal.one_ne_top
(fun f : α →₁[μ] F' => ∫ x in s, condExpL1CLM F' hm μ f x ∂μ = ∫ x in s, f x ∂μ) ?_ ?_ (isClosed_eq ?_ ?_) f
· intro x t ht hμt
simp_rw [condExpL1CLM_indicatorConst ht hμt.ne x]
rw [Lp.simpleFunc.coe_indicatorConst, setIntegral_indicatorConstLp (hm _ hs)]
exact setIntegral_condExpInd hs ht hμs hμt.ne x
· intro f g hf_Lp hg_Lp _ hf hg
simp_rw [(condExpL1CLM F' hm μ).map_add]
rw [setIntegral_congr_ae (hm s hs)
((Lp.coeFn_add (condExpL1CLM F' hm μ (hf_Lp.toLp f)) (condExpL1CLM F' hm μ (hg_Lp.toLp g))).mono fun x hx _ =>
hx)]
rw [setIntegral_congr_ae (hm s hs) ((Lp.coeFn_add (hf_Lp.toLp f) (hg_Lp.toLp g)).mono fun x hx _ => hx)]
simp_rw [Pi.add_apply]
rw [integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn,
integral_add (L1.integrable_coeFn _).integrableOn (L1.integrable_coeFn _).integrableOn, hf, hg]
· exact (continuous_setIntegral s).comp (condExpL1CLM F' hm μ).continuous
· exact continuous_setIntegral s
