awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
i : α
hi : i ∉ ⋯.toFinset (s := {i : α | f i ≠ 0})
⊢ ‖f i‖ ^ p.toReal = 0
have this : f i = 0
Tactic: have : f i = 0 := by simpa using hi
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
have this : ∀ i ∉ sorry.toFinset (s := {i : α | f i ≠ 0}), ‖f i‖ ^ p.toReal = 0
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']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hq : 0 < q.toReal
hpq : q ≤ ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
have inr : ∀ (A : ℝ) (hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖ ^ q.toReal)) A),
  BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
Tactic: obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖ ^ q.toReal)) A
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖f i‖)
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) (A ^ q.toReal⁻¹)
Tactic: use A ^ q.toReal⁻¹
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp (E := E) f q
hq : 0 < q.toReal
hpq : q ≤ ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖ ^ q.toReal)) A
i : α
⊢ (fun (i : α) ↦ ‖f i‖) i ≤ A ^ q.toReal⁻¹
have this : 0 ≤ ‖f i‖ ^ q.toReal
Tactic: have : 0 ≤ ‖f i‖ ^ q.toReal := by positivity
-- 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
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ 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 (hypothesis)
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
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
have hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
Tactic: have hf' := hfq.summable hq
-- 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
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
have inr : Set.Finite.{u_3} (α := α) {i : α | 1 ≤ ‖f i‖}
Tactic: refine .of_norm_bounded_eventually hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } ?_ _ ?_)
-- 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
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
inr : Set.Finite.{u_3} (α := α) {i : α | 1 ≤ ‖f i‖}
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ p.toReal
have inr₁ : Subset.{u_3} (α := Set α) {x : α | (fun (i : α) ↦ ‖‖f i‖ ^ p.toReal‖ ≤ ‖f i‖ ^ q.toReal) x}ᶜ {i : α | 1 ≤ ‖f i‖}
Tactic: refine .of_norm_bounded_eventually hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } ?_ _ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
hq : 0 < q.toReal
left : 0 < p.toReal
hpq' : q.toReal ≤ p.toReal
hf' : Summable (α := ℝ) fun (i : α) ↦ ‖f i‖ ^ q.toReal
⊢ Set.Finite.{u_3} (α := α) {i : α | 1 ≤ ‖f i‖}
have H : Set.Finite.{u_3} (α := α) {x : α | 1 ≤ ‖f x‖ ^ q.toReal}
Tactic: have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by
        simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
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‖
have this : 0 ≤ ‖f i‖ ^ p.toReal
Tactic: have : 0 ≤ ‖f i‖ ^ p.toReal := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
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
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‖
have hi₁ : ¬‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal
Tactic: simp only [abs_of_nonneg, this] at hi
Cleared hypotheses: hi
-- 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
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‖
have inr : ∀ (hi : ‖f i‖ < 1), ‖f i‖ ^ p.toReal ≤ ‖f i‖ ^ q.toReal
Tactic: contrapose! hi
Cleared hypotheses: hi
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
⊢ Memℓp (E := E) (f + g) p
have inl : ∀ (hf : Memℓp (E := E) f 0) (hg : Memℓp (E := E) g 0), Memℓp (E := E) (f + g) 0
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hf, 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
inl : ∀ (hf : Memℓp (E := E) f 0) (hg : Memℓp (E := E) g 0), Memℓp (E := E) (f + g) 0
⊢ Memℓp (E := E) (f + g) p
have inr : ∀ (hf : Memℓp (E := E) f ∞) (hg : Memℓp (E := E) g ∞), Memℓp (E := E) (f + g) ∞
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hf, 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
inl : ∀ (hf : Memℓp (E := E) f 0) (hg : Memℓp (E := E) g 0), Memℓp (E := E) (f + g) 0
inr : ∀ (hf : Memℓp (E := E) f ∞) (hg : Memℓp (E := E) g ∞), Memℓp (E := E) (f + g) ∞
⊢ Memℓp (E := E) (f + g) p
have inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) (f + g) 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 g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
⊢ Memℓp (E := E) (f + g) 0
have inl : Set.Finite.{u_3} (α := α) {i : α | (f + g) 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)
f g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
⊢ Set.Finite.{u_3} (α := α) {i : α | (f + g) i ≠ 0}
have inl : ∀ (i : α),
  Membership.mem (γ := Set α) {i : α | (f + g) i ≠ 0} i →
    Membership.mem (γ := Set α) ({i : α | f i ≠ 0} ∪ {i : α | g i ≠ 0}) i
