English
For r ≠ 0, HolderTriple(p:q:r in ENNReal) is equivalent to NNReal.HolderTriple p q r.
Русский
При r ≠ 0 условие HolderTriple для ENNReal эквивалентно NNReal.HolderTriple p q r.
LaTeX
$$HolderTriple(p : ℝ≥0∞) (q : ℝ≥0∞) (r : ℝ≥0∞) (hr ≠ 0) ↔ NNReal.HolderTriple p q r$$
Lean4
@[simp, norm_cast]
theorem holderTriple_coe_iff {p q r : ℝ≥0} (hr : r ≠ 0) :
HolderTriple (p : ℝ≥0∞) (q : ℝ≥0∞) (r : ℝ≥0∞) ↔ NNReal.HolderTriple p q r :=
by
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rw [NNReal.holderTriple_iff]
obtain ⟨hp, hq⟩ : p ≠ 0 ∧ q ≠ 0 := by
constructor
all_goals
rintro rfl
apply hr
exact_mod_cast (coe_zero ▸ h).unique _ _ r 0
exact ⟨by exact_mod_cast h.inv_add_inv_eq_inv, hp.bot_lt, hq.bot_lt⟩
· rw [holderTriple_iff]
have hp := h.ne_zero
have hq := h.symm.ne_zero
exact_mod_cast h.inv_add_inv_eq_inv
