compMeasurePreservingLp — Mathlib

English

If f and g are continuous at a point z and all g(z) preserve μ→ν, then the composition map z ↦ Lp.compMeasurePreserving(g z)(f z) is continuous at z.

Русский

Если f и g непрерывны в точке z и каждый g(z) сохраняет меру μ→ν, то отображение z↦Lp.compMeasurePreserving(g z)(f z) непрерывно в этой точке.

LaTeX

$$$\\text{If } f,g, \\ hgm, \\ hp, \\; \\text{then } z \\mapsto Lp\\bigl(g(z),hgm(z),f(z)\\bigr) \\text{ is continuous at } z.$$$

Lean4

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

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