English
Second variant asserting equality of integrals involving condExpL2.
Русский
Второй вариант утверждения равенства интегралов, связанных с condExpL2.
LaTeX
$$integral_condExpL2_eq (hm) (f) (hs) (hμs)$$
Lean4
theorem setLIntegral_nnnorm_condExpL2_indicator_le (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : E')
{t : Set α} (ht : MeasurableSet[m] t) (hμt : μ t ≠ ∞) :
∫⁻ a in t, ‖(condExpL2 E' 𝕜 hm (indicatorConstLp 2 hs hμs x) : α → E') a‖₊ ∂μ ≤ μ (s ∩ t) * ‖x‖₊ :=
calc
∫⁻ a in t, ‖(condExpL2 E' 𝕜 hm (indicatorConstLp 2 hs hμs x) : α → E') a‖₊ ∂μ =
∫⁻ a in t, ‖(condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) a • x‖₊ ∂μ :=
setLIntegral_congr_fun_ae (hm t ht) ((condExpL2_indicator_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) _
