English
Let hm ≤ m0, hs measurable, hμs ≠ ∞, x ∈ G. Then for any t measurable with hμt ≠ ∞, the lintegral over t of the nn-norm of condExpIndSMul is bounded by μ(s ∩ t) times the nn-norm of x.
Русский
Пусть hm ≤ m0, hs измеримо, hμs не бесконечно, x ∈ G. Тогда для любого измеримого t с μ(t) ≠ ∞ линтеграл по t нормы condExpIndSMul ограничен μ( s ∩ t )·‖x‖.
LaTeX
$$$\int^{\infty}_{a\in t} \|\operatorname{condExpIndSMul} hm hs hμs x a\|_+ \ dμ ≤ μ(s \cap t) \cdot \|x\|_+$$$
Lean4
theorem setLIntegral_nnnorm_condExpIndSMul_le (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) {t : Set α}
(ht : MeasurableSet[m] t) (hμt : μ t ≠ ∞) : (∫⁻ a in t, ‖condExpIndSMul hm hs hμs x a‖₊ ∂μ) ≤ μ (s ∩ t) * ‖x‖₊ :=
calc
∫⁻ a in t, ‖condExpIndSMul hm hs hμs x a‖₊ ∂μ =
∫⁻ a in t, ‖(condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) a • x‖₊ ∂μ :=
setLIntegral_congr_fun_ae (hm t ht) ((condExpIndSMul_ae_eq_smul hm hs hμs x).mono fun a ha _ => by rw [ha])
_ = (∫⁻ a in t, ‖(condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) a‖₊ ∂μ) * ‖x‖₊ :=
by
simp_rw [nnnorm_smul, ENNReal.coe_mul]
rw [lintegral_mul_const]
exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)
_ ≤ μ (s ∩ t) * ‖x‖₊ := mul_le_mul_right' (lintegral_nnnorm_condExpL2_indicator_le_real hs hμs ht hμt) _
