English
If hg is HolderOnWith on t and hf is HolderWith on f, and f maps into t, then g∘f is HolderWith with combined constants.
Русский
Если hg HölderOnWith на t и hf Hölder на f с отображением в t, то g∘f HölderWith с объединёнными константами.
LaTeX
$$$\\text{HolderOnWith } C_g r_g g t \\Rightarrow \\text{HolderWith } C_f r_f f \\Rightarrow \\forall x, f x \\in t \\Rightarrow \\text{HolderWith } (C_g * C_f^{r_g}) (r_g * r_f) (g \\circ f)$$$
Lean4
theorem comp_holderWith {Cg rg : ℝ≥0} {g : Y → Z} {t : Set Y} (hg : HolderOnWith Cg rg g t) {Cf rf : ℝ≥0} {f : X → Y}
(hf : HolderWith Cf rf f) (ht : ∀ x, f x ∈ t) : HolderWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) :=
holderOnWith_univ.mp <| hg.comp (hf.holderOnWith univ) fun x _ => ht x
