English
If g is Hölder with constants Cg,rg and f is Hölder with Cf,rf, then g∘f is Hölder with constants Cg Cf^{rg} and rg·rf.
Русский
Если g Холдер с константами Cg, rg, и f Холдер с Cf, rf, то композиция g∘f Холдер с константами Cg Cf^{rg} и rg rf.
LaTeX
$$$\operatorname{HolderWith}(C_g, r_g, g) \wedge \operatorname{HolderWith}(C_f, r_f, f) \Rightarrow \operatorname{HolderWith}(C_g \cdot C_f^{r_g},\; r_g r_f,\; g \circ f)$$$
Lean4
theorem comp {Cg rg : ℝ≥0} {g : Y → Z} (hg : HolderWith Cg rg g) {Cf rf : ℝ≥0} {f : X → Y} (hf : HolderWith Cf rf f) :
HolderWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) :=
(hg.holderOnWith univ).comp_holderWith hf fun _ => trivial
