awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
rw : B = (B ^ p) ^ (1 / p)
rw₁ rw₂ : B = B
⊢ B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)

Tactic:
rw [hg.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)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
⊢ B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)

Tactic:
have hB : B = (∑' i : ι, g i ^ p) ^ (1 / p) := by rw [hg.tsum_eq, rpow_inv_rpow_self hp']
-- 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)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)

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

Premises used: HDiv.hDiv, HPow.hPow, HAdd.hAdd, tsum, And.intro, Exists.intro, OfNat.ofNat, SummationFilter.unconditional
-- 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)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
refine_1 : HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤ A + B
refine_2 : HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ^ p)
⊢ ∃ C ≤ A + B, HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (C ^ p)

Tactic:
refine ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), ?_, ?_⟩
-- 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)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
⊢ HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ≤ A + B

Tactic:
simpa [hA, hB] using H₂
-- 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)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ p) (1 / p)
⊢ HasSum (fun (i : ι) ↦ (f i + g i) ^ p) (HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i + g i) ^ p) (1 / p) ^ p)

Tactic:
simpa only [rpow_self_rpow_inv hp'] using H₁.hasSum

Premises used: Summable.hasSum, NNReal.rpow_self_rpow_inv
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ ∑ i ∈ s, |f i * g i| ^ r ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (r / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ q) (r / q)

Tactic:
simpa using NNReal.coe_le_coe.2 <| NNReal.Lr_rpow_le_Lp_mul_Lq s (fun i ↦ ⟨_, abs_nonneg (f i)⟩)
    (fun i ↦ ⟨_, abs_nonneg (g i)⟩) hpqr

Premises used: Iff.mpr, abs, Subtype.mk, NNReal.Lr_rpow_le_Lp_mul_Lq, abs_nonneg, NNReal.coe_le_coe
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
⊢ ∑ i ∈ s, |f i| * |g i| ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ q) (1 / q)

Tactic:
simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq

Premises used: Real.Lr_rpow_le_Lp_mul_Lq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
refine : ∀ i ∈ s, f i * g i ≤ |f i| * |g i|
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ q) (1 / q)

Tactic:
refine le_trans (sum_le_sum fun i _ ↦ ?_) (by simpa using Lr_rpow_le_Lp_mul_Lq s f g hpq)

Premises used: Finset.sum_le_sum, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
i : ι
h : i ∈ s
⊢ f i * g i ≤ |f i| * |g i|

Tactic:
simp only [← abs_mul, le_abs_self]

Premises used: le_abs_self, abs_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
⊢ (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) i) p) : ℝ) ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) *
          ∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) i) p) :
      ℝ)

Tactic:
have :=
    NNReal.coe_le_coe.2
      (NNReal.rpow_sum_le_const_mul_sum_rpow s (fun i => ⟨_, abs_nonneg (f i)⟩) hp)
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) i) p) : ℝ) ≤
    (↑(HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) *
          ∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) i) p) :
      ℝ)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) : ℝ)) p ≤
    HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ x ∈ s, (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f x| ⋯) : ℝ) ^ p

Tactic:
push_cast at this
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ i ∈ s, (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) : ℝ)) p ≤
    HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ x ∈ s, (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f x| ⋯) : ℝ) ^ p
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i|) p ≤ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ i ∈ s, |f i| ^ p

Tactic:
this

Premises used: abs, NNReal.toReal
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ i ∈ s, (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f i| ⋯) : ℝ)) p ≤
    HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ x ∈ s, (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) |f x| ⋯) : ℝ) ^ p
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i|) p ≤ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ i ∈ s, |f i| ^ p

Tactic:
exact this
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
⊢ (↑(HPow.hPow (α := ℝ≥0)
          (∑ i ∈ s,
            HAdd.hAdd (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |f i| ⋯) i) ((fun (i : ι) ↦ NNReal.mk |g i| ⋯) i) ^ p)
          (1 / p)) :
      ℝ) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |f i| ⋯) i) p) (1 / p) +
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |g i| ⋯) i) p) (1 / p)) :
      ℝ)

Tactic:
have := NNReal.coe_le_coe.2
    (NNReal.Lp_add_le s (fun i => .mk _ (abs_nonneg (f i))) (fun i => .mk _ (abs_nonneg (g i))) hp)
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  (↑(HPow.hPow (α := ℝ≥0)
          (∑ i ∈ s,
            HAdd.hAdd (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |f i| ⋯) i) ((fun (i : ι) ↦ NNReal.mk |g i| ⋯) i) ^ p)
          (1 / p)) :
      ℝ) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |f i| ⋯) i) p) (1 / p) +
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ NNReal.mk |g i| ⋯) i) p) (1 / p)) :
      ℝ)
⊢ HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)

Tactic:
push_cast at this
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i + g i| ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)

Tactic:
le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this

Premises used: Real.rpow_le_rpow, Finset.sum_le_sum, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
refine_1 : LE.le (α := ℝ) 0 (∑ i ∈ s, |f i + g i| ^ p)
refine_2 : ∀ i ∈ s, |f i + g i| ^ p ≤ (|f i| + |g i|) ^ p
refine_3 : 0 ≤ 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:
refine le_trans (rpow_le_rpow ?_ (sum_le_sum fun i _ => ?_) ?_) this

Premises used: Real.rpow_le_rpow, Finset.sum_le_sum, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, |f i + g i| ^ p)

Tactic:
simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add_le,
      rpow_le_rpow]

Premises used: Finset.sum_nonneg, zero_le_one, Real.rpow_le_rpow, Real.rpow_nonneg, abs_add_le, abs_nonneg, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
i : ι
h : i ∈ s
⊢ |f i + g i| ^ p ≤ (|f i| + |g i|) ^ p

Tactic:
simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add_le,
      rpow_le_rpow]

Premises used: Finset.sum_nonneg, zero_le_one, Real.rpow_le_rpow, Real.rpow_nonneg, abs_add_le, abs_nonneg, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
this :
  HPow.hPow (α := ℝ) (∑ x ∈ s, (|f x| + |g x|) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ x ∈ s, |f x| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ x ∈ s, |g x| ^ p) (1 / p)
⊢ 0 ≤ 1 / p

Tactic:
simp [sum_nonneg, rpow_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add_le,
      rpow_le_rpow]

Premises used: Finset.sum_nonneg, zero_le_one, Real.rpow_le_rpow, Real.rpow_nonneg, abs_add_le, abs_nonneg, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ q) (1 / q)

Tactic:
inner_le_Lp_mul_Lq s f g hpq

Premises used: Real.inner_le_Lp_mul_Lq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
h₁ : Eq (α := ℝ) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, |g i| ^ q)
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
convert! inner_le_Lp_mul_Lq s f g hpq using 3

Premises used: Real.inner_le_Lp_mul_Lq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ 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 q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ x ∈ s, g x ^ q = |g x| ^ q
⊢ Eq (α := ℝ) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, |g i| ^ q)

Tactic:
apply sum_congr rfl

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

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

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

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

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ ∑ i ∈ s, |f i * g i| ^ r ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (r / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ q) (r / q)

Tactic:
Lr_rpow_le_Lp_mul_Lq s f g hpqr

Premises used: Real.Lr_rpow_le_Lp_mul_Lq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ (i : ι) (hi : i ∈ s), f i * g i = |f i * g i|
h₁ : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
h₂ : Eq (α := ℝ) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, |g i| ^ q)
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ q) (r / q)

Tactic:
convert! Lr_rpow_le_Lp_mul_Lq s f g hpqr using 3 with i hi

Premises used: Real.Lr_rpow_le_Lp_mul_Lq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
h h₁ : f i * g i = f i * g i
⊢ f i * g i = |f i * g i|

Tactic:
rw [abs_of_nonneg (mul_nonneg (hf i hi) (hg i hi))]

Premises used: mul_nonneg, abs_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ (i : ι) (hi : i ∈ s), f i = |f i|
⊢ Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)

Tactic:
congr! with i hi
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ 0 ≤ f i

Tactic:
grind
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i = |f i|

Tactic:
exact Eq.symm (abs_of_nonneg (by grind))

Premises used: abs_of_nonneg, Eq.symm
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
h : ∀ (i : ι) (hi : i ∈ s), g i = |g i|
⊢ Eq (α := ℝ) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, |g i| ^ q)

Tactic:
congr! with i hi
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ 0 ≤ g i

Tactic:
grind
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i = |g i|

Tactic:
exact Eq.symm (abs_of_nonneg (by grind))

Premises used: abs_of_nonneg, Eq.symm
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∀ (i : ι), 0 ≤ w i

Tactic:
hw
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
lift :
  ∀ (w : (i : ι) → ℝ≥0),
    ∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * f i ≤
      HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i) (1 - p⁻¹) *
        HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * f i ^ p) p⁻¹
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
lift w to ι → ℝ≥0 using hw
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
w : (i : ι) → ℝ≥0
⊢ ∀ (i : ι), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
w : (i : ι) → ℝ≥0
lift :
  ∀ (f : (i : ι) → ℝ≥0),
    ∑ i ∈ s, HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(w i) : ℝ)) i) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ≤
      HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i) (1 - p⁻¹) *
        HPow.hPow (α := ℝ)
          (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) p⁻¹
⊢ ∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * f i ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i) (1 - p⁻¹) *
      HPow.hPow (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ (↑(w i) : ℝ)) i * f i ^ p) p⁻¹

Tactic:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : (i : ι) → ℝ≥0
norm_cast :
  ∀ (hp : 1 ≤ p),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ ∑ i ∈ s, (↑(w i) : ℝ) * (↑(f i) : ℝ) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, (↑(w i) : ℝ)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ) (∑ i ∈ s, (↑(w i) : ℝ) * (↑(f i) : ℝ) ^ p) p⁻¹

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
w f : (i : ι) → ℝ≥0
hp : 1 ≤ p
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
NNReal.inner_le_weight_mul_Lp _ hp _ _

Premises used: NNReal.inner_le_weight_mul_Lp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
w f : (i : ι) → ℝ≥0
hp : 1 ≤ p
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
exact NNReal.inner_le_weight_mul_Lp _ hp _ _

Premises used: NNReal.inner_le_weight_mul_Lp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
simp_rw :
  HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * f i) (↑(#s) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (↑(#s) : ℝ) ^ (1 - p⁻¹) *
      HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * f i ^ p) (↑(#s) : ℝ) ^ p⁻¹
⊢ 𝔼 i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ) (𝔼 i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ) (𝔼 i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
simp_rw [expect_eq_sum_div_card]

Premises used: Finset.expect_eq_sum_div_card
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
rw :
  HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * f i) (↑(#s) : ℝ) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ) (∑ i ∈ s, w i * f i ^ p) p⁻¹ / (↑(#s) : ℝ)
hx : LE.le (α := ℝ) 0 (↑(#s) : ℝ)
h : 1 - p⁻¹ + p⁻¹ ≠ 0
hx₁ : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * f i ^ p)
hy : LE.le (α := ℝ) 0 (↑(#s) : ℝ)
hx₂ : LE.le (α := ℝ) 0 (∑ i ∈ s, w i)
hy₁ : LE.le (α := ℝ) 0 (↑(#s) : ℝ)
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * f i) (↑(#s) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (↑(#s) : ℝ) ^ (1 - p⁻¹) *
      HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * f i ^ p) (↑(#s) : ℝ) ^ p⁻¹

Tactic:
rw [div_rpow, div_rpow, div_mul_div_comm, ← rpow_add', sub_add_cancel, rpow_one]

Premises used: div_mul_div_comm, Real.div_rpow, Real.rpow_one, Real.rpow_add', sub_add_cancel
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
hab : ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * f i) (↑(#s) : ℝ) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ) (∑ i ∈ s, w i * f i ^ p) p⁻¹ / (↑(#s) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
inner_le_weight_mul_Lp_of_nonneg s hp _ _ hw hf

Premises used: Real.inner_le_weight_mul_Lp_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
exact inner_le_weight_mul_Lp_of_nonneg s hp _ _ hw hf

Premises used: Real.inner_le_weight_mul_Lp_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ LE.le (α := ℝ) 0 (↑(#s) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 1 - p⁻¹ + p⁻¹ ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
i : ι
h : i ∈ s
⊢ 0 ≤ w i

Tactic:
have := hw i
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
i : ι
h : i ∈ s
this : 0 ≤ w i
⊢ 0 ≤ f i

Tactic:
have := hf i
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
i : ι
h : i ∈ s
this_1 : 0 ≤ w i
this : 0 ≤ f i
⊢ 0 ≤ w i * f i ^ p

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, w i * f i ^ p)

Tactic:
exact sum_nonneg fun i _ ↦ by have := hw i; have := hf i; positivity

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
i : ι
h : i ∈ s
this : 0 ≤ w i
⊢ 0 ≤ w i

Tactic:
positivity