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)
f : ↥(lp E p)
⊢ ‖-f‖ = ‖f‖
have inl : ∀ ⦃f : ↥(lp E 0)⦄, ‖-f‖ = ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, f
-- 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 : ↥(lp E p)
inl : ∀ ⦃f : ↥(lp E 0)⦄, ‖-f‖ = ‖f‖
⊢ ‖-f‖ = ‖f‖
have inr : ∀ ⦃f : ↥(lp E ∞)⦄, ‖-f‖ = ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, f
-- 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 : ↥(lp E p)
inl : ∀ ⦃f : ↥(lp E 0)⦄, ‖-f‖ = ‖f‖
inr : ∀ ⦃f : ↥(lp E ∞)⦄, ‖-f‖ = ‖f‖
⊢ ‖-f‖ = ‖f‖
have inr₁ : ∀ (hp : 0 < p.toReal), ‖-f‖ = ‖f‖
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 : ↥(lp E ∞)
⊢ ‖-f‖ = ‖f‖
have inr : IsEmpty α → ‖-f‖ = ‖f‖
Tactic: cases isEmpty_or_nonempty α
-- 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 : ↥(lp E ∞)
inr : IsEmpty α → ‖-f‖ = ‖f‖
⊢ ‖-f‖ = ‖f‖
have inr₁ : Nonempty α → ‖-f‖ = ‖f‖
Tactic: cases isEmpty_or_nonempty α
-- 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 : ↥(lp E ∞)
h : Nonempty α
⊢ ‖-f‖ = ‖f‖
have inr : IsLUB (Set.range fun (i : α) ↦ ‖(↑(-f) : (i : α) → E i) i‖) ‖f‖
Tactic: apply (lp.isLUB_norm (-f)).unique
-- 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 : ↥(lp E p)
hp : 0 < p.toReal
⊢ ‖-f‖ = ‖f‖
have inr : ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal
Tactic: suffices ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal by
      exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this
-- 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 : ↥(lp E p)
hp : 0 < p.toReal
⊢ ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal
have inr : HasSum (fun (i : α) ↦ ‖(↑(-f) : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
Tactic: apply (lp.hasSum_norm hp (-f)).unique
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : ↥(lp E ∞)), ‖f + g‖ ≤ ‖f‖ + ‖g‖
Tactic: rcases p.dichotomy with (rfl | hp')
Cleared hypotheses: p, hp, f, g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
inl : ∀ [hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)] (f g : ↥(lp E ∞)), ‖f + g‖ ≤ ‖f‖ + ‖g‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have inr : ∀ (hp' : 1 ≤ p.toReal), ‖f + g‖ ≤ ‖f‖ + ‖g‖
Tactic: rcases p.dichotomy with (rfl | hp')
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have inl : IsEmpty α → ‖f + g‖ ≤ ‖f‖ + ‖g‖
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
inl : IsEmpty α → ‖f + g‖ ≤ ‖f‖ + ‖g‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have inl₁ : Nonempty α → ‖f + g‖ ≤ ‖f‖ + ‖g‖
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : Nonempty α
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have inl : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖)) (‖f‖ + ‖g‖)
Tactic: refine (lp.isLUB_norm (f + g)).2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (LE.le (α := ℝ≥0∞) 1 ∞)
f g : ↥(lp E ∞)
h : Nonempty α
i : α
⊢ (fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖) i ≤ ‖f‖ + ‖g‖
have inl : LE.le (α := ℝ) ((fun (i : α) ↦ ‖(↑(f + g) : (i : α) → E i) i‖) i)
  ((fun (x1 x2 : ℝ) ↦ x1 + x2) ((fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖) i)
    ((fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖) i))
Tactic: refine le_trans ?_ (add_mem_upperBounds_add
            (lp.isLUB_norm f).1 (lp.isLUB_norm g).1 ⟨_, ⟨i, rfl⟩, _, ⟨i, rfl⟩, rfl⟩)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have hp'' : 0 < p.toReal
Tactic: have hp'' : 0 < p.toReal := zero_lt_one.trans_le hp'
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
Tactic: have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
Tactic: have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
Tactic: have hf₂ := lp.hasSum_norm hp'' f
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
Tactic: have hg₂ := lp.hasSum_norm hp'' g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have inr : ∀ (C : ℝ) (hC₁ : 0 ≤ C) (hC₂ : C ≤ ‖f‖ + ‖g‖)
  (hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)),
  ‖f + g‖ ≤ ‖f‖ + ‖g‖