Tactic: refine (hf.finite_dsupport.union hg.finite_dsupport).subset fun i => ?_
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
i : α
⊢ Membership.mem (γ := Set α) {i : α | (f + g) i ≠ 0} i →
    Membership.mem (γ := Set α) ({i : α | f i ≠ 0} ∪ {i : α | g i ≠ 0}) i
have inl : ¬f i + g i = 0 → ¬f i = 0 ∨ ¬g i = 0
Tactic: simp only [Pi.add_apply, Ne, Set.mem_union, Set.mem_setOf_eq]
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f 0
hg : Memℓp (E := E) g 0
i : α
⊢ ¬f i + g i = 0 → ¬f i = 0 ∨ ¬g i = 0
have inl : f i = 0 ∧ g i = 0 → f i + g i = 0
Tactic: contrapose!
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f ∞
hg : Memℓp (E := E) g ∞
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)
have inr : ∀ (A : ℝ) (hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A),
  BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)
Tactic: obtain ⟨A, hA⟩ := hf.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 g : (i : α) → E i
hf : Memℓp (E := E) f ∞
hg : Memℓp (E := E) g ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)
have inr : ∀ (B : ℝ) (hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖g i‖)) B),
  BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)
Tactic: obtain ⟨B, hB⟩ := hg.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 g : (i : α) → E i
hf : Memℓp (E := E) f ∞
hg : Memℓp (E := E) g ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
B : ℝ
hB : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖g i‖)) B
⊢ BddAbove (α := ℝ) (Set.range fun (i : α) ↦ ‖(f + g) i‖)
have inr : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖(f + g) i‖)) (A + B)
Tactic: refine ⟨A + B, ?_⟩
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
⊢ Memℓp (E := E) (f + g) p
have inr : Summable (α := ℝ) fun (i : α) ↦ ‖(f + g) 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(f + g) i‖ ^ p.toReal
have inr : ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ p.toReal
Tactic: refine .of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
inr : ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ p.toReal
⊢ Summable (α := ℝ) fun (i : α) ↦ ‖(f + g) i‖ ^ p.toReal
have inr₁ : ∀ (i : α), ‖(f + g) i‖ ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
Tactic: refine .of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
⊢ ‖(f + g) i‖ ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
have inr : (‖f i‖ + ‖g i‖) ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
Tactic: refine (Real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans ?_
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤
    (if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
have pos : ∀ (h : p.toReal < 1), (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 1 * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
Tactic: split_ifs with h
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
pos : ∀ (h : p.toReal < 1), (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 1 * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤
    (if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
have neg : ∀ (h : ¬p.toReal < 1),
  (‖f i‖ + ‖g i‖) ^ p.toReal ≤ HPow.hPow (α := ℝ) 2 (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
Tactic: split_ifs with h
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else HPow.hPow (α := ℝ) 2 (p.toReal - 1)
i : α
h : ¬p.toReal < 1
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ HPow.hPow (α := ℝ) 2 (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)
have h₁ : 1 ≤ p.toReal
Tactic: simp only [not_lt] at h
Cleared hypotheses: h
-- 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 g : (i : α) → E i
hf : Memℓp (E := E) f p
hg : Memℓp (E := E) g p
⊢ Memℓp (E := E) (f - g) p
have rw : Memℓp (E := E) (f + -g) p
Tactic: rw [sub_eq_add_neg]
-- 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)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ i ∈ s, Memℓp (E := E) (f i) p
⊢ Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
have haveI : ∀ (this : DecidableEq ι), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
Tactic: haveI : DecidableEq ι := Classical.decEq _
-- 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)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
hf : ∀ i ∈ s, Memℓp (E := E) (f i) p
this : DecidableEq ι
⊢ Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
have revert : ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
Tactic: revert 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)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
⊢ ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
have refine_1 : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Memℓp (E := E) (f i) p),
  Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ ∅, f i a) p
Tactic: refine Finset.induction_on s ?_ ?_
-- 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)
ι : Type u_5
s : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
refine_1 :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Memℓp (E := E) (f i) p),
    Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ ∅, f i a) p
