compMeasurePreservingLp — Mathlib

English

Let X,Y be spaces with inner regular and locally finite measures. If f: X→Lp(E,p,ν) and g: X→C(X,Y) are continuous on a set s, and g preserves μ→ν, then z↦Lp.compMeasurePreserving(g z)(f z) is continuous on s.

Русский

Пусть f и g непрерывны на s, g(z) сохраняет меру, тогда композиционная операция Lp непрерывна на s.

LaTeX

$$$\\forall z\\in s,\\; \\text{ContinuousOn}(f,g;z) \\Rightarrow \\text{ContinuousOn}(z \\mapsto Lp\\bigl(g(z),f(z)\\bigr);s).$$$

Lean4

theorem compMeasurePreservingLp (hf : ContinuousOn f s) (hg : ContinuousOn g s) (hgm : ∀ z, MeasurePreserving (g z) μ ν)
    (hp : p ≠ ∞) : ContinuousOn (fun z ↦ Lp.compMeasurePreserving (g z) (hgm z) (f z)) s := fun z hz ↦
  (hf z hz).compMeasurePreservingLp (hg z hz) hgm hp

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