English
If a function f has a positive lower bound C on a measurable set s, then C · μ(s)^{1/p.toReal} ≤ eLpNorm(f, p, μ).
Русский
Если на измеримом множестве s функция f имеет нижнюю границу C > 0, то C · μ(s)^{1/p.toReal} ≤ eLpNorm(f, p, μ).
LaTeX
$$$$C \\cdot μ(s)^{1/p.toReal} \\le eLpNorm(f)_{p, μ}$$$$
Lean4
theorem ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd {p : ℝ≥0∞} {f : ℕ → α → E} (hfmeas : ∀ n, Measurable (f n))
(hbdd : ∀ n, eLpNorm (f n) p μ ≤ R) : ∀ᵐ x ∂μ, liminf (fun n => ((‖f n x‖ₑ) ^ p.toReal : ℝ≥0∞)) atTop < ∞ :=
by
by_cases hp0 : p.toReal = 0
· simp only [hp0, ENNReal.rpow_zero]
filter_upwards with _
rw [liminf_const (1 : ℝ≥0∞)]
exact ENNReal.one_lt_top
have hp : p ≠ 0 := fun h => by simp [h] at hp0
have hp' : p ≠ ∞ := fun h => by simp [h] at hp0
refine
ae_lt_top (.liminf fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
(lt_of_le_of_lt (lintegral_liminf_le fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
(lt_of_le_of_lt ?_ (by finiteness : (R : ℝ≥0∞) ^ p.toReal < ∞))).ne
simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp hp', one_div] at hbdd
simp_rw [liminf_eq, eventually_atTop]
exact sSup_le fun b ⟨a, ha⟩ => (ha a le_rfl).trans ((ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hp hp')).1 (hbdd _))