⊢ ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
have refine_2 : ∀ (a : ι) (s : Finset ι),
  a ∉ s →
    (∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p) →
      ∀ (hf : ∀ i ∈ insert a s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a_3 : α) ↦ ∑ i ∈ insert a s, f i a_3) p
Tactic: refine Finset.induction_on s ?_ ?_
-- 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)
ι : Type u_5
s_1 : Finset ι
f : ι → (i : α) → E i
this : DecidableEq ι
i : ι
s : Finset ι
his : i ∉ s
ih : ∀ (hf : ∀ i ∈ s, Memℓp (E := E) (f i) p), Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ s, f i a) p
hf : ∀ i_1 ∈ insert i s, Memℓp (E := E) (f i_1) p
⊢ Memℓp (E := E) (fun (a : α) ↦ ∑ i ∈ insert i s, f i a) p
have refine_2 : Memℓp (E := E) (fun (a : α) ↦ f i a + ∑ i ∈ s, f i a) p
Tactic: simp only [his, Finset.sum_insert, not_false_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
⊢ Memℓp (E := E) (c • f) p
have inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (c • 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_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (c • f) 0
⊢ Memℓp (E := E) (c • f) p
have inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (c • 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_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
inl : ∀ (hf : Memℓp (E := E) f 0), Memℓp (E := E) (c • f) 0
inr : ∀ (hf : Memℓp (E := E) f ∞), Memℓp (E := E) (c • f) ∞
⊢ Memℓp (E := E) (c • f) p
have inr₁ : ∀ (hp : 0 < p.toReal), Memℓp (E := E) (c • f) p
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f 0
⊢ Memℓp (E := E) (c • f) 0
have inl : Set.Finite.{u_3} (α := α) {i : α | (c • f) i ≠ 0}
Tactic: apply memℓp_zero
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f 0
⊢ Set.Finite.{u_3} (α := α) {i : α | (c • f) i ≠ 0}
have inl : ∀ (i : α), ¬c • f i = 0 → ¬f i = 0
Tactic: refine hf.finite_dsupport.subset fun i => (?_ : ¬c • f i = 0 → ¬f i = 0)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
⊢ Memℓp (E := E) (c • f) ∞
have inr : ∀ (A : ℝ) (hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A), Memℓp (E := E) (c • f) ∞
Tactic: obtain ⟨A, hA⟩ := hf.bddAbove
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
⊢ Memℓp (E := E) (c • f) ∞
have inr : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖(c • f) i‖)) (‖c‖ * A)
Tactic: refine memℓp_infty ⟨‖c‖ * A, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
⊢ (fun (i : α) ↦ ‖(c • f) i‖) i ≤ ‖c‖ * A
have inr : ‖c • f i‖ ≤ ‖c‖ * A
Tactic: dsimp only [Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
⊢ ‖c • f i‖ ≤ ‖c‖ * A
have inr : ‖c‖ * ‖f i‖ ≤ ‖c‖ * A
Tactic: refine (norm_smul_le _ _).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp (E := E) f ∞
A : ℝ
hA : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖f i‖)) A
i : α
⊢ ‖c‖ * ‖f i‖ ≤ ‖c‖ * A
have inr : ‖f i‖ ≤ A
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
inst_1 : NormedRing 𝕜
inst_2 : (i : α) → Module.{u_1, u_4} 𝕜 (E i)
inst_3 : ∀ (i : α), IsBoundedSMul.{u_1, u_4} 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp (E := E) f p
c : 𝕜
hp : 0 < p.toReal
⊢ Memℓp (E := E) (c • f) p
have inr : Summable (α := ℝ) fun (i : α) ↦ ‖(c • f) i‖ ^ p.toReal
Tactic: apply memℓp_gen