awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
pos : 0 < p
s : Finset ι
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have h₁ : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑' (i : ι), f i ^ p)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
pos : 0 < p
s : Finset ι
h₁ : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑' (i : ι), f i ^ p)
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have h₂ : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (∑' (i : ι), g i ^ p)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
pos : 0 < p
⊢ (Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p) ∧
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have H₁ : ∀ (s : Finset ι),
  ∑ i ∈ s, (f i + g i) ^ p ≤
    (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p
Tactic: have H₁ : ∀ s : Finset ι,
      (∑ i ∈ s, (f i + g i) ^ p) ≤
        ((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p := by
    intro s
    rw [one_div, ← NNReal.rpow_inv_le_iff pos, ← one_div]
    refine le_trans (Lp_add_le s f g hp) ?_
    gcongr <;>
      refine Summable.sum_le_tsum _ (fun _ _ ↦ zero_le) ?_
    exacts [hf, hg]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι),
    ∑ i ∈ s, (f i + g i) ^ p ≤
      (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p
⊢ BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i + g i) ^ p)
have refine : Membership.mem (γ := Set ℝ≥0) (upperBounds (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i + g i) ^ p))
  ((HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p)
Tactic: refine ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι),
    ∑ i ∈ s, (f i + g i) ^ p ≤
      (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p
⊢ (Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p) ∧
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have bdd : BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i + g i) ^ p)
Tactic: have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p) := by
    refine ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, ?_⟩
    rintro a ⟨s, rfl⟩
    exact H₁ s
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι),
    ∑ i ∈ s, (f i + g i) ^ p ≤
      (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p
bdd : BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i + g i) ^ p)
⊢ (Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p) ∧
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have H₂ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
Tactic: have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι),
    ∑ i ∈ s, (f i + g i) ^ p ≤
      (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p
bdd : BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
⊢ (Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p) ∧
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have refine : HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
Tactic: refine ⟨H₂, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι),
    ∑ i ∈ s, (f i + g i) ^ p ≤
      (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p
bdd : BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
⊢ HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have rw : ∑' (i : ι), (f i + g i) ^ p ≤
  (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p
Tactic: rw [one_div, NNReal.rpow_inv_le_iff pos, ← one_div]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
have hp' : p ≠ 0
Tactic: have hp' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp).ne'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
have H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
Tactic: obtain ⟨H₁, H₂⟩ := Lp_add_le_tsum hp hf.summable hg.summable
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
have H₂ : HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
Tactic: obtain ⟨H₁, H₂⟩ := Lp_add_le_tsum hp hf.summable hg.summable
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
H₂ :
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
⊢ A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
have rw : A = (A ^ p) ^ (1 / p)
Tactic: rw [hf.tsum_eq, rpow_inv_rpow_self hp']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
H₂ :
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
rw : A = (A ^ p) ^ (1 / p)
⊢ A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
have rw₁ : A = A
Tactic: rw [hf.tsum_eq, rpow_inv_rpow_self hp']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
H₂ :
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
have hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
Tactic: have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hp']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
H₂ :
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
⊢ B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have rw : B = (B ^ p) ^ (1 / p)
Tactic: rw [hg.tsum_eq, rpow_inv_rpow_self hp']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
H₂ :
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
rw : B = (B ^ p) ^ (1 / p)
⊢ B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
have rw₁ : B = B
Tactic: rw [hg.tsum_eq, rpow_inv_rpow_self hp']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
H₂ :
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
have hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
Tactic: have hB : B = (∑' i : ι, g i ^ p) ^ (1 / p) := by rw [hg.tsum_eq, rpow_inv_rpow_self hp']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
H₂ :
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
have refine_1 : HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤ A + B
Tactic: refine ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p
H₂ :
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
refine_1 : HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤ A + B
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
have refine_2 : HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ^ p)
Tactic: refine ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ q) (1 / q)
have refine : ∀ i ∈ s, f i * g i ≤ |f i| * |g i|
Tactic: refine le_trans (sum_le_sum fun i _ ↦ ?_) (by simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i|) p ≤ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ i ∈ s, |f i| ^ p
have this : (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| sorry) i) p) : ℝ) ≤
  (↑(HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) *
        ∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| sorry) i) p) :
    ℝ)
Tactic: have :=
    NNReal.coe_le_coe.2
      (NNReal.rpow_sum_le_const_mul_sum_rpow s (fun i => ⟨_, abs_nonneg (f i)⟩) hp)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) i) p) : ℝ) ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) *
          ∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) i) p) :
      ℝ)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i|) p ≤ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ i ∈ s, |f i| ^ p
