English
If f ∈ ℓ^q for q ≤ p, then f ∈ ℓ^p.
Русский
Если f ∈ ℓ^q и q ≤ p, то f ∈ ℓ^p.
LaTeX
$$$$ Mem_{\ell^p}(f,q) \land q \le p \Rightarrow Mem_{\ell^p}(f,p). $$$$
Lean4
theorem of_exponent_ge {p q : ℝ≥0∞} {f : ∀ i, E i} (hfq : Memℓp f q) (hpq : q ≤ p) : Memℓp f p :=
by
rcases ENNReal.trichotomy₂ hpq with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
· exact hfq
· apply memℓp_infty
obtain ⟨C, hC⟩ := (hfq.finite_dsupport.image fun i => ‖f i‖).bddAbove
use max 0 C
rintro x ⟨i, rfl⟩
by_cases hi : f i = 0
· simp [hi]
· exact (hC ⟨i, hi, rfl⟩).trans (le_max_right _ _)
· apply memℓp_gen
have : ∀ i ∉ hfq.finite_dsupport.toFinset, ‖f i‖ ^ p.toReal = 0 :=
by
intro i hi
have : f i = 0 := by simpa using hi
simp [this, Real.zero_rpow hp.ne']
exact summable_of_ne_finset_zero this
· exact hfq
· apply memℓp_infty
obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite
use A ^ q.toReal⁻¹
rintro x ⟨i, rfl⟩
have : 0 ≤ ‖f i‖ ^ q.toReal := by positivity
simpa [← Real.rpow_mul, mul_inv_cancel₀ hq.ne'] using Real.rpow_le_rpow this (hA ⟨i, rfl⟩) (inv_nonneg.mpr hq.le)
· apply memℓp_gen
have hf' := hfq.summable hq
refine .of_norm_bounded_eventually hf' (@Set.Finite.subset _ {i | 1 ≤ ‖f i‖} ?_ _ ?_)
· have H : {x : α | 1 ≤ ‖f x‖ ^ q.toReal}.Finite := by
simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)
exact H.subset fun i hi => Real.one_le_rpow hi hq.le
· change ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖
intro i hi
have : 0 ≤ ‖f i‖ ^ p.toReal := Real.rpow_nonneg (norm_nonneg _) p.toReal
simp only [abs_of_nonneg, this] at hi
contrapose! hi
exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'
