condExpL2_indicator_ae_eq_smul — Mathlib

English

Equality of two representations of condExpL2 involving an indicator and a span singleton after appropriate transformation.

Русский

Свойство равенства различных представлений condExpL2 для индикатора и span singleton после преобразований.

LaTeX

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

Lean4

theorem condExpL2_indicator_ae_eq_smul (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E') :
    condExpL2 E' 𝕜 hm (indicatorConstLp 2 hs hμs x) =ᵐ[μ] fun a =>
      (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs (1 : ℝ)) : α → ℝ) a • x :=
  by
  rw [indicatorConstLp_eq_toSpanSingleton_compLp hs hμs x]
  have h_comp := condExpL2_comp_continuousLinearMap ℝ 𝕜 hm (toSpanSingleton ℝ x) (indicatorConstLp 2 hs hμs (1 : ℝ))
  refine h_comp.trans ?_
  exact (toSpanSingleton ℝ x).coeFn_compLp _

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