English
If hm ≤ m0 and s is measurable with μ(s) finite, then condExpL2 acts trivially on the indicatorConstLp of s: condExpL2 of the indicator scaled by a constant equals the indicator itself.
Русский
Если hm ≤ m0 и s измеримо с конечной μ-масштабировкой, то CondExpL2 оставляет неизменным индикатор индикатора множества: condExpL2(indicatorConstLp 2 (hm s hs) hμs c) = indicatorConstLp 2 (hm s hs) hμs c.
LaTeX
$$$ (\operatorname{condExpL2} E \, 𝕜 \; hm \; (\operatorname{indicatorConstLp} 2 (hm s hs) hμs c) : α \to_2[μ] E) = \operatorname{indicatorConstLp} 2 (hm s hs) hμs c $$$
Lean4
theorem condExpL2_indicator_of_measurable (hm : m ≤ m0) (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) (c : E) :
(condExpL2 E 𝕜 hm (indicatorConstLp 2 (hm s hs) hμs c) : α →₂[μ] E) = indicatorConstLp 2 (hm s hs) hμs c :=
by
rw [condExpL2]
haveI : Fact (m ≤ m0) := ⟨hm⟩
have h_mem : indicatorConstLp 2 (hm s hs) hμs c ∈ lpMeas E 𝕜 m 2 μ := mem_lpMeas_indicatorConstLp hm hs hμs
let ind := (⟨indicatorConstLp 2 (hm s hs) hμs c, h_mem⟩ : lpMeas E 𝕜 m 2 μ)
have h_coe_ind : (ind : α →₂[μ] E) = indicatorConstLp 2 (hm s hs) hμs c := rfl
have h_orth_mem := Submodule.orthogonalProjection_mem_subspace_eq_self ind
rw [← h_coe_ind, h_orth_mem]
