awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ∞
f : (i : α) → E i
rw :
  (if p = ∞ then BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
    else Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal) ↔
    Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
⊢ (if p = 0 then Set.Finite.{u_3} (α := α) {i : α | ¬f i = 0}
    else
      if p = ∞ then BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
      else Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal) ↔
    Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
have rw₁ : (Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal) ↔ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
Tactic: rw [if_neg hp.1.ne', if_neg hp.2.ne]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
⊢ Memℓp (E := E) f p
have inl : ∀ (hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0), Memℓp (E := E) f 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
inl : ∀ (hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0), Memℓp (E := E) f 0
⊢ Memℓp (E := E) f p
have inr : ∀ (hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal ∞), Memℓp (E := E) f ∞
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
inl : ∀ (hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0), Memℓp (E := E) f 0
inr : ∀ (hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal ∞), Memℓp (E := E) f ∞
⊢ Memℓp (E := E) f p
have inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) f p
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0
⊢ Memℓp (E := E) f 0
have inl : Set.Finite.{u_3} (α := α) {i : α | f i ≠ 0}
Tactic: apply memℓp_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal 0
⊢ Set.Finite.{u_3} (α := α) {i : α | f i ≠ 0}
have H : Summable (α := ℝ) fun (x : α) ↦ 1
Tactic: have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ ENNReal.toReal ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
have H : Summable (α := ℝ) fun (x : α) ↦ 1
Tactic: have H : Summable fun _ : α => (1 : ℝ) := by simpa using hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ Memℓp (E := E) f p
have hf₁ : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
Tactic: apply memℓp_gen
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
have h : HasSum (α := ℝ) (fun (i : α) ↦ ‖f i‖ ^ p.toReal) (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)
Tactic: use ⨆ s : Finset α, ∑ i ∈ s, ‖f i‖ ^ p.toReal
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖f i‖ ^ p.toReal) (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)
have h : ∀ (i : α), 0 ≤ ‖f i‖ ^ p.toReal
Tactic: apply hasSum_of_isLUB_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
h : ∀ (i : α), 0 ≤ ‖f i‖ ^ p.toReal
⊢ HasSum (α := ℝ) (fun (i : α) ↦ ‖f i‖ ^ p.toReal) (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)
have h₁ : IsLUB (α := ℝ) (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal) (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)
Tactic: apply hasSum_of_isLUB_of_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ IsLUB (α := ℝ) (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)
    (⨆ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal)
