condExpL2_const_inner — Mathlib

English

Let f be a function in an Lp space with values in E, and let c be a fixed vector in E. Then the conditional expectation of the inner product with c commutes with taking the inner product after applying the conditional expectation; i.e., almost everywhere, condExpL2 𝕜 𝕜 hm of the constant-inner f equals the inner product of c with the conditional expectation of f.

Русский

Пусть f — функция, принадлежащая пространству Lp, значения которой лежат в E, и пусть c фиксирован в E. Тогда условное ожидание произведения по скалярному произведению с c коммутирует с взятием скалярного произведения после условного ожидания; т.е. почти всюду выполняется тождество condExpL2 𝕜 𝕜 hm от константного по внутреннему произведению f и c равно ⟨c, condExpL2 E 𝕜 hm f⟩.

LaTeX

$$$\operatorname{condExpL2} 𝕜 𝕜 hm \Big(((Lp.memLp f).const_inner c).toLp (\lambda a, ⟪c, f(a)⟫)\Big) =^{μ}_{a.e.} \lambda a, ⟪c, (\operatorname{condExpL2} E 𝕜 hm f : α \to E) a ⟫$$$

Lean4

/-- `condExpL2` commutes with taking inner products with constants. See the lemma
`condExpL2_comp_continuousLinearMap` for a more general result about commuting with continuous
linear maps. -/
theorem condExpL2_const_inner (hm : m ≤ m0) (f : Lp E 2 μ) (c : E) :
    condExpL2 𝕜 𝕜 hm (((Lp.memLp f).const_inner c).toLp fun a => ⟪c, f a⟫) =ᵐ[μ] fun a =>
      ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫ :=
  by
  have h_mem_Lp : MemLp (fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫) 2 μ := by refine MemLp.const_inner _ ?_;
    exact Lp.memLp _
  have h_eq : h_mem_Lp.toLp _ =ᵐ[μ] fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫ := h_mem_Lp.coeFn_toLp
  refine EventuallyEq.trans ?_ h_eq
  refine
    Lp.ae_eq_of_forall_setIntegral_eq' 𝕜 hm _ _ two_ne_zero ENNReal.coe_ne_top
      (fun s _ hμs => integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _) ?_ ?_ ?_ ?_
  · intro s _ hμs
    rw [IntegrableOn, integrable_congr (ae_restrict_of_ae h_eq)]
    exact (integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _).const_inner _
  · intro s hs hμs
    rw [integral_condExpL2_eq_of_fin_meas_real _ hs hμs.ne, integral_congr_ae (ae_restrict_of_ae h_eq), ←
      L2.inner_indicatorConstLp_eq_setIntegral_inner 𝕜 (↑(condExpL2 E 𝕜 hm f)) (hm s hs) c hμs.ne, ←
      inner_condExpL2_left_eq_right, condExpL2_indicator_of_measurable _ hs,
      L2.inner_indicatorConstLp_eq_setIntegral_inner 𝕜 f (hm s hs) c hμs.ne,
      setIntegral_congr_ae (hm s hs) ((MemLp.coeFn_toLp ((Lp.memLp f).const_inner c)).mono fun x hx _ => hx)]
  · exact lpMeas.aestronglyMeasurable _
  · refine AEStronglyMeasurable.congr ?_ h_eq.symm
    exact (lpMeas.aestronglyMeasurable _).const_inner

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