have this₁ : HPow.hPow (α := ℝ) (∑ i ∈ s, (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| sorry) : ℝ)) p ≤
  HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ x ∈ s, (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f x| sorry) : ℝ) ^ p
Tactic: push_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i + g i| ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)
have this : (↑(HPow.hPow (α := ℝ≥0)
        (∑ i ∈ s, HAdd.hAdd (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |f i| sorry) i) ((fun (i : ι) ↦ NNReal.mk |g i| sorry) i) ^ p)
        (1 / p)) :
    ℝ) ≤
  (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |f i| sorry) i) p) (1 / p) +
        HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |g i| sorry) i) p) (1 / p)) :
    ℝ)
Tactic: have := NNReal.coe_le_coe.2
    (NNReal.Lp_add_le s (fun i => .mk _ (abs_nonneg (f i))) (fun i => .mk _ (abs_nonneg (g i))) hp)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  (↑(HPow.hPow (α := ℝ≥0)
          (∑ i ∈ s,
            HAdd.hAdd (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |f i| ⋯) i) ((fun (i : ι) ↦ NNReal.mk |g i| ⋯) i) ^ p)
          (1 / p)) :
      ℝ) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |f i| ⋯) i) p) (1 / p) +
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |g i| ⋯) i) p) (1 / p)) :
      ℝ)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i + g i| ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)
have this₁ : HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
  HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
Tactic: push_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i + g i| ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)
have refine_1 : LE.le (α := ℝ) 0 (∑ i ∈ s, |f i + g i| ^ p)
Tactic: refine le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
refine_1 : LE.le (α := ℝ) 0 (∑ i ∈ s, |f i + g i| ^ p)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i + g i| ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)
have refine_2 : ∀ i ∈ s, |f i + g i| ^ p ≤ (|f i| + |g i|) ^ p
Tactic: refine le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
refine_1 : LE.le (α := ℝ) 0 (∑ i ∈ s, |f i + g i| ^ p)
refine_2 : ∀ i ∈ s, |f i + g i| ^ p ≤ (|f i| + |g i|) ^ p
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i + g i| ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)
have refine_3 : 0 ≤ 1 / p
Tactic: refine le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ q) (1 / q)
have h : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
Tactic: convert! inner_le_Lp_mul_Lq s f g hpq using 3
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ q) (1 / q)
have h₁ : Eq (α := ℝ) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, |g i| ^ q)
Tactic: convert! inner_le_Lp_mul_Lq s f g hpq using 3
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
have h : ∀ x ∈ s, f x ^ p = |f x| ^ p
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ Eq (α := ℝ) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, |g i| ^ q)
have h : ∀ x ∈ s, g x ^ q = |g x| ^ q
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ q) (r / q)
have h : ∀ (i : ι) (hi : i ∈ s), f i * g i = |f i * g i|
Tactic: convert! Lr_rpow_le_Lp_mul_Lq s f g hpqr using 3 with i hi
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ (i : ι) (hi : i ∈ s), f i * g i = |f i * g i|
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ q) (r / q)
have h₁ : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
Tactic: convert! Lr_rpow_le_Lp_mul_Lq s f g hpqr using 3 with i hi
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ (i : ι) (hi : i ∈ s), f i * g i = |f i * g i|
h₁ : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ q) (r / q)
have h₂ : Eq (α := ℝ) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, |g i| ^ q)
Tactic: convert! Lr_rpow_le_Lp_mul_Lq s f g hpqr using 3 with i hi
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i * g i = |f i * g i|
have h : f i * g i = f i * g i
Tactic: rw [abs_of_nonneg (mul_nonneg (hf i hi) (hg i hi))]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
have h : ∀ (i : ι) (hi : i ∈ s), f i = |f i|
Tactic: congr! with i hi
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ Eq (α := ℝ) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, |g i| ^ q)
have h : ∀ (i : ι) (hi : i ∈ s), g i = |g i|
Tactic: congr! with i hi
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have lift : ∀ (w : (i : ι) → ℝ≥0),
  ∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * f i ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i) (1 - p⁻¹) *
      HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * f i ^ p) p⁻¹
Tactic: lift w to ι → ℝ≥0 using hw
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
w : (i : ι) → ℝ≥0
⊢ ∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * f i ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i) (1 - p⁻¹) *
      HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * f i ^ p) p⁻¹
have lift : ∀ (f : (i : ι) → ℝ≥0),
  ∑ i ∈ s, HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(w i) : ℝ)) i) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i) (1 - p⁻¹) *
      HPow.hPow (α := ℝ)
        (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) p⁻¹
Tactic: lift f to ι → ℝ≥0 using hf
Cleared hypotheses: f, hf