English
Let s be measurable, t measurable with finite measure, and x ∈ E'. Then the L^1-norm of condExpL2 indicator is bounded by μ(s ∩ t) times the norm of x.
Русский
Пусть s и t измеримы и имеют конечную меру; тогда ||condExpL2( indicatorConstLp 2 hs hμs x )||_1 на t ≤ μ(s ∩ t) · ||x||.
LaTeX
$$$\int_{a \in t} \big\| (\operatorname{condExpL2} E' \, 𝕜 \; hm \; (\operatorname{indicatorConstLp} 2 hs hμs 1) : α \to E') (a) \big\|_+ \, dμ(a) \le μ(s \cap t) \cdot \|x\|_+$$
Lean4
theorem lintegral_nnnorm_condExpL2_le (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) (f : Lp ℝ 2 μ) :
∫⁻ x in s, ‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ ∂μ ≤ ∫⁻ x in s, ‖f x‖₊ ∂μ :=
by
let h_meas := lpMeas.aestronglyMeasurable (condExpL2 ℝ ℝ hm f)
let g := h_meas.choose
have hg_meas : StronglyMeasurable[m] g := h_meas.choose_spec.1
have hg_eq : g =ᵐ[μ] condExpL2 ℝ ℝ hm f := h_meas.choose_spec.2.symm
have hg_eq_restrict : g =ᵐ[μ.restrict s] condExpL2 ℝ ℝ hm f := ae_restrict_of_ae hg_eq
have hg_nnnorm_eq : (fun x => (‖g x‖₊ : ℝ≥0∞)) =ᵐ[μ.restrict s] fun x => (‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ : ℝ≥0∞) :=
by
refine hg_eq_restrict.mono fun x hx => ?_
dsimp only
simp_rw [hx]
rw [lintegral_congr_ae hg_nnnorm_eq.symm]
refine lintegral_enorm_le_of_forall_fin_meas_integral_eq hm (Lp.stronglyMeasurable f) ?_ ?_ ?_ ?_ hs hμs
· exact integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs
· exact hg_meas
· rw [IntegrableOn, integrable_congr hg_eq_restrict]
exact integrableOn_condExpL2_of_measure_ne_top hm hμs f
· intro t ht hμt
rw [← integral_condExpL2_eq_of_fin_meas_real (hm := hm) f ht hμt.ne]
exact setIntegral_congr_ae (hm t ht) (hg_eq.mono fun x hx _ => hx)
