English
The function conjExponent defines the conjugate exponent for ENNReal: if p ≥ 1, then p.HolderConjugate (conjExponent p).
Русский
Функция conjExponent задаёт сопряжённый показатель: если p ≥ 1, то p.HolderConjugate(conjExponent p).
LaTeX
$$$p.HolderConjugate (conjExponent p)$$$
Lean4
protected theorem conjExponent {p : ℝ≥0∞} (hp : 1 ≤ p) : p.HolderConjugate (conjExponent p) :=
by
have : p ≠ 0 := (zero_lt_one.trans_le hp).ne'
rw [HolderConjugate, holderTriple_iff, conjExponent, add_comm]
refine (AddLECancellable.eq_tsub_iff_add_eq_of_le (α := ℝ≥0∞) (by simpa) (by simpa)).1 ?_
rw [inv_eq_iff_eq_inv]
obtain rfl | hp₁ := hp.eq_or_lt
· simp
obtain rfl | hp := eq_or_ne p ∞
· simp
calc
1 + (p - 1)⁻¹ = (p - 1 + 1) / (p - 1) := by
rw [ENNReal.add_div, ENNReal.div_self ((tsub_pos_of_lt hp₁).ne') (sub_ne_top hp), one_div]
_ = (1⁻¹ - p⁻¹)⁻¹ := by
rw [tsub_add_cancel_of_le, ← inv_eq_iff_eq_inv, div_eq_mul_inv, ENNReal.mul_inv, inv_inv, ENNReal.mul_sub,
ENNReal.inv_mul_cancel, mul_one] <;>
simp [*]
