English
For q > 0, scaling f by c scales eLpNorm' by |c|: eLpNorm'(c · f)_{q} = |c| · eLpNorm'(f)_{q}.
Русский
При q > 0 масштабирование f на c масштабирует eLpNorm' на |c|: eLpNorm'(c · f)_{q} = |c| · eLpNorm'(f)_{q}.
LaTeX
$$$$eLpNorm'(c \\cdot f)_{q} = \\\\|c\\\\|_e \\, eLpNorm'(f)_{q} \\\\quad (q > 0).$$$$
Lean4
theorem le_eLpNorm_of_bddBelow (hp : p ≠ 0) (hp' : p ≠ ∞) {f : α → F} (C : ℝ≥0) {s : Set α} (hs : MeasurableSet s)
(hf : ∀ᵐ x ∂μ, x ∈ s → C ≤ ‖f x‖₊) : C • μ s ^ (1 / p.toReal) ≤ eLpNorm f p μ :=
by
rw [ENNReal.smul_def, smul_eq_mul, eLpNorm_eq_lintegral_rpow_enorm hp hp', one_div,
ENNReal.le_rpow_inv_iff (ENNReal.toReal_pos hp hp'), ENNReal.mul_rpow_of_nonneg _ _ ENNReal.toReal_nonneg, ←
ENNReal.rpow_mul, inv_mul_cancel₀ (ENNReal.toReal_pos hp hp').ne.symm, ENNReal.rpow_one, ← setLIntegral_const, ←
lintegral_indicator hs]
refine lintegral_mono_ae ?_
filter_upwards [hf] with x hx
by_cases hxs : x ∈ s
· simp only [Set.indicator_of_mem, hxs, true_implies] at hx ⊢
gcongr
rwa [coe_le_enorm]
· simp [Set.indicator_of_notMem hxs]
