-- 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:
case inr.inr.inr.inr.inr.intro.intro.hf
α : 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
⊢ Summable fun i => ‖f i‖ ^ p.toReal

Tactic:
have hf' := hfq.summable hq

Result:
case inr.inr.inr.inr.inr.intro.intro.hf
α : 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
⊢ Summable fun i => ‖f i‖ ^ p.toReal

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 : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
this : 0 ≤ ‖f i‖ ^ p.toReal
⊢ 1 ≤ ‖f i‖

Tactic:
simp only [abs_of_nonneg, this] at 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‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal
⊢ 1 ≤ ‖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
⊢ ‖f i‖ ^ p.toReal = 0

Tactic:
have : f i = 0 := by simpa using hi

Result:
α : 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

Proof state:
case inr.inr.inl.intro
α : 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
⊢ Memℓp f p

Tactic:
apply memℓp_gen

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
⊢ Summable fun i => ‖f i‖ ^ p.toReal

Proof state:
case inr.inr.inr.inr.inr.intro.intro
α : 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
⊢ Memℓp f p

Tactic:
apply memℓp_gen

Result:
case inr.inr.inr.inr.inr.intro.intro.hf
α : 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
⊢ Summable fun i => ‖f i‖ ^ p.toReal

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 ∉ ⋯.toFinset, ‖f i‖ ^ p.toReal = 0

Tactic:
intro i hi

Result:
α : 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‖ ^ p.toReal = 0

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
this : ∀ i ∉ ⋯.toFinset, ‖f i‖ ^ p.toReal = 0
⊢ Summable fun i => ‖f i‖ ^ p.toReal

Tactic:
exact summable_of_ne_finset_zero this

Result:
no goals

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 : α
⊢ (fun i => ‖f i‖) i ≤ A ^ q.toReal⁻¹

Tactic:
have : 0 ≤ ‖f i‖ ^ q.toReal := by positivity

Result:
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⁻¹

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‖ < 1
⊢ ‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal

Tactic:
exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'

Result:
no goals

Proof state:
case inr.inl.intro.hf.intro
α : 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})
⊢ BddAbove (Set.range fun i => ‖f i‖)

Tactic:
use max 0 C

Result:
case h
α : 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})
⊢ 0 ⊔ C ∈ upperBounds (Set.range fun i => ‖f i‖)

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 : α
hi : ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal
⊢ 1 ≤ ‖f i‖

Tactic:
have : 0 ≤ ‖f i‖ ^ p.toReal := Real.rpow_nonneg (norm_nonneg _) p.toReal

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
this : 0 ≤ ‖f i‖ ^ p.toReal
⊢ 1 ≤ ‖f i‖

Proof state:
case inr.inr.inr.inr.inl.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 ≤ ⊤
⊢ Memℓp f ⊤

Tactic:
apply memℓp_infty

Result:
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‖)

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
⊢ {x | (fun i => ‖‖f i‖ ^ p.toReal‖ ≤ ‖f i‖ ^ q.toReal) x}ᶜ ⊆ {i | 1 ≤ ‖f i‖}

Tactic:
show ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖

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 : α), ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