awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
⊢ ∃ C ≤ A * B, HasSum (fun (i : ι) ↦ f i * g i) C
have H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
Tactic: obtain ⟨H₁, H₂⟩ := summable_and_inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
⊢ ∃ C ≤ A * B, HasSum (fun (i : ι) ↦ f i * g i) C
have H₂ : ∑' (i : ι), f i * g i ≤
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
Tactic: obtain ⟨H₁, H₂⟩ := summable_and_inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
⊢ 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 hpq.ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
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 hpq.ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
⊢ ∃ C ≤ A * B, HasSum (fun (i : ι) ↦ f i * g i) C
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 hpq.ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
⊢ B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
have rw : B = (B ^ q) ^ (1 / q)
Tactic: rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
rw : B = (B ^ q) ^ (1 / q)
⊢ B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
have rw₁ : B = B
Tactic: rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
⊢ ∃ C ≤ A * B, HasSum (fun (i : ι) ↦ f i * g i) C
have hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
Tactic: have hB : B = (∑' i : ι, g i ^ q) ^ (1 / q) := by
    rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
⊢ ∃ C ≤ A * B, HasSum (fun (i : ι) ↦ f i * g i) C
have refine_1 : ∑' (i : ι), f i * g i ≤ A * B
Tactic: refine ⟨∑' i, f i * g i, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
refine_1 : ∑' (i : ι), f i * g i ≤ A * B
⊢ ∃ C ≤ A * B, HasSum (fun (i : ι) ↦ f i * g i) C
have refine_2 : HasSum (α := ℝ≥0) (fun (i : ι) ↦ f i * g i) (∑' (i : ι), f i * g i)
Tactic: refine ⟨∑' i, f i * g i, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
have inl : ∀ (hp : 1 = p), HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
Tactic: rcases eq_or_lt_of_le hp with hp | hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
inl :
  ∀ (hp : 1 = p), HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
have inr : ∀ (hp : 1 < p), HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
Tactic: rcases eq_or_lt_of_le hp with hp | hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
have hpq : p.HolderConjugate q
Tactic: have hpq : p.HolderConjugate q := .conjExponent hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
have hp₁ : 1 / p * p = 1
Tactic: have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p - 1
have rw : 1 / q * p = p / q
Tactic: rw [← hpq.div_conj_eq_sub_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
hp₁ : 1 / p * p = 1
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
have hq : 1 / q * p = p - 1
Tactic: have hq : 1 / q * p = p - 1 := by
    rw [← hpq.div_conj_eq_sub_one]
    ring
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ IsGreatest ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1})
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))
have left : Membership.mem (γ := Set ℝ≥0)
  ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1})
  (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
left :
  Membership.mem (γ := Set ℝ≥0)
    ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1})
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))
⊢ IsGreatest ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1})
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))
have right : Membership.mem (γ := Set ℝ≥0)
  (upperBounds ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1}))
  (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ Membership.mem (γ := Set ℝ≥0)
    ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1})
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))
have h : (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
    f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
  ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
Tactic: use fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
have h : ∀ (hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0),
  (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
Tactic: obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
h :
  ∀ (hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0),
    (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
      ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
          f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
        HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
⊢ (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
have h₁ : ∀ (hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)),
  (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
Tactic: obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
⊢ (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
have A : p + q - q ≠ 0
Tactic: have A : p + q - q ≠ 0 := by simp [hpq.ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
⊢ ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
have refine : ∀ (y : ℝ≥0) (h : y = 0), y ^ p = 0
Tactic: refine fun y => mul_div_cancel_left_of_imp fun h => ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
⊢ (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
have B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
Tactic: have B : ∀ y : ℝ≥0, y * y ^ p / y = y ^ p := by
        refine fun y => mul_div_cancel_left_of_imp fun h => ?_
        simp [h, hpq.ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
have h : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q) = HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
Tactic: simp only [Set.mem_setOf_eq, div_rpow, ← sum_div, ← rpow_mul,
        div_mul_cancel₀ _ hpq.symm.ne_zero, rpow_one, div_le_iff₀ hf, one_mul, hpq.mul_eq_add, ←
        rpow_sub' A, add_sub_cancel_right, le_refl, true_and, ← mul_div_assoc, B]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q) = HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
have h : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q) ≠ 0
Tactic: rw [div_eq_iff, ← rpow_add hf.ne', one_div, one_div, hpq.inv_add_inv_eq_one, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
g : ι → ℝ≥0
hg : Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} g
⊢ (fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) g ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
have right : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ≤
  HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
Tactic: apply le_trans (inner_le_Lp_mul_Lq s f g hpq)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
have inl : ∀ (hp : LE.le (α := ℝ) 1 1),
  HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (β := ℝ) (f i + g i) 1) (1 / 1) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (β := ℝ) (f i) 1) (1 / 1) +
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (β := ℝ) (g i) 1) (1 / 1)
Tactic: rcases eq_or_lt_of_le hp with (rfl | hp)
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
inl :
  ∀ (hp : LE.le (α := ℝ) 1 1),
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (β := ℝ) (f i + g i) 1) (1 / 1) ≤
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (β := ℝ) (f i) 1) (1 / 1) +
        HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (β := ℝ) (g i) 1) (1 / 1)
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
have inr : ∀ (hp : 1 < p),
  HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
Tactic: rcases eq_or_lt_of_le hp with (rfl | hp)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
have hpq : p.HolderConjugate p.conjExponent
Tactic: have hpq := Real.HolderConjugate.conjExponent hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
have this : IsGreatest
  ((fun (g_1 : ι → ℝ≥0) ↦ ∑ i ∈ s, (f + g) i * g_1 i) ''
    {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p.conjExponent) 1})
  (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f + g) i ^ p) (1 / p))
Tactic: have := isGreatest_Lp s (f + g) hpq
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
this :
  IsGreatest
    ((fun (g_1 : ι → ℝ≥0) ↦ ∑ i ∈ s, (f + g) i * g_1 i) ''
      {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p.conjExponent) 1})
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f + g) i ^ p) (1 / p))
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
have this₁ : IsGreatest
  ((fun (a : ι → ℝ≥0) ↦ HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x * a x) (∑ x ∈ s, g x * a x)) ''
    {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p.conjExponent) 1})
  (HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (f x + g x) ^ p) (1 / p))
Tactic: simp only [Pi.add_apply, add_mul, sum_add_distrib] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
this :
  IsGreatest
    ((fun (a : ι → ℝ≥0) ↦ HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x * a x) (∑ x ∈ s, g x * a x)) ''
      {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p.conjExponent) 1})
    (HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (f x + g x) ^ p) (1 / p))
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
have inr : ∀ (φ : ι → ℝ≥0)
  (hφ : Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p.conjExponent) 1} φ)
  (H :
    (fun (a : ι → ℝ≥0) ↦ HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x * a x) (∑ x ∈ s, g x * a x)) φ =
      HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (f x + g x) ^ p) (1 / p)),
  HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
Tactic: rcases this.1 with ⟨φ, hφ, H⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
this :
  IsGreatest
    ((fun (a : ι → ℝ≥0) ↦ HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x * a x) (∑ x ∈ s, g x * a x)) ''
      {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p.conjExponent) 1})
    (HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (f x + g x) ^ p) (1 / p))
φ : ι → ℝ≥0
hφ : Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p.conjExponent) 1} φ
H :
  (fun (a : ι → ℝ≥0) ↦ HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x * a x) (∑ x ∈ s, g x * a x)) φ =
    HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (f x + g x) ^ p) (1 / p)
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
have inr : (fun (a : ι → ℝ≥0) ↦ HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x * a x) (∑ x ∈ s, g x * a x)) φ ≤
  HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (1 / p)
Tactic: rw [← H]
-- 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
⊢ (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 pos : 0 < p
Tactic: have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
-- 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 ι
⊢ ∑ 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
have rw : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (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: rw [one_div, ← NNReal.rpow_inv_le_iff pos, ← one_div]
-- 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 + 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 ∈ 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)
Tactic: refine le_trans (Lp_add_le s f g hp) ?_