English
From MemHolder r f, one obtains HolderWith (nnHolderNorm r f) r f.
Русский
Из MemHolder r f следует HolderWith (nnHolderNorm r f) r f.
LaTeX
$$$\operatorname{MemHolder}(r,f) \Rightarrow \operatorname{HolderWith}(\mathrm{nnHolderNorm}(r,f), r, f).$$$
Lean4
theorem holderWith {r : ℝ≥0} {f : X → Y} (hf : MemHolder r f) : HolderWith (nnHolderNorm r f) r f :=
by
intro x₁ x₂
by_cases hx : x₁ = x₂
· simp only [hx, edist_self, zero_le]
rw [nnHolderNorm, eHolderNorm, coe_toNNReal]
on_goal 2 => exact hf.eHolderNorm_lt_top.ne
have h₁ : edist x₁ x₂ ^ (r : ℝ) ≠ 0 :=
(Ne.symm <| ne_of_lt <| ENNReal.rpow_pos (edist_pos.2 hx) (edist_lt_top x₁ x₂).ne)
have h₂ : edist x₁ x₂ ^ (r : ℝ) ≠ ∞ := by simp [(edist_lt_top x₁ x₂).ne]
rw [← ENNReal.div_le_iff h₁ h₂]
refine le_iInf₂ fun C hC => ?_
rw [ENNReal.div_le_iff h₁ h₂]
exact hC x₁ x₂
