awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)
have h : Eq (α := ℝ) (∑ i ∈ s, g i ^ p) (∑ i ∈ s, |g i| ^ p)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ 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 h : Eq (α := ℝ) (∑ i ∈ s, (f i + g i) ^ p) (∑ i ∈ s, |f i + g i| ^ p)
Tactic: convert! Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : Eq (α := ℝ) (∑ i ∈ s, (f i + g i) ^ p) (∑ 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 h₁ : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
Tactic: convert! Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : Eq (α := ℝ) (∑ i ∈ s, (f i + g i) ^ p) (∑ i ∈ s, |f i + g i| ^ p)
h₁ : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f 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 h₂ : Eq (α := ℝ) (∑ i ∈ s, g i ^ p) (∑ i ∈ s, |g i| ^ p)
Tactic: convert! Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ Eq (α := ℝ) (∑ i ∈ s, (f i + g i) ^ p) (∑ i ∈ s, |f i + g i| ^ p)
have h : ∀ x ∈ s, (f x + g x) ^ p = |f x + g x| ^ p
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
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 : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ Eq (α := ℝ) (∑ i ∈ s, g i ^ p) (∑ i ∈ s, |g i| ^ p)
have h : ∀ x ∈ s, g x ^ p = |g x| ^ p
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ f i ^ p
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ g i ^ p
⊢ (Summable (α := ℝ) fun (i : ι) ↦ (f i + g i) ^ p) ∧
    HPow.hPow (α := ℝ) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ p) (1 / p)
have lift : ∀ (f : (i : ι) → ℝ≥0) (hf_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p),
  (Summable (α := ℝ) fun (i : ι) ↦ ((fun (i : ι) ↦ (↑(f i) : ℝ)) i + g i) ^ p) ∧
    HPow.hPow (α := ℝ) (∑' (i : ι), ((fun (i : ι) ↦ (↑(f i) : ℝ)) i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (1 / p) +
        HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ p) (1 / p)
Tactic: lift f to ι → ℝ≥0 using hf
Cleared hypotheses: f, hf, hf_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ g i ^ p
f : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p
⊢ (Summable (α := ℝ) fun (i : ι) ↦ ((fun (i : ι) ↦ (↑(f i) : ℝ)) i + g i) ^ p) ∧
    HPow.hPow (α := ℝ) (∑' (i : ι), ((fun (i : ι) ↦ (↑(f i) : ℝ)) i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (1 / p) +
        HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ p) (1 / p)
have lift : ∀ (g : (i : ι) → ℝ≥0) (hg_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p),
  (Summable (α := ℝ) fun (i : ι) ↦
      HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p) ∧
    HPow.hPow (α := ℝ)
        (∑' (i : ι), HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (1 / p) +
        HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p) (1 / p)
Tactic: lift g to ι → ℝ≥0 using hg
Cleared hypotheses: g, hg, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
f : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p
g : (i : ι) → ℝ≥0
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p
⊢ (Summable (α := ℝ) fun (i : ι) ↦
      HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p) ∧
    HPow.hPow (α := ℝ)
        (∑' (i : ι), HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (1 / p) +
        HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p) (1 / p)
