awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
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₁ : HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p)
h₂ : HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |g 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)

Tactic:
convert! Lp_add_le s f g hp using 2

Premises used: Real.Lp_add_le
-- Module: Mathlib.Analysis.MeanInequalities
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 ^ p) (∑ i ∈ s, |f i| ^ p)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p)

Tactic:
congr 1
-- Module: Mathlib.Analysis.MeanInequalities
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, g i ^ p) (∑ i ∈ s, |g i| ^ p)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)

Tactic:
congr 1
-- Module: Mathlib.Analysis.MeanInequalities
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)
h₂ : Eq (α := ℝ) (∑ i ∈ s, g i ^ p) (∑ i ∈ s, |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)

Tactic:
convert! Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1]

Premises used: Real.Lp_add_le
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ x ∈ s, (f x + g x) ^ p = |f x + g x| ^ p
⊢ Eq (α := ℝ) (∑ i ∈ s, (f i + g i) ^ p) (∑ i ∈ s, |f i + g i| ^ p)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ x ∈ s, f x ^ p = |f x| ^ p
⊢ Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ x ∈ s, g x ^ p = |g x| ^ p
⊢ Eq (α := ℝ) (∑ i ∈ s, g i ^ p) (∑ i ∈ s, |g i| ^ p)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ (f i + g i) ^ p = |f i + g i| ^ p

Tactic:
simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]

Premises used: add_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p

Tactic:
simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]

Premises used: add_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i ^ p = |g i| ^ p

Tactic:
simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]

Premises used: add_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ ∀ (i : ι), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Analysis.MeanInequalities
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
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)
⊢ (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:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ ∀ (i : ι), 0 ≤ g i

Tactic:
hg
-- Module: Mathlib.Analysis.MeanInequalities
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
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)
⊢ (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 g to ι → ℝ≥0 using hg
-- Module: Mathlib.Analysis.MeanInequalities
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
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)
⊢ (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:
beta_reduce at *
-- Module: Mathlib.Analysis.MeanInequalities
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
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)
⊢ (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:
norm_cast0 at *
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p : ℝ
f g : (i : ι) → ℝ≥0
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:
NNReal.Lp_add_le_tsum hp hf_sum hg_sum

Premises used: NNReal.Lp_add_le_tsum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p : ℝ
f g : (i : ι) → ℝ≥0
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:
exact NNReal.Lp_add_le_tsum hp hf_sum hg_sum

Premises used: NNReal.Lp_add_le_tsum
-- Module: Mathlib.Analysis.MeanInequalities
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

Tactic:
(Lp_add_le_tsum_of_nonneg hp hf hg hf_sum hg_sum).1

Premises used: Real.Lp_add_le_tsum_of_nonneg, And.left
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ 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:
(Lp_add_le_tsum_of_nonneg hp hf hg hf_sum hg_sum).2

Premises used: Real.Lp_add_le_tsum_of_nonneg, And.right
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ ∀ (i : ι), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)

Tactic:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ ∀ (i : ι), 0 ≤ g i

Tactic:
hg
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun (i : ι) ↦ ((fun (i : ι) ↦ (↑(f i) : ℝ)) i + g i) ^ p) (C ^ p)

Tactic:
lift g to ι → ℝ≥0 using hg
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ 0 ≤ A

Tactic:
hA
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∃ (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
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ 0 ≤ B

Tactic:
hB
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∃ (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
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∃ (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
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)

Tactic:
norm_cast at hfA hgB
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ HasSum (fun (a : ι) ↦ g a ^ p) (B ^ p)

Tactic:
norm_cast at hfA hgB
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∃ (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

Premises used: NNReal.Lp_add_le_hasSum
-- Module: Mathlib.Analysis.MeanInequalities
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)
h :
  0 ≤ (↑C : ℝ) ∧
    (↑C : ℝ) ≤ (↑A : ℝ) + (↑B : ℝ) ∧
      HasSum (fun (i : ι) ↦ HAdd.hAdd (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) 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:
use C
-- Module: Mathlib.Analysis.MeanInequalities
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)
h : 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun (a : ι) ↦ (f a + g a) ^ p) (C ^ p)
⊢ 0 ≤ (↑C : ℝ) ∧
    (↑C : ℝ) ≤ (↑A : ℝ) + (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ ((↑(f i) : ℝ) + (↑(g i) : ℝ)) ^ p) ((↑C : ℝ) ^ p)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.MeanInequalities
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 (a : ι) ↦ (f a + g a) ^ p) (C ^ p)

Tactic:
⟨zero_le, hC₁, hC₂⟩

Premises used: zero_le, And.intro
-- Module: Mathlib.Analysis.MeanInequalities
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 (a : ι) ↦ (f a + g a) ^ p) (C ^ p)

Tactic:
exact ⟨zero_le, hC₁, hC₂⟩
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∑ 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

Premises used: HDiv.hDiv, HPow.hPow, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.MeanInequalities
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 = 0) ∨ ∀ i ∈ s, g i = 0

Tactic:
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

Premises used: ENNReal.rpow_eq_zero_iff, asymm, Finset.sum_eq_zero_iff_of_nonneg, Real.HolderConjugate.symm, Real.HolderTriple.pos
-- Module: Mathlib.Analysis.MeanInequalities
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 = 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
-- Module: Mathlib.Analysis.MeanInequalities
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
inr : ∀ (H : ∀ i ∈ s, g i = 0), f i * g i = 0
⊢ f i * g i = 0

Tactic:
rcases H with H | H
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
i : ι
hi : i ∈ s
H : ∀ i ∈ s, f i = 0
⊢ f i * g i = 0

Tactic:
simp [H i hi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
i : ι
hi : i ∈ s
H : ∀ i ∈ s, g i = 0
⊢ f i * g i = 0

Tactic:
simp [H i hi]
-- Module: Mathlib.Analysis.MeanInequalities
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 = 0

Tactic:
have : ∀ i ∈ s, f i * g i = 0 := fun i hi => by rcases H with H | H <;> simp [H i hi]
-- Module: Mathlib.Analysis.MeanInequalities
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
this : ∀ i ∈ s, f i * 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)

Tactic:
simp [sum_eq_zero this]

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∑ 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'
-- Module: Mathlib.Analysis.MeanInequalities
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) = ∞
⊢ ∑ 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:
simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]

Premises used: ENNReal.rpow_eq_zero_iff, one_div, Finset.sum_eq_zero_iff