English
If g is Hölder on t and f is Hölder on s, and f maps s into t, then g∘f is Hölder on s with constants CgCf^rg and rg rf.
Русский
Если g Hölder на t, f Hölder на s, и f(s) ⊆ t, то g∘f является Hölder на s с объединёнными константами.
LaTeX
$$$\\text{HolderOnWith } C_g r_g (g) t \\; \\text{ и } \\text{HolderOnWith } C_f r_f (f) s, \\; \\text{MapsTo } f s t \\;\Rightarrow\\; \\text{HolderOnWith } (C_g * C_f^{r_g}) (r_g * r_f) (g \\circ f) s$$$
Lean4
theorem comp {Cg rg : ℝ≥0} {g : Y → Z} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf rf : ℝ≥0} {f : X → Y}
(hf : HolderOnWith Cf rf f s) (hst : MapsTo f s t) : HolderOnWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s :=
by
intro x hx y hy
rw [ENNReal.coe_mul, mul_comm rg, NNReal.coe_mul, ENNReal.rpow_mul, mul_assoc,
ENNReal.coe_rpow_of_nonneg _ rg.coe_nonneg, ← ENNReal.mul_rpow_of_nonneg _ _ rg.coe_nonneg]
exact hg.edist_le_of_le (hst hx) (hst hy) (hf.edist_le hx hy)