Tactic: obtain ⟨C, hC₁, hC₂, hCfg⟩ :=
            Real.Lp_add_le_hasSum_of_nonneg hp' hf₁ hg₁ (norm_nonneg' _) (norm_nonneg' _) hf₂ hg₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
⊢ ‖f + g‖ ≤ ‖f‖ + ‖g‖
have inr : ‖f + g‖ ≤ C
Tactic: refine le_trans ?_ hC₂
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
⊢ ‖f + g‖ ≤ C
have inr : ‖f + g‖ ^ p.toReal ≤ C ^ p.toReal
Tactic: rw [← Real.rpow_le_rpow_iff (norm_nonneg' (f + g)) hC₁ hp'']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
⊢ ‖f + g‖ ^ p.toReal ≤ C ^ p.toReal
have inr : ∀ (i : α), ‖(↑(f + g) : (i : α) → E i) i‖ ^ p.toReal ≤ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal
Tactic: refine hasSum_le ?_ (lp.hasSum_norm hp'' (f + g)) hCfg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (goal)
Goal:
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
p q : ℝ≥0∞
inst : (i : α) → NormedAddCommGroup (E i)
hp : Fact (1 ≤ p)
f g : ↥(lp E p)
hp' : 1 ≤ p.toReal
hp'' : 0 < p.toReal
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ p.toReal) (‖g‖ ^ p.toReal)
C : ℝ
hC₁ : 0 ≤ C
hC₂ : C ≤ ‖f‖ + ‖g‖
hCfg : HasSum (fun (i : α) ↦ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal) (C ^ p.toReal)
i : α
⊢ ‖(↑(f + g) : (i : α) → E i) i‖ ^ p.toReal ≤ (‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖) ^ p.toReal
have inr : ‖(↑(f + g) : (i : α) → E i) i‖ ≤ ‖(↑f : (i : α) → E i) i‖ + ‖(↑g : (i : α) → E i) i‖
Tactic: gcongr
-- 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∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖
have hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
Tactic: have hf₁ : ∀ i, 0 ≤ ‖f i‖ := fun i => norm_nonneg _
-- 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∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖
have hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
Tactic: have hg₁ : ∀ i, 0 ≤ ‖g i‖ := fun i => norm_nonneg _
-- 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∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖
have hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
Tactic: have hf₂ := lp.hasSum_norm hpq.pos f
-- 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∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖
have hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)
Tactic: have hg₂ := lp.hasSum_norm hpq.symm.pos g
-- 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∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖
have obtain : ∀ (C : ℝ) (hC' : C ≤ ‖f‖ * ‖g‖) (hC : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) C),
  (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖
Tactic: obtain ⟨C, -, hC', hC⟩ :=
    Real.inner_le_Lp_mul_Lq_hasSum_of_nonneg hpq (norm_nonneg' _) (norm_nonneg' _) hf₁ hg₁ hf₂ 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)
p q : ℝ≥0∞
hpq : p.toReal.HolderConjugate q.toReal
f : ↥(lp E p)
g : ↥(lp E q)
hf₁ : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖
hg₁ : ∀ (i : α), 0 ≤ ‖(↑g : (i : α) → E i) i‖
hf₂ : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (‖f‖ ^ p.toReal)
hg₂ : HasSum (fun (i : α) ↦ ‖(↑g : (i : α) → E i) i‖ ^ q.toReal) (‖g‖ ^ q.toReal)
C : ℝ
hC' : C ≤ ‖f‖ * ‖g‖
hC : HasSum (fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) C
⊢ (Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖) ∧
    ∑' (i : α), ‖(↑f : (i : α) → E i) i‖ * ‖(↑g : (i : α) → E i) i‖ ≤ ‖f‖ * ‖g‖
have hC'₁ : ∑' (b : α), ‖(↑f : (i : α) → E i) b‖ * ‖(↑g : (i : α) → E i) b‖ ≤ ‖f‖ * ‖g‖
Tactic: rw [← hC.tsum_eq] at hC'
Cleared hypotheses: hC', 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)
hp : p ≠ 0
f : ↥(lp E p)
i : α
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
have inl : ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) (f : ↥(lp E ∞)), ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
Tactic: rcases eq_or_ne p ∞ with (rfl | hp')
Cleared hypotheses: p, hp, f
-- 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 : p ≠ 0
f : ↥(lp E p)
i : α
inl : ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) (f : ↥(lp E ∞)), ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
have inr : ∀ (hp' : p ≠ ∞), ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
Tactic: rcases eq_or_ne p ∞ with (rfl | hp')
-- Lean 4 proof step from Mathlib.Analysis.Normed.Lp.lpSpace (hypothesis)
Goal:
α : Type u_3
E : α → Type u_4
inst : (i : α) → NormedAddCommGroup (E i)
i : α
hp : Ne (α := ℝ≥0∞) ∞ 0
f : ↥(lp E ∞)
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
have this : Nonempty α
Tactic: haveI : Nonempty α := ⟨i⟩
-- 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)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
have hp'' : 0 < p.toReal
Tactic: have hp'' : 0 < p.toReal := ENNReal.toReal_pos hp 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)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
have this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
Tactic: have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ 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)
hp : p ≠ 0
f : ↥(lp E p)
i : α
hp' : p ≠ ∞
hp'' : 0 < p.toReal
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ ‖(↑f : (i : α) → E i) i‖ ≤ ‖f‖
have inr : ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal
Tactic: rw [← Real.rpow_le_rpow_iff (norm_nonneg _) (norm_nonneg' _) 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)
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
i : α
x x_1 : ↥(lp E p)
⊢ dist ((↑x : (i : α) → E i) i) ((↑x_1 : (i : α) → E i) i) ≤ dist x x_1
have simp_rw : ‖(↑(x - x_1) : (i : α) → E i) i‖ ≤ ‖x - x_1‖
Tactic: simp_rw [dist_eq_norm, ← Pi.sub_apply, ← lp.coeFn_sub]
-- 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
f : ↥(lp E p)
s : Finset α
⊢ ∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal ≤ ‖f‖ ^ p.toReal
have rw : LE.le (α := ℝ) (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
Tactic: rw [lp.norm_rpow_eq_tsum hp f]
-- 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)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
⊢ LE.le (α := ℝ) (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
have this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
Tactic: have : ∀ i, 0 ≤ ‖f i‖ ^ p.toReal := fun i ↦ 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)
hp : 0 < p.toReal
f : ↥(lp E p)
s : Finset α
this : ∀ (i : α), 0 ≤ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
⊢ LE.le (α := ℝ) (∑ i ∈ s, ‖(↑f : (i : α) → E i) i‖ ^ p.toReal) (∑' (i : α), ‖(↑f : (i : α) → E i) i‖ ^ p.toReal)
have refine : Summable (α := ℝ) fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖ ^ p.toReal
Tactic: refine Summable.sum_le_tsum _ (fun i _ => this 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)
inst_1 : Nonempty α
f : ↥(lp E ∞)
C : ℝ
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
⊢ ‖f‖ ≤ C
have refine : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (i : α) ↦ ‖(↑f : (i : α) → E i) i‖)) C
Tactic: refine (isLUB_norm f).2 ?_
-- 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 : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
⊢ ‖f‖ ≤ C
have inl : IsEmpty α → ‖f‖ ≤ C
Tactic: cases isEmpty_or_nonempty α
-- 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 : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖(↑f : (i : α) → E i) i‖ ≤ C
inl : IsEmpty α → ‖f‖ ≤ C
⊢ ‖f‖ ≤ C
have inr : Nonempty α → ‖f‖ ≤ C
Tactic: cases isEmpty_or_nonempty α
-- 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 : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
⊢ ‖x‖ ≤ ‖y‖
have inl : ∀ (hp : Ne (α := ℝ≥0∞) 0 0) {x : ↥(lp E 0)} {y : ↥(lp F 0)}
  (h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖), ‖x‖ ≤ ‖y‖
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
Cleared hypotheses: p, hp, x, y, h
-- 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 : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
inl :
  ∀ (hp : Ne (α := ℝ≥0∞) 0 0) {x : ↥(lp E 0)} {y : ↥(lp F 0)}
    (h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖), ‖x‖ ≤ ‖y‖
⊢ ‖x‖ ≤ ‖y‖
have inr : ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) {x : ↥(lp E ∞)} {y : ↥(lp F ∞)}
  (h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖), ‖x‖ ≤ ‖y‖
