condExp_smul — Mathlib

English

Under suitable conditions, μ[f|m] is ae-equal to condExpL1CLM E hm μ (hf.toL1 f).

Русский

При некоторых условиях μ[f|m] почти равен condExpL1CLM E hm μ (hf.toL1 f).

LaTeX

$$$$\\mu[f|m] =_{\\text{ae}} condExpL1CLM E hm μ (hf.toL1 f).$$$$

Lean4

theorem condExp_smul [NormedSpace 𝕜 E] (c : 𝕜) (f : α → E) (m : MeasurableSpace α) : μ[c • f|m] =ᵐ[μ] c • μ[f|m] :=
  by
  by_cases hm : m ≤ m₀
  swap; · simp_rw [condExp_of_not_le hm]; simp
  by_cases hμm : SigmaFinite (μ.trim hm)
  swap; · simp_rw [condExp_of_not_sigmaFinite hm hμm]; simp
  refine (condExp_ae_eq_condExpL1 hm _).trans ?_
  rw [condExpL1_smul c f]
  refine (condExp_ae_eq_condExpL1 hm f).mp ?_
  refine (coeFn_smul c (condExpL1 hm μ f)).mono fun x hx1 hx2 => ?_
  simp only [hx1, hx2, Pi.smul_apply]

Похожие утверждения