condExp_stronglyMeasurable_mul_of_bound

English

If f is strongly measurable and bounded by c almost everywhere, then CondExp of f · g equals f times CondExp of g, a.e.

Русский

Если f сильно измеримо и ограничено на almost everywhere величиной c, тогда CondExp(f·g) = f·CondExp(g) почти всюду.

LaTeX

$$$$ \\mu[ f\\cdot g|m ] =_{a.e.} f \\cdot \\mu[g|m], $$$$

Lean4

theorem condExp_stronglyMeasurable_mul_of_bound (hm : m ≤ m0) [IsFiniteMeasure μ] {f g : α → ℝ}
    (hf : StronglyMeasurable[m] f) (hg : Integrable g μ) (c : ℝ) (hf_bound : ∀ᵐ x ∂μ, ‖f x‖ ≤ c) :
    μ[f * g|m] =ᵐ[μ] f * μ[g|m] := by
  let fs := hf.approxBounded c
  have hfs_tendsto : ∀ᵐ x ∂μ, Tendsto (fs · x) atTop (𝓝 (f x)) := hf.tendsto_approxBounded_ae hf_bound
  by_cases hμ : μ = 0
  · simp only [hμ, ae_zero]; norm_cast
  have : (ae μ).NeBot := ae_neBot.2 hμ
  have hc : 0 ≤ c := by
    rcases hf_bound.exists with ⟨_x, hx⟩
    exact (norm_nonneg _).trans hx
  have hfs_bound : ∀ n x, ‖fs n x‖ ≤ c := hf.norm_approxBounded_le hc
  have : μ[f * μ[g|m]|m] = f * μ[g|m] :=
    by
    refine condExp_of_stronglyMeasurable hm (hf.mul stronglyMeasurable_condExp) ?_
    exact integrable_condExp.bdd_mul' (hf.mono hm).aestronglyMeasurable hf_bound
  rw [← this]
  refine
    tendsto_condExp_unique (fun n x => fs n x * g x) (fun n x => fs n x * (μ[g|m]) x) (f * g) (f * μ[g|m]) ?_ ?_ ?_ ?_
      (c * ‖g ·‖) ?_ (c * ‖(μ[g|m]) ·‖) ?_ ?_ ?_ ?_
  ·
    exact fun n =>
      hg.bdd_mul' ((SimpleFunc.stronglyMeasurable (fs n)).mono hm).aestronglyMeasurable
        (Eventually.of_forall (hfs_bound n))
  ·
    exact fun n =>
      integrable_condExp.bdd_mul' ((SimpleFunc.stronglyMeasurable (fs n)).mono hm).aestronglyMeasurable
        (Eventually.of_forall (hfs_bound n))
  · filter_upwards [hfs_tendsto] with x hx
    exact hx.mul tendsto_const_nhds
  · filter_upwards [hfs_tendsto] with x hx
    exact hx.mul tendsto_const_nhds
  · exact hg.norm.const_mul c
  · fun_prop
  · refine fun n => Eventually.of_forall fun x => ?_
    exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right (hfs_bound n x) (norm_nonneg _))
  · refine fun n => Eventually.of_forall fun x => ?_
    exact (norm_mul_le _ _).trans (mul_le_mul_of_nonneg_right (hfs_bound n x) (norm_nonneg _))
  · intro n
    simp_rw [← Pi.mul_apply]
    refine (condExp_stronglyMeasurable_simpleFunc_mul hm _ hg).trans ?_
    rw [condExp_of_stronglyMeasurable hm ((SimpleFunc.stronglyMeasurable _).mul stronglyMeasurable_condExp) _]
    exact
      integrable_condExp.bdd_mul' ((SimpleFunc.stronglyMeasurable (fs n)).mono hm).aestronglyMeasurable
        (Eventually.of_forall (hfs_bound n))

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