have h : BddAbove (α := ℝ) (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)
Tactic: apply isLUB_ciSup
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
C : ℝ
f : (i : α) → E i
hf : ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
⊢ BddAbove (α := ℝ) (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (s : Finset α) ↦ ∑ i ∈ s, ‖f i‖ ^ p.toReal)) C
Tactic: use C
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
⊢ Memℓp (E := E) f p ↔ ∀ (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)
have refine : ∀ (hf : Memℓp (E := E) f p) (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)
Tactic: refine ⟨fun hf ↦ ?_, memℓp_gen'⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hf : Memℓp (E := E) f p
⊢ ∀ (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)
have hp₁ : 0 < p
Tactic: obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hf : Memℓp (E := E) f p
hp₁ : 0 < p
⊢ ∀ (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)
have hp₂ : p < ∞
Tactic: obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
hf : Memℓp (E := E) f p
hp₁ : 0 < p
hp₂ : p < ∞
⊢ ∀ (s : Finset α), LE.le (α := ℝ) (∑ i ∈ s, ‖f i‖ ^ p.toReal) (∑' (i : α), ‖f i‖ ^ p.toReal)
have hf₁ : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
Tactic: simp only [Memℓp, hp₁.ne', ↓reduceIte, hp₂.ne] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hp : 0 < p.toReal
⊢ Memℓp (E := E) f p ↔ ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
have refine : ∀ (hf : Memℓp (E := E) f p), ∃ (C : ℝ), 0 ≤ C ∧ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ C
Tactic: refine ⟨fun hf ↦ ?_, fun ⟨C, _, hC⟩ ↦ memℓp_gen' hC⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp (E := E) 0 p
have inl : Memℓp (E := E) 0 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inl : Memℓp (E := E) 0 0
⊢ Memℓp (E := E) 0 p
have inr : Memℓp (E := E) 0 ∞
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inl : Memℓp (E := E) 0 0
inr : Memℓp (E := E) 0 ∞
⊢ Memℓp (E := E) 0 p
have inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) 0 p
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp (E := E) 0 0
have inl : Set.Finite.{u_3} (α := α) {i : α | Ne.{u_4 + 1} (α := E i) (0 i) 0}
Tactic: apply memℓp_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ norm.{u_4} (E := E i) (0 i))
have inr : BddAbove (α := ℝ) (Set.range fun (i : α) ↦ 0)
Tactic: simp only [norm_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
⊢ Memℓp (E := E) 0 p
have inr : Summable (α := ℝ) fun (i : α) ↦ norm.{u_4} (E := E i) (0 i) ^ p.toReal
Tactic: apply memℓp_gen
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) p ↔ Memℓp (E := E) f p
have inl : Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) 0 ↔ Memℓp (E := E) f 0
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
inl : Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) 0 ↔ Memℓp (E := E) f 0
⊢ Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) p ↔ Memℓp (E := E) f p
have inr : Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) ∞ ↔ Memℓp (E := E) f ∞
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
inl : Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) 0 ↔ Memℓp (E := E) f 0
inr : Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) ∞ ↔ Memℓp (E := E) f ∞
⊢ Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) p ↔ Memℓp (E := E) f p
have inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := fun (x : α) ↦ ℝ) (fun (x : α) ↦ ‖f x‖) p ↔ Memℓp (E := E) f p
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp (E := fun (i : α) ↦ ℝ) g p
hfg : ∀ (i : α), ‖f i‖ ≤ g i
⊢ Memℓp (E := E) f p
have hfg₁ : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
Tactic: replace hfg (i) : ‖f i‖ ≤ ‖g i‖ := (hfg i).trans (Real.le_norm_self _)
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp (E := fun (i : α) ↦ ℝ) g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
⊢ Memℓp (E := E) f p
have inl : ∀ (hg : Memℓp (E := fun (i : α) ↦ ℝ) g 0), Memℓp (E := E) f 0
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
Cleared hypotheses: p, hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp (E := fun (i : α) ↦ ℝ) g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
inl : ∀ (hg : Memℓp (E := fun (i : α) ↦ ℝ) g 0), Memℓp (E := E) f 0
⊢ Memℓp (E := E) f p
have inr : ∀ (hg : Memℓp (E := fun (i : α) ↦ ℝ) g ∞), Memℓp (E := E) f ∞
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
Cleared hypotheses: p, hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp (E := fun (i : α) ↦ ℝ) g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
inl : ∀ (hg : Memℓp (E := fun (i : α) ↦ ℝ) g 0), Memℓp (E := E) f 0
inr : ∀ (hg : Memℓp (E := fun (i : α) ↦ ℝ) g ∞), Memℓp (E := E) f ∞
⊢ Memℓp (E := E) f p
have inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) f p
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp (E := fun (i : α) ↦ ℝ) g 0
⊢ Memℓp (E := E) f 0
have inl : ∀ (hg : Set.Finite.{u_3} (α := α) {i : α | 0 < ‖g i‖}), Set.Finite.{u_3} (α := α) {i : α | 0 < ‖f i‖}
Tactic: simp_rw [memℓp_zero_iff, ← norm_pos_iff] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : Memℓp (E := fun (i : α) ↦ ℝ) g ∞
⊢ Memℓp (E := E) f ∞
have hg₁ : BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖g i‖)
Tactic: rw [memℓp_infty_iff] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Memℓp (E := fun (i : α) ↦ ℝ) g p
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
⊢ Memℓp (E := E) f p
have inr : ∀ (hg : Summable (α := ℝ) fun (i : α) ↦ ‖g i‖ ^ p.toReal) (hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖) (hp : 0 < p.toReal),
  Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
