-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem of_exponent_ge {p q : ℝ≥0∞} {f : ∀ i, E i} (hfq : Memℓp f q) (hpq : q ≤ p) : Memℓp f p

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i => ‖f i‖ ^ q.toReal
⊢ {x | 1 ≤ ‖f x‖ ^ q.toReal}.Finite

Tactic:
simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by norm_num)

Result:
no goals

Proof state:
case inr.inr.inl.intro.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
⊢ Summable fun i => ‖f i‖ ^ p.toReal

Tactic:
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']

Result:
case inr.inr.inl.intro.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
this : ∀ i ∉ ⋯.toFinset, ‖f i‖ ^ p.toReal = 0
⊢ Summable fun i => ‖f i‖ ^ p.toReal

Proof state:
case h.intro
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ q.toReal)
i : α
this : 0 ≤ ‖f i‖ ^ q.toReal
⊢ (fun i => ‖f i‖) i ≤ A ^ q.toReal⁻¹

Tactic:
simpa [← Real.rpow_mul, mul_inv_cancel₀ hq.ne'] using
  Real.rpow_le_rpow this (hA ⟨i, rfl⟩) (inv_nonneg.mpr hq.le)

Result:
no goals

Proof state:
case pos
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
C : ℝ
hC : C ∈ upperBounds ((fun i => ‖f i‖) '' {i | f i ≠ 0})
i : α
hi : f i = 0
⊢ (fun i => ‖f i‖) i ≤ 0 ⊔ C

Tactic:
simp [hi]

Result:
no goals

Proof state:
case inr.inr.inr.inr.inr.intro.intro.hf.refine_2
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i => ‖f i‖ ^ q.toReal
⊢ ∀ (i : α), ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖

Tactic:
intro i hi

Result:
case inr.inr.inr.inr.inr.intro.intro.hf.refine_2
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i => ‖f i‖ ^ q.toReal
i : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
⊢ 1 ≤ ‖f i‖

Proof state:
case inr.inl.intro
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
⊢ Memℓp f ⊤

Tactic:
apply memℓp_infty

Result:
case inr.inl.intro.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f 0
hpq : 0 ≤ ⊤
⊢ BddAbove (Set.range fun i => ‖f i‖)

Proof state:
case inr.inr.inr.inl.intro
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp f ⊤
hpq : ⊤ ≤ ⊤
⊢ Memℓp f ⊤

Tactic:
exact hfq

Result:
no goals

Proof state:
case inr.inr.inr.inr.inr.intro.intro.hf.refine_1
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i => ‖f i‖ ^ q.toReal
H : {x | 1 ≤ ‖f x‖ ^ q.toReal}.Finite
⊢ {i | 1 ≤ ‖f i‖}.Finite

Tactic:
exact H.subset fun i hi => Real.one_le_rpow hi hq.le

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ q.toReal)
i : α
⊢ 0 ≤ ‖f i‖ ^ q.toReal

Tactic:
positivity

Result:
no goals

Proof state:
case inr.inr.inr.inr.inr.intro.intro.hf.refine_2
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i => ‖f i‖ ^ q.toReal
i : α
this : 0 ≤ ‖f i‖ ^ p.toReal
hi : ¬‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal
⊢ 1 ≤ ‖f i‖

Tactic:
contrapose! hi

Result:
case inr.inr.inr.inr.inr.intro.intro.hf.refine_2
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i => ‖f i‖ ^ q.toReal
i : α
this : 0 ≤ ‖f i‖ ^ p.toReal
hi : ‖f i‖ < 1
⊢ ‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal

Proof state:
case inr.inr.inr.inr.inl.intro.hf.intro
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ q.toReal)
⊢ BddAbove (Set.range fun i => ‖f i‖)

Tactic:
use A ^ q.toReal⁻¹

Result:
case h
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ q.toReal)
⊢ A ^ q.toReal⁻¹ ∈ upperBounds (Set.range fun i => ‖f i‖)

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
hi : i ∉ ⋯.toFinset
this : f i = 0
⊢ ‖f i‖ ^ p.toReal = 0

Tactic:
simp [this, Real.zero_rpow hp.ne']

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
f : (i : α) → E i
hp : 0 < p.toReal
hfq : Memℓp f 0
hpq : 0 ≤ p
i : α
hi : i ∉ ⋯.toFinset
⊢ f i = 0

Tactic:
simpa using hi

Result:
no goals

Proof state:
case inr.inr.inr.inr.inl.intro.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ⊤
⊢ BddAbove (Set.range fun i => ‖f i‖)

Tactic:
obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite

Result:
case inr.inr.inr.inr.inl.intro.hf.intro
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hq : 0 < q.toReal
hpq : q ≤ ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖ ^ q.toReal)
⊢ BddAbove (Set.range fun i => ‖f i‖)

Proof state:
case inr.inr.inr.inr.inr.intro.intro.hf.refine_1
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i => ‖f i‖ ^ q.toReal
⊢ {i | 1 ≤ ‖f i‖}.Finite

Tactic:
have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by
  simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by norm_num)

Result:
case inr.inr.inr.inr.inr.intro.intro.hf.refine_1
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
hq : 0 < q.toReal
left✝ : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable fun i => ‖f i‖ ^ q.toReal
H : {x | 1 ≤ ‖f x‖ ^ q.toReal}.Finite
⊢ {i | 1 ≤ ‖f i‖}.Finite