English
With an AEStronglyMeasurable f, μ{x | ε ≤ ‖f x‖} ≤ ε^{-1 toReal} · (eLpNorm f)^p.toReal when ε ≠ 0.
Русский
Пусть f AEStronglyMeasurable; тогда μ{x: ε ≤ ‖f(x)‖} ≤ ε^{-1} · (eLpNorm f)^p.toReal при ε ≠ 0.
LaTeX
$$$$μ\\{x \\mid ε \\le \\|f(x)\\|_e \\} \\\\le ε^{-1} ^ {p.toReal} \\, (eLpNorm f)^{p.toReal}.$$$$
Lean4
theorem meas_ge_le_mul_pow_eLpNorm_enorm (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) {f : α → ε'}
(hf : AEStronglyMeasurable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) (hmeas_top : ε = ∞ → μ {x | ‖f x‖ₑ = ⊤} = 0) :
μ {x | ε ≤ ‖f x‖ₑ} ≤ ε⁻¹ ^ p.toReal * eLpNorm f p μ ^ p.toReal :=
by
by_cases h : ε = ∞
· have : (0 : ℝ≥0∞) ^ p.toReal = 0 := by rw [ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]
simp [h, this, hmeas_top]
· have hεpow : ε ^ p.toReal ≠ 0 := (ENNReal.rpow_pos (pos_iff_ne_zero.2 hε) h).ne.symm
have hεpow' : ε ^ p.toReal ≠ ∞ := by finiteness
rw [ENNReal.inv_rpow, ← ENNReal.mul_le_mul_left hεpow hεpow', ← mul_assoc, ENNReal.mul_inv_cancel hεpow hεpow',
one_mul]
exact mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top hf ε