Tactic: rw [memℓp_gen_iff hp] at hg ⊢
Cleared hypotheses: hg, hfg, hp
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Summable (α := ℝ) fun (i : α) ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
have apply : ∀ (i : α), ‖‖f i‖ ^ p.toReal‖ ≤ ‖g i‖ ^ p.toReal
Tactic: apply hg.of_norm_bounded fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Summable (α := ℝ) fun (i : α) ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
i : α
⊢ ‖‖f i‖ ^ p.toReal‖ ≤ ‖g i‖ ^ p.toReal
have rw : ‖f i‖ ^ p.toReal ≤ ‖g i‖ ^ p.toReal
Tactic: rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Summable (α := ℝ) fun (i : α) ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
i : α
⊢ ‖f i‖ ^ p.toReal ≤ ‖g i‖ ^ p.toReal
have h₁ : ‖f i‖ ≤ ‖g i‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
⊢ Memℓp (E := E) (-f) p
have inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (-f) 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (-f) 0
⊢ Memℓp (E := E) (-f) p
have inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (-f) ∞
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (-f) 0
inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (-f) ∞
⊢ Memℓp (E := E) (-f) p
have inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) (-f) p
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f 0
⊢ Memℓp (E := E) (-f) 0
have inl : Set.Finite.{u_3} (α := α) {i : α | (-f) i ≠ 0}
Tactic: apply memℓp_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
hp : 0 < p.toReal
⊢ Memℓp (E := E) (-f) p
have inr : Summable (α := ℝ) fun (i : α) ↦ ‖(-f) i‖ ^ p.toReal
Tactic: apply memℓp_gen
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
⊢ Memℓp (E := E) f p
have inl : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 0), Memℓp (E := E) f 0
Tactic: rcases ENNReal.trichotomy₂ hpq with
    (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
Cleared hypotheses: p, q, hfq, hpq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
inl : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 0), Memℓp (E := E) f 0
⊢ Memℓp (E := E) f p
have inr : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 ∞), Memℓp (E := E) f ∞
Tactic: rcases ENNReal.trichotomy₂ hpq with
    (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
Cleared hypotheses: p, q, hfq, hpq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
inl : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 0), Memℓp (E := E) f 0
inr : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 ∞), Memℓp (E := E) f ∞
⊢ Memℓp (E := E) f p
have inr₁ : ∀ (hp : 0 < p.toReal) (hfq : Memℓp (E := E) f 0) (hpq : 0 ≤ p), Memℓp (E := E) f p
Tactic: rcases ENNReal.trichotomy₂ hpq with
    (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
Cleared hypotheses: q, hfq, hpq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
inl : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 0), Memℓp (E := E) f 0
inr : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 ∞), Memℓp (E := E) f ∞
inr₁ : ∀ (hp : 0 < p.toReal) (hfq : Memℓp (E := E) f 0) (hpq : 0 ≤ p), Memℓp (E := E) f p
⊢ Memℓp (E := E) f p
have inr₂ : ∀ (hfq : Memℓp (E := E) f ∞) (hpq : LE.le (α := ℝ≥0∞) ∞ ∞), Memℓp (E := E) f ∞
Tactic: rcases ENNReal.trichotomy₂ hpq with
    (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
Cleared hypotheses: p, q, hfq, hpq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
inl : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 0), Memℓp (E := E) f 0
inr : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 ∞), Memℓp (E := E) f ∞
inr₁ : ∀ (hp : 0 < p.toReal) (hfq : Memℓp (E := E) f 0) (hpq : 0 ≤ p), Memℓp (E := E) f p
inr₂ : ∀ (hfq : Memℓp (E := E) f ∞) (hpq : LE.le (α := ℝ≥0∞) ∞ ∞), Memℓp (E := E) f ∞
⊢ Memℓp (E := E) f p
have inr₃ : ∀ (hq : 0 < q.toReal) (hpq : q ≤ ∞), Memℓp (E := E) f ∞
Tactic: rcases ENNReal.trichotomy₂ hpq with
    (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
Cleared hypotheses: p, hpq
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hpq : q ≤ p
inl : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 0), Memℓp (E := E) f 0
inr : ∀ (hfq : Memℓp (E := E) f 0) (hpq : LE.le (α := ℝ≥0∞) 0 ∞), Memℓp (E := E) f ∞
inr₁ : ∀ (hp : 0 < p.toReal) (hfq : Memℓp (E := E) f 0) (hpq : 0 ≤ p), Memℓp (E := E) f p
inr₂ : ∀ (hfq : Memℓp (E := E) f ∞) (hpq : LE.le (α := ℝ≥0∞) ∞ ∞), Memℓp (E := E) f ∞
inr₃ : ∀ (hq : 0 < q.toReal) (hpq : q ≤ ∞), Memℓp (E := E) f ∞
⊢ Memℓp (E := E) f p
have inr₄ : ∀ (hq : 0 < q.toReal), 0 < p.toReal → ∀ (hpq' : q.toReal ≤ p.toReal), Memℓp (E := E) f p
Tactic: rcases ENNReal.trichotomy₂ hpq with
    (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
have inr : ∀ (C : ℝ) (hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C),
  BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
Tactic: obtain ⟨C, hC⟩ := (hfq.finite_dsupport.image fun i => ‖f i‖).bddAbove
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) (max 0 C)
Tactic: use max 0 C
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C
i : α
⊢ (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C
have pos : ∀ (hi : f i = 0), (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C
Tactic: by_cases hi : f i = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
hfq : Memℓp (E := E) f 0
hpq : LE.le (α := ℝ≥0∞) 0 ∞
C : ℝ
hC : Membership.mem (γ := Set ℝ) (upperBounds ((fun (i : α) ↦ ‖f i‖) '' {i : α | f i ≠ 0})) C
i : α
pos : ∀ (hi : f i = 0), (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C
⊢ (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C
have neg : ∀ (hi : ¬f i = 0), (fun (i : α) ↦ ‖f i‖) i ≤ max 0 C
Tactic: by_cases hi : f i = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : 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 (E := E) f 0
hpq : 0 ≤ p
⊢ Memℓp (E := E) f p
have inr : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
Tactic: apply memℓp_gen