English
For a natural number n, eLpNorm(n • f) = n · eLpNorm(f).
Русский
Для натурального n: eLpNorm(n • f) = n · eLpNorm(f).
LaTeX
$$$$eLpNorm(n \\cdot f)_{p} = n \\cdot eLpNorm(f)_{p}.$$$$
Lean4
theorem ae_bdd_liminf_atTop_of_eLpNorm_bdd {p : ℝ≥0∞} (hp : p ≠ 0) {f : ℕ → α → E} (hfmeas : ∀ n, Measurable (f n))
(hbdd : ∀ n, eLpNorm (f n) p μ ≤ R) : ∀ᵐ x ∂μ, liminf (fun n => (‖f n x‖ₑ)) atTop < ∞ :=
by
by_cases hp' : p = ∞
· subst hp'
simp_rw [eLpNorm_exponent_top] at hbdd
have : ∀ n, ∀ᵐ x ∂μ, (‖f n x‖ₑ) < R + 1 := fun n =>
ae_lt_of_essSup_lt (lt_of_le_of_lt (hbdd n) <| ENNReal.lt_add_right ENNReal.coe_ne_top one_ne_zero)
rw [← ae_all_iff] at this
filter_upwards [this] with x hx using
lt_of_le_of_lt (liminf_le_of_frequently_le' <| Frequently.of_forall fun n => (hx n).le)
(ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.one_lt_top⟩)
filter_upwards [ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd hfmeas hbdd] with x hx
have hppos : 0 < p.toReal := ENNReal.toReal_pos hp hp'
have : liminf (fun n => (‖f n x‖ₑ) ^ p.toReal) atTop = liminf (fun n => (‖f n x‖ₑ)) atTop ^ p.toReal :=
by
change
liminf (fun n => ENNReal.orderIsoRpow p.toReal hppos (‖f n x‖ₑ)) atTop =
ENNReal.orderIsoRpow p.toReal hppos (liminf (fun n => (‖f n x‖ₑ)) atTop)
refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm <;> isBoundedDefault
rw [this] at hx
rw [← ENNReal.rpow_one (liminf (‖f · x‖ₑ) atTop), ← mul_inv_cancel₀ hppos.ne.symm, ENNReal.rpow_mul]
exact ENNReal.rpow_lt_top_of_nonneg (inv_nonneg.2 hppos.le) hx.ne