Tactic: obtain (rfl | rfl | hp) := p.trichotomy
Cleared hypotheses: p, hp, x, y, h
-- 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 : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
inl :
  ∀ (hp : Ne (α := ℝ≥0∞) 0 0) {x : ↥(lp E 0)} {y : ↥(lp F 0)}
    (h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖), ‖x‖ ≤ ‖y‖
inr :
  ∀ (hp : Ne (α := ℝ≥0∞) ∞ 0) {x : ↥(lp E ∞)} {y : ↥(lp F ∞)}
    (h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖), ‖x‖ ≤ ‖y‖
⊢ ‖x‖ ≤ ‖y‖
have inr₁ : ∀ (hp : 0 < p.toReal), ‖x‖ ≤ ‖y‖
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 : α → Type u_5
inst_1 : (i : α) → NormedAddCommGroup (F i)
p : ℝ≥0∞
hp_1 : p ≠ 0
x : ↥(lp E p)
y : ↥(lp F p)
h : ∀ (i : α), ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
hp : 0 < p.toReal
s : Finset α
⊢ LE.le (α := ℝ) (∑ i ∈ s, ‖(↑x : (i : α) → E i) i‖ ^ p.toReal) (∑ i ∈ s, ‖(↑y : (i : α) → F i) i‖ ^ p.toReal)
have h₁ : ∀ i ∈ s, ‖(↑x : (i : α) → E i) i‖ ≤ ‖(↑y : (i : α) → F i) i‖
Tactic: gcongr with i _
-- 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)
hp : p ≠ 0
c : 𝕜
f : ↥(lp E p)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have inl : ∀ (hp : Ne (α := ℝ≥0∞) 0 0) (f : ↥(lp E 0)), ‖c • f‖ ≤ ‖c‖ * ‖f‖
Tactic: rcases p.trichotomy with (rfl | rfl | hp)
Cleared hypotheses: p, hp, f