-- Mathlib/Analysis/MeanInequalities.lean
theorem isGreatest_Lp (f : ι → ℝ≥0) {p q : ℝ} (hpq : p.IsConjExponent q) :
    IsGreatest ((fun g : ι → ℝ≥0 => ∑ i ∈ s, f i * g i) '' { g | ∑ i ∈ s, g i ^ q ≤ 1 })
      ((∑ i ∈ s, f i ^ p) ^ (1 / p))

Proof state:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
simp only [Set.mem_setOf_eq, div_rpow, ← sum_div, ← rpow_mul,
  div_mul_cancel₀ _ hpq.symm.ne_zero, rpow_one, div_le_iff₀ hf, one_mul, hpq.mul_eq_add, ←
  rpow_sub' A, add_sub_cancel_right, le_refl, true_and, ← mul_div_assoc, B]

Result:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) / (∑ i ∈ s, f i ^ p) ^ (1 / q) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Proof state:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
y : ℝ≥0
h : y = 0
⊢ y ^ p = 0

Tactic:
simp [h, hpq.ne_zero]

Result:
no goals

Proof state:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
have A : p + q - q ≠ 0 := by simp [hpq.ne_zero]

Result:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Proof state:
case left
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ (fun g => ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}

Tactic:
use fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)

Result:
case h
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Proof state:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
⊢ ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p

Tactic:
refine fun y => mul_div_cancel_left_of_imp fun h => ?_

Result:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
y : ℝ≥0
h : y = 0
⊢ y ^ p = 0

Proof state:
case right.intro.intro
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
g : ι → ℝ≥0
hg : g ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1}
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
simpa only [mul_one] using
  mul_le_mul_left' (NNReal.rpow_le_one hg (le_of_lt hpq.symm.one_div_pos)) _

Result:
no goals

Proof state:
case h.inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
simp [hf, hpq.ne_zero, hpq.symm.ne_zero]

Result:
no goals

Proof state:
case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g => ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})

Tactic:
rintro _ ⟨g, hg, rfl⟩

Result:
case right.intro.intro
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
g : ι → ℝ≥0
hg : g ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1}
⊢ (fun g => ∑ i ∈ s, f i * g i) g ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p)

Proof state:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
⊢ p + q - q ≠ 0

Tactic:
simp [hpq.ne_zero]

Result:
no goals

Proof state:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0

Tactic:
simpa [hpq.symm.ne_zero] using hf.ne'

Result:
no goals

Proof state:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
have B : ∀ y : ℝ≥0, y * y ^ p / y = y ^ p := by
  refine fun y => mul_div_cancel_left_of_imp fun h => ?_
  simp [h, hpq.ne_zero]

Result:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Proof state:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
⊢ IsGreatest ((fun g => ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}) ((∑ i ∈ s, f i ^ p) ^ (1 / p))

Tactic:
constructor

Result:
case left
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ (fun g => ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1}

case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g => ∑ i ∈ s, f i * g i) '' {g | ∑ i ∈ s, g i ^ q ≤ 1})

Proof state:
case h
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)

Result:
case h.inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
⊢ (fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i ∈ s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i ∈ s, f i * g i) fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Proof state:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) / (∑ i ∈ s, f i ^ p) ^ (1 / q) = (∑ i ∈ s, f i ^ p) ^ (1 / p)

Tactic:
rw [div_eq_iff, ← rpow_add hf.ne', one_div, one_div, hpq.inv_add_inv_conj, rpow_one]

Result:
case h.inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : 0 < ∑ i ∈ s, f i ^ p
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / q) ≠ 0