have beta_reduce : ∀ (hf_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) (g : (i : ι) → ℝ≥0)
  (hg_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(g i) : ℝ) ^ p),
  (Summable (α := ℝ) fun (i : ι) ↦ ((↑(f i) : ℝ) + (↑(g i) : ℝ)) ^ p) ∧
    HPow.hPow (α := ℝ) (∑' (i : ι), ((↑(f i) : ℝ) + (↑(g i) : ℝ)) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), (↑(f i) : ℝ) ^ p) (1 / p) +
        HPow.hPow (α := ℝ) (∑' (i : ι), (↑(g i) : ℝ) ^ p) (1 / p)
Tactic: beta_reduce at *
Cleared hypotheses: hf_sum, g, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
f : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(f i) : ℝ) ^ p
g : (i : ι) → ℝ≥0
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(g i) : ℝ) ^ p
⊢ (Summable (α := ℝ) fun (i : ι) ↦ ((↑(f i) : ℝ) + (↑(g i) : ℝ)) ^ p) ∧
    HPow.hPow (α := ℝ) (∑' (i : ι), ((↑(f i) : ℝ) + (↑(g i) : ℝ)) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), (↑(f i) : ℝ) ^ p) (1 / p) +
        HPow.hPow (α := ℝ) (∑' (i : ι), (↑(g i) : ℝ) ^ p) (1 / p)
have norm_cast0 : ∀ (hp : 1 ≤ p) (hf_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ f a ^ p)
  (hg_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ g a ^ p),
  (Summable (α := ℝ≥0) fun (a : ι) ↦ (f a + g a) ^ p) ∧
    HPow.hPow (α := ℝ≥0) (∑' (a : ι), (f a + g a) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0) (∑' (a : ι), f a ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (a : ι), g a ^ p) (1 / p)
Tactic: norm_cast0 at *
Cleared hypotheses: hp, hf_sum, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hfA : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hgB : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
have lift : ∀ (f : (i : ι) → ℝ≥0) (hfA : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (A ^ p)),
  ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun (i : ι) ↦ ((fun (i : ι) ↦ (↑(f i) : ℝ)) i + g i) ^ p) (C ^ p)
Tactic: lift f to ι → ℝ≥0 using hf
Cleared hypotheses: f, hf, hfA
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hgB : HasSum (fun (i : ι) ↦ g i ^ p) (B ^ p)
f : (i : ι) → ℝ≥0
hfA : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (A ^ p)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun (i : ι) ↦ ((fun (i : ι) ↦ (↑(f i) : ℝ)) i + g i) ^ p) (C ^ p)
have lift : ∀ (g : (i : ι) → ℝ≥0) (hgB : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p) (B ^ p)),
  ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ A + B ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
Tactic: lift g to ι → ℝ≥0 using hg
Cleared hypotheses: g, hg, hgB
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : (i : ι) → ℝ≥0
hfA : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (A ^ p)
g : (i : ι) → ℝ≥0
hgB : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p) (B ^ p)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ A + B ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
have lift : ∀ (A : ℝ≥0) (hfA : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)),
  ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + B ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
Tactic: lift A to ℝ≥0 using hA
Cleared hypotheses: A, hA, hfA
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
B : ℝ
hB : 0 ≤ B
f g : (i : ι) → ℝ≥0
hgB : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p) (B ^ p)
A : ℝ≥0
hfA : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + B ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
have lift : ∀ (B : ℝ≥0) (hgB : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p) ((↑B : ℝ) ^ p)),
  ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
Tactic: lift B to ℝ≥0 using hB
Cleared hypotheses: B, hB, hgB
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hgB : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) p) ((↑B : ℝ) ^ p)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
have beta_reduce : ∀ (hfA : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)) (B : ℝ≥0)
  (hgB : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ p) ((↑B : ℝ) ^ p)),
  ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
Tactic: beta_reduce at hfA hgB
Cleared hypotheses: hfA, B, hgB
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hgB : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ p) ((↑B : ℝ) ^ p)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
have hfA₁ : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
Tactic: norm_cast at hfA hgB
Cleared hypotheses: hfA, hgB
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hgB : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ p) ((↑B : ℝ) ^ p)
hfA₁ : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
have hgB₁ : HasSum (fun (a : ι) ↦ g a ^ p) (B ^ p)
Tactic: norm_cast at hfA hgB
Cleared hypotheses: hfA, hgB
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : (i : ι) → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
hgB : HasSum (fun (a : ι) ↦ g a ^ p) (B ^ p)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
have obtain : ∀ (C : ℝ≥0) (hC₁ : C ≤ A + B) (hC₂ : HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)),
  ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
Tactic: obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : (i : ι) → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
hgB : HasSum (fun (a : ι) ↦ g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) + (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
          (C ^ p)
have h : 0 ≤ (↑C : ℝ) ∧
  (↑C : ℝ) ≤ (↑A : ℝ) + (↑B : ℝ) ∧
    HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ p)
      ((↑C : ℝ) ^ p)
Tactic: use C
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : (i : ι) → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
hgB : HasSum (fun (a : ι) ↦ g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ (↑C : ℝ) ∧
    (↑C : ℝ) ≤ (↑A : ℝ) + (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ ((↑(f i) : ℝ) + (↑(g i) : ℝ)) ^ p) ((↑C : ℝ) ^ p)
have h : 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun (a : ι) ↦ (f a + g a) ^ p) (C ^ p)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have pos : ∀ (H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = 0 ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = 0),
  ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: by_cases! H : (∑ i ∈ s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
pos :
  ∀ (H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = 0 ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = 0),
    ∑ i ∈ s, f i * g i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have neg : ∀ (H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0),
  ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: by_cases! H : (∑ i ∈ s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i ∈ s, g i ^ q) ^ (1 / q) = 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = 0 ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = 0
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have H₁ : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0
Tactic: replace H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0 := by
      simpa [ENNReal.rpow_eq_zero_iff, hpq.pos, hpq.symm.pos, asymm hpq.pos, asymm hpq.symm.pos,
        sum_eq_zero_iff_of_nonneg] using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0
i : ι
hi : i ∈ s
⊢ f i * g i = 0
have inl : ∀ (H : ∀ i ∈ s, f i = 0), f i * g i = 0
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0
i : ι
hi : i ∈ s
inl : ∀ (H : ∀ i ∈ s, f i = 0), f i * g i = 0
⊢ f i * g i = 0
have inr : ∀ (H : ∀ i ∈ s, g i = 0), f i * g i = 0
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have this : ∀ i ∈ s, f i * g i = 0
Tactic: have : ∀ i ∈ s, f i * g i = 0 := fun i hi => by rcases H with H | H <;> simp [H i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = ∞
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have pos : ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞),
  ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: rcases H' with H' | H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = ∞
pos :
  ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞),
    ∑ i ∈ s, f i * g i ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have pos₁ : ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = ∞),
  ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: rcases H' with H' | H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) = ∞)
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have H'₁ : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
Tactic: replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤ := by
    simpa [ENNReal.rpow_eq_top_iff, asymm hpq.pos, asymm hpq.symm.pos, hpq.pos, hpq.symm.pos,
      ENNReal.sum_eq_top, not_or] using H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have this : (↑(∑ i ∈ s, HMul.hMul (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) ((fun (i : ι) ↦ (g i).toNNReal) i)) : ℝ≥0∞) ≤
  (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) p) (1 / p) *
        HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (g i).toNNReal) i) q) (1 / q)) :
    ℝ≥0∞)
Tactic: have := ENNReal.coe_le_coe.2 (@NNReal.inner_le_Lp_mul_Lq _ s (fun i => ENNReal.toNNReal (f i))
    (fun i => ENNReal.toNNReal (g i)) _ _ hpq)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  (↑(∑ i ∈ s, HMul.hMul (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) ((fun (i : ι) ↦ (g i).toNNReal) i)) : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) p) (1 / p) *
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (g i).toNNReal) i) q) (1 / q)) :
      ℝ≥0∞)
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have this₁ : ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
  HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
Tactic: simp [ENNReal.coe_rpow_of_nonneg, hpq.pos.le, hpq.symm.pos.le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q) ≠ 0
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  ∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) p⁻¹ *
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ q) q⁻¹
⊢ ∑ i ∈ s, f i * g i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ q) (1 / q)
have h : Eq (α := ℝ≥0∞) (∑ i ∈ s, f i * g i) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) * (↑(g x).toNNReal : ℝ≥0∞))
Tactic: convert! this using 1