English
Same as previous, in simp form for negation of X.
Русский
То же для упрощённой формы при отрицании X.
LaTeX
$$@[simp] Var[-X; μ | m] =^a.e_μ Var[X; μ | m]$$
Lean4
/-- If `m₁, m₂` are independent σ-algebras and `f` is `m₁`-measurable, then `𝔼[f | m₂] = 𝔼[f]`
almost everywhere. -/
theorem condExp_indep_eq (hle₁ : m₁ ≤ m) (hle₂ : m₂ ≤ m) [SigmaFinite (μ.trim hle₂)] (hf : StronglyMeasurable[m₁] f)
(hindp : Indep m₁ m₂ μ) : μ[f|m₂] =ᵐ[μ] fun _ => μ[f] :=
by
by_cases hfint : Integrable f μ
swap; · rw [condExp_of_not_integrable hfint, integral_undef hfint]; rfl
refine
(ae_eq_condExp_of_forall_setIntegral_eq hle₂ hfint (fun s _ hs ↦ integrableOn_const hs.ne) (fun s hms hs => ?_)
stronglyMeasurable_const.aestronglyMeasurable).symm
rw [setIntegral_const]
rw [← memLp_one_iff_integrable] at hfint
refine MemLp.induction_stronglyMeasurable hle₁ ENNReal.one_ne_top _ ?_ ?_ ?_ ?_ hfint ?_
· exact ⟨f, hf, EventuallyEq.rfl⟩
· intro c t hmt _
rw [Indep_iff] at hindp
rw [integral_indicator (hle₁ _ hmt), setIntegral_const, smul_smul, measureReal_def, measureReal_def, ←
ENNReal.toReal_mul, mul_comm, ← hindp _ _ hmt hms, setIntegral_indicator (hle₁ _ hmt), setIntegral_const,
Set.inter_comm, measureReal_def]
· intro u v _ huint hvint hu hv hu_eq hv_eq
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 _)
· 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 ∂μ)]
filter_upwards [huv] with x hx _ using hx
