awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ 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:
simpa only [mul_one] using
      mul_le_mul_right (NNReal.rpow_le_one hg (le_of_lt hpq.symm.one_div_pos)) _

Premises used: le_of_lt, mul_le_mul_right, Real.HolderConjugate.symm, NNReal.rpow_le_one, Real.HolderTriple.one_div_pos, mul_one
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ 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)

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
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:
simp [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
⊢ p.HolderConjugate p.conjExponent

Tactic:
have hpq := Real.HolderConjugate.conjExponent hp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
hpq : p.HolderConjugate p.conjExponent
⊢ 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
-- Module: Mathlib.Analysis.MeanInequalities
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))
⊢ 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

Premises used: add_mul, Finset.sum_add_distrib, Pi.add_apply
-- Module: Mathlib.Analysis.MeanInequalities
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))
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)
⊢ 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⟩

Premises used: And.left
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ 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:
rw [← H]
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ (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:
add_le_add ((isGreatest_Lp s f hpq).2 ⟨φ, hφ, rfl⟩) ((isGreatest_Lp s g hpq).2 ⟨φ, hφ, rfl⟩)

Premises used: add_le_add, NNReal.isGreatest_Lp, And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ (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:
exact add_le_add ((isGreatest_Lp s f hpq).2 ⟨φ, hφ, rfl⟩) ((isGreatest_Lp s g hpq).2 ⟨φ, hφ, rfl⟩)

Premises used: add_le_add, NNReal.isGreatest_Lp, And.right, And.intro, Exists.intro, rfl
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ 0 < p

Tactic:
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
-- Module: Mathlib.Analysis.MeanInequalities
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 ι
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)
⊢ ∑ 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:
rw [one_div, ← NNReal.rpow_inv_le_iff pos, ← one_div]

Premises used: NNReal.rpow_inv_le_iff, one_div
-- Module: Mathlib.Analysis.MeanInequalities
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)

Tactic:
le_trans (Lp_add_le s f g hp) ?_

Premises used: NNReal.Lp_add_le, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
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 ι
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)
⊢ 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:
refine le_trans (Lp_add_le s f g hp) ?_

Premises used: NNReal.Lp_add_le, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
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)
h₂ : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (∑' (i : ι), g 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)

Tactic:
gcongr
-- Module: Mathlib.Analysis.MeanInequalities
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 ι
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑' (i : ι), f i ^ p)

Tactic:
Summable.sum_le_tsum _ (fun _ _ ↦ zero_le) ?_

Premises used: zero_le, Summable.sum_le_tsum
-- Module: Mathlib.Analysis.MeanInequalities
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₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑' (i : ι), f i ^ p)

Tactic:
refine Summable.sum_le_tsum _ (fun _ _ ↦ zero_le) ?_

Premises used: zero_le, Summable.sum_le_tsum
-- Module: Mathlib.Analysis.MeanInequalities
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 ι
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (∑' (i : ι), g i ^ p)

Tactic:
Summable.sum_le_tsum _ (fun _ _ ↦ zero_le) ?_

Premises used: zero_le, Summable.sum_le_tsum
-- Module: Mathlib.Analysis.MeanInequalities
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₂ : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ p) (∑' (i : ι), g i ^ p)

Tactic:
refine Summable.sum_le_tsum _ (fun _ _ ↦ zero_le) ?_

Premises used: zero_le, Summable.sum_le_tsum
-- Module: Mathlib.Analysis.MeanInequalities
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 ι
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p

Tactic:
hf
-- Module: Mathlib.Analysis.MeanInequalities
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 ι
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ p

Tactic:
hg
-- Module: Mathlib.Analysis.MeanInequalities
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 ι
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p

Tactic:
exacts [hf, hg]
-- Module: Mathlib.Analysis.MeanInequalities
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

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]
-- Module: Mathlib.Analysis.MeanInequalities
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)

Tactic:
⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, ?_⟩

Premises used: HDiv.hDiv, BddAbove, Set.Nonempty, HPow.hPow, HAdd.hAdd, tsum, Exists.intro, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.Analysis.MeanInequalities
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
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)
⊢ BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i + g i) ^ p)

Tactic:
refine ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, ?_⟩
-- Module: Mathlib.Analysis.MeanInequalities
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
s : Finset ι
⊢ (fun (s : Finset ι) ↦ (∑ i ∈ s, (f i + g i) ^ p : ℝ≥0)) s ≤
    (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p

Tactic:
H₁ s
-- Module: Mathlib.Analysis.MeanInequalities
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
s : Finset ι
⊢ (fun (s : Finset ι) ↦ (∑ i ∈ s, (f i + g i) ^ p : ℝ≥0)) s ≤
    (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)) ^ p

Tactic:
exact H₁ s
-- Module: Mathlib.Analysis.MeanInequalities
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)

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
-- Module: Mathlib.Analysis.MeanInequalities
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

Tactic:
have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable
-- Module: Mathlib.Analysis.MeanInequalities
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)

Tactic:
⟨H₂, ?_⟩

Premises used: And.intro
-- Module: Mathlib.Analysis.MeanInequalities
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
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)
⊢ (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)

Tactic:
refine ⟨H₂, ?_⟩
-- Module: Mathlib.Analysis.MeanInequalities
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
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
⊢ 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:
rw [one_div, NNReal.rpow_inv_le_iff pos, ← one_div]

Premises used: NNReal.rpow_inv_le_iff, one_div
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ ∑' (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:
H₂.tsum_le_of_sum_le H₁

Premises used: Summable.tsum_le_of_sum_le
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ ∑' (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:
exact H₂.tsum_le_of_sum_le H₁

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

Tactic:
(Lp_add_le_tsum hp hf hg).1

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

Premises used: And.right, NNReal.Lp_add_le_tsum
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ p ≠ 0

Tactic:
have hp' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp).ne'
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ (f i + g i) ^ p

Tactic:
obtain ⟨H₁, H₂⟩ := Lp_add_le_tsum hp hf.summable hg.summable

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

Premises used: HasSum.summable, NNReal.Lp_add_le_tsum
-- Module: Mathlib.Analysis.MeanInequalities
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)
rw₁ rw₂ : A = A
⊢ A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)

Tactic:
rw [hf.tsum_eq, rpow_inv_rpow_self hp']

Premises used: NNReal.rpow_inv_rpow_self, HasSum.tsum_eq
-- Module: Mathlib.Analysis.MeanInequalities
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)

Tactic:
have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hp']