condExpL2_indicator_eq_toSpanSingleton_comp

English

A repeated formulation showing ae-equivalence of condExpL2 with indicator-smul representations.

Русский

Повторная формулировка ae-эквивалентности condExpL2 с индикатором и умножением.

LaTeX

$$condExpL2_indicator_ae_eq_smul (hm) (hs) (hμs) (x)$$

Lean4

theorem condExpL2_indicator_eq_toSpanSingleton_comp (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E') :
    (condExpL2 E' 𝕜 hm (indicatorConstLp 2 hs hμs x) : α →₂[μ] E') =
      (toSpanSingleton ℝ x).compLp (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1)) :=
  by
  ext1
  refine (condExpL2_indicator_ae_eq_smul 𝕜 hm hs hμs x).trans ?_
  have h_comp := (toSpanSingleton ℝ x).coeFn_compLp (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α →₂[μ] ℝ)
  rw [← EventuallyEq] at h_comp
  refine EventuallyEq.trans ?_ h_comp.symm
  filter_upwards with y using rfl

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