awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : (i : ι) → ℝ≥0
⊢ ∑ i ∈ s, (↑(w i) : ℝ) * (↑(f i) : ℝ) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, (↑(w i) : ℝ)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ) (∑ i ∈ s, (↑(w i) : ℝ) * (↑(f i) : ℝ) ^ p) p⁻¹
have 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⁻¹
Tactic: norm_cast at *
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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⁻¹
have 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⁻¹
Tactic: simp_rw [expect_eq_sum_div_card]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 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⁻¹
have 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) : ℝ)
Tactic: rw [div_rpow, div_rpow, div_mul_div_comm, ← rpow_add', sub_add_cancel, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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) : ℝ)
⊢ 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⁻¹
have hx : LE.le (α := ℝ) 0 (↑(#s) : ℝ)
Tactic: rw [div_rpow, div_rpow, div_mul_div_comm, ← rpow_add', sub_add_cancel, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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) : ℝ)
⊢ 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⁻¹
have h : 1 - p⁻¹ + p⁻¹ ≠ 0
Tactic: rw [div_rpow, div_rpow, div_mul_div_comm, ← rpow_add', sub_add_cancel, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ 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⁻¹
have hx₁ : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * f i ^ p)
Tactic: rw [div_rpow, div_rpow, div_mul_div_comm, ← rpow_add', sub_add_cancel, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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) : ℝ)
⊢ 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⁻¹
have hx₂ : LE.le (α := ℝ) 0 (∑ i ∈ s, w i)
Tactic: rw [div_rpow, div_rpow, div_mul_div_comm, ← rpow_add', sub_add_cancel, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ 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) : ℝ)
have 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⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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 * f i ^ p
have this : 0 ≤ w i
Tactic: have := hw i
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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 * f i ^ p
have this₁ : 0 ≤ f i
Tactic: have := hf i
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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 ^ q
⊢ (Summable (α := ℝ) fun (i : ι) ↦ (f i * g i) ^ r) ∧
    ∑' (i : ι), (f i * g i) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)
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) ^ r) ∧
    ∑' (i : ι), ((fun (i : ι) ↦ (↑(f i) : ℝ)) i * g i) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)
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 q r : ℝ
hpqr : p.HolderTriple q r
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ g i ^ q
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) ^ r) ∧
    ∑' (i : ι), ((fun (i : ι) ↦ (↑(f i) : ℝ)) i * g i) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)
have lift : ∀ (g : (i : ι) → ℝ≥0) (hg_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q),
  (Summable (α := ℝ) fun (i : ι) ↦
      HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ r) ∧
    ∑' (i : ι), HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (r / q)
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 q r : ℝ
hpqr : p.HolderTriple q r
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) q
⊢ (Summable (α := ℝ) fun (i : ι) ↦
      HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ r) ∧
    ∑' (i : ι), HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (r / q)
have beta_reduce : ∀ (hf_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) (g : (i : ι) → ℝ≥0)
  (hg_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(g i) : ℝ) ^ q),
  (Summable (α := ℝ) fun (i : ι) ↦ ((↑(f i) : ℝ) * (↑(g i) : ℝ)) ^ r) ∧
    ∑' (i : ι), ((↑(f i) : ℝ) * (↑(g i) : ℝ)) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), (↑(f i) : ℝ) ^ p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), (↑(g i) : ℝ) ^ q) (r / q)
Tactic: beta_reduce at *
Cleared hypotheses: hf_sum, g, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(f i) : ℝ) ^ p
g : (i : ι) → ℝ≥0
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(g i) : ℝ) ^ q
⊢ (Summable (α := ℝ) fun (i : ι) ↦ ((↑(f i) : ℝ) * (↑(g i) : ℝ)) ^ r) ∧
    ∑' (i : ι), ((↑(f i) : ℝ) * (↑(g i) : ℝ)) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), (↑(f i) : ℝ) ^ p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), (↑(g i) : ℝ) ^ q) (r / q)
have norm_cast : ∀ (hf_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ f a ^ p) (hg_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ g a ^ q),
  (Summable (α := ℝ≥0) fun (a : ι) ↦ (f a * g a) ^ r) ∧
    ∑' (a : ι), (f a * g a) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (a : ι), f a ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (a : ι), g a ^ q) (r / q)
Tactic: norm_cast at *
Cleared hypotheses: hf_sum, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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 ^ q
⊢ HPow.hPow (α := ℝ) (∑' (i : ι), (f i * g i) ^ r) (1 / r) ≤
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q)
have hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
Tactic: have hf' : 0 ≤ ∑' i, f i ^ p := tsum_nonneg fun i ↦ rpow_nonneg (hf i) p
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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 ^ q
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
⊢ HPow.hPow (α := ℝ) (∑' (i : ι), (f i * g i) ^ r) (1 / r) ≤
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q)
have hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
Tactic: have hg' : 0 ≤ ∑' i, g i ^ q := tsum_nonneg fun i ↦ rpow_nonneg (hg i) q
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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 ^ q
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
⊢ HPow.hPow (α := ℝ) (∑' (i : ι), (f i * g i) ^ r) (1 / r) ≤
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q)
have hr : 0 < r
Tactic: have hr := hpqr.pos'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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 ^ q
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
i : ι
⊢ 0 ≤ (f i * g i) ^ r
have positivity : 0 ≤ f i → 0 ≤ (f i * g i) ^ r
Tactic: positivity [hf i, hg i]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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 ^ q
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
i : ι
positivity positivity₁ positivity₂ : 0 ≤ f i → 0 ≤ (f i * g i) ^ r
⊢ 0 ≤ (f i * g i) ^ r
have positivity₃ : 0 ≤ f i → 0 ≤ g i → 0 ≤ (f i * g i) ^ r
Tactic: positivity [hf i, hg i]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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 ^ q
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
⊢ HPow.hPow (α := ℝ) (∑' (i : ι), (f i * g i) ^ r) (1 / r) ≤
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q)
have h : HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q) =
  (HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)) ^ (1 / r)
Tactic: convert!
    rpow_le_rpow_iff (tsum_nonneg fun i ↦ by positivity [hf i, hg i]) (by positivity)
          (inv_eq_one_div r ▸ inv_pos.mpr hr) |>.mpr <|
      Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum using 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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 ^ q
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
⊢ HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q) =
    (HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)) ^ (1 / r)
have h : HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q) =
  HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p * (1 / r)) *
    HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q * (1 / r))
Tactic: rw [mul_rpow (rpow_nonneg hf' _) (rpow_nonneg hg' _), ← Real.rpow_mul hg', ← Real.rpow_mul hf']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg_sum : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun (i : ι) ↦ f i * g i) C
have lift : ∀ (f : (i : ι) → ℝ≥0) (hf_sum : 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) C
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 q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
f : (i : ι) → ℝ≥0
hf_sum : 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) C
have lift : ∀ (g : (i : ι) → ℝ≥0) (hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (B ^ q)),
  ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ A * B ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
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 q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : (i : ι) → ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (A ^ p)
g : (i : ι) → ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (B ^ q)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ A * B ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
have lift : ∀ (A : ℝ≥0) (hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)),
  ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) * B ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
Tactic: lift A to ℝ≥0 using hA
Cleared hypotheses: A, hA, hf_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
B : ℝ
hB : 0 ≤ B
f g : (i : ι) → ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (B ^ q)
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) * B ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
have lift : ∀ (B : ℝ≥0) (hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) ((↑B : ℝ) ^ q)),
  ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) * (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
Tactic: lift B to ℝ≥0 using hB
Cleared hypotheses: B, hB, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) ((↑B : ℝ) ^ q)
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) * (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
have beta_reduce : ∀ (hf_sum : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)) (B : ℝ≥0)
  (hg_sum : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ q) ((↑B : ℝ) ^ q)),
  ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C
Tactic: beta_reduce at *
Cleared hypotheses: hf_sum, B, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ q) ((↑B : ℝ) ^ q)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C
have hf_sum₁ : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
Tactic: norm_cast at hf_sum hg_sum
Cleared hypotheses: hf_sum, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ q) ((↑B : ℝ) ^ q)
hf_sum₁ : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C
have hg_sum₁ : HasSum (fun (a : ι) ↦ g a ^ q) (B ^ q)
Tactic: norm_cast at hf_sum hg_sum
Cleared hypotheses: hf_sum, hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
hg_sum : HasSum (fun (a : ι) ↦ g a ^ q) (B ^ q)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C
have obtain : ∀ (C : ℝ≥0) (hC : C ≤ A * B) (H : HasSum (fun (i : ι) ↦ f i * g i) C),
  ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C
Tactic: obtain ⟨C, hC, H⟩ := NNReal.inner_le_Lp_mul_Lq_hasSum hpq hf_sum hg_sum
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
hg_sum : HasSum (fun (a : ι) ↦ g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun (i : ι) ↦ f i * g i) C
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C
have refine : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) (↑C : ℝ)
Tactic: refine ⟨C, C.prop, hC, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ i ∈ s, f i ^ p
have h : Eq (α := ℝ) (∑ i ∈ s, f i) (∑ i ∈ s, |f i|)
Tactic: convert! rpow_sum_le_const_mul_sum_rpow s f hp using 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
h : Eq (α := ℝ) (∑ i ∈ s, f i) (∑ i ∈ s, |f i|)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ i ∈ s, f i ^ p
have h₁ : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
Tactic: convert! rpow_sum_le_const_mul_sum_rpow s f hp using 2
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ Eq (α := ℝ) (∑ i ∈ s, f i) (∑ i ∈ s, |f i|)
have h : ∀ x ∈ s, f x = |f x|
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f 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
⊢ 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
-- 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₁ : HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p)
Tactic: convert! Lp_add_le s f g hp using 2
-- 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₁ : HPow.hPow (α := ℝ) (∑ i ∈ s, f i ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |f 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)
have h₂ : HPow.hPow (α := ℝ) (∑ i ∈ s, g i ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)
Tactic: convert! Lp_add_le s f g hp using 2
-- 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 ^ p) (1 / p) = HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p)
have h : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
Tactic: congr 1