comp_holderOnWith — Mathlib

English

If g is HölderWith and f is HölderOnWith on s, then g∘f is HölderOnWith on s with corresponding constants.

Русский

Если g ХолдерWith, а f ХолдерOnWith на s, то композиция g∘f ХолдерOnWith на s с соответствующими константами.

LaTeX

$$$\operatorname{HolderOnWith}(C_g,r_g,g) \wedge \operatorname{HolderOnWith}(C_f,r_f,f,s) \Rightarrow \operatorname{HolderOnWith}(C_g \cdot C_f^{r_g},\; r_g r_f,\; g \circ f,\; s)$$$

Lean4

theorem comp_holderOnWith {Cg rg : ℝ≥0} {g : Y → Z} (hg : HolderWith Cg rg g) {Cf rf : ℝ≥0} {f : X → Y} {s : Set X}
    (hf : HolderOnWith Cf rf f s) : HolderOnWith (Cg * Cf ^ (rg : ℝ)) (rg * rf) (g ∘ f) s :=
  (hg.holderOnWith univ).comp hf fun _ _ => trivial

Похожие утверждения