English
Given a continuous linear map L and φ in Lp, the integral of L ∘ φ equals the integral of φ mapped by L.
Русский
Для непрерывного линейного отображения L и φ в Lp, интеграл от L ∘ φ равен L от интеграла φ.
LaTeX
$$$\\int (L(φ(x))) dμ = L(\\int φ(x) dμ)$$$
Lean4
theorem eLpNorm_one_le_of_le {r : ℝ≥0} (hfint : Integrable f μ) (hfint' : 0 ≤ ∫ x, f x ∂μ) (hf : ∀ᵐ ω ∂μ, f ω ≤ r) :
eLpNorm f 1 μ ≤ 2 * μ Set.univ * r := by
by_cases hr : r = 0
· suffices f =ᵐ[μ] 0 by rw [eLpNorm_congr_ae this, eLpNorm_zero, hr, ENNReal.coe_zero, mul_zero]
rw [hr] at hf
norm_cast at hf
have hnegf : ∫ x, -f x ∂μ = 0 := by
rw [integral_neg, neg_eq_zero]
exact le_antisymm (integral_nonpos_of_ae hf) hfint'
have := (integral_eq_zero_iff_of_nonneg_ae ?_ hfint.neg).1 hnegf
· filter_upwards [this] with ω hω
rwa [Pi.neg_apply, Pi.zero_apply, neg_eq_zero] at hω
· filter_upwards [hf] with ω hω
rwa [Pi.zero_apply, Pi.neg_apply, Right.nonneg_neg_iff]
by_cases hμ : IsFiniteMeasure μ
swap
· have : μ Set.univ = ∞ := by
by_contra hμ'
exact hμ (IsFiniteMeasure.mk <| lt_top_iff_ne_top.2 hμ')
rw [this, ENNReal.mul_top', if_neg, ENNReal.top_mul', if_neg]
· exact le_top
· simp [hr]
· simp
haveI := hμ
rw [integral_eq_integral_pos_part_sub_integral_neg_part hfint, sub_nonneg] at hfint'
have hposbdd : ∫ ω, max (f ω) 0 ∂μ ≤ μ.real Set.univ • (r : ℝ) :=
by
rw [← integral_const]
refine integral_mono_ae hfint.real_toNNReal (integrable_const (r : ℝ)) ?_
filter_upwards [hf] with ω hω using Real.toNNReal_le_iff_le_coe.2 hω
rw [MemLp.eLpNorm_eq_integral_rpow_norm one_ne_zero ENNReal.one_ne_top (memLp_one_iff_integrable.2 hfint),
ENNReal.ofReal_le_iff_le_toReal (by finiteness)]
simp_rw [ENNReal.toReal_one, _root_.inv_one, Real.rpow_one, Real.norm_eq_abs, ← max_zero_add_max_neg_zero_eq_abs_self,
← Real.coe_toNNReal']
rw [integral_add hfint.real_toNNReal]
· simp only [Real.coe_toNNReal', ENNReal.toReal_mul, ENNReal.coe_toReal, toReal_ofNat] at hfint' ⊢
refine (add_le_add_left hfint' _).trans ?_
rwa [← two_mul, mul_assoc, mul_le_mul_iff_right₀ (two_pos : (0 : ℝ) < 2)]
· exact hfint.neg.sup (integrable_zero _ _ μ)
