integrable_comp_iff_of_antilipschitz

English

If g is Lipschitz with constant K and antilipschitz with K', and g(0)=0, then Integrable(g ∘ f) μ is equivalent to Integrable(f) μ.

Русский

Если g липшицева с константой K и антилипищитова с константой K', и g(0)=0, тогдаIntegrable(g∘f) эквивалентна Integrable(f).

LaTeX

$$$hg:\\text{ LipschitzWith }K\\, g\\,\\land\\, hg':\\text{ AntilipschitzWith }K'\\, g\\land g(0)=0\\ \\Rightarrow\\ Integrable (g\\circ f)\\mu\\;\\Leftrightarrow\\ Integrable f\\mu$$$

Lean4

theorem integrable_comp_iff_of_antilipschitz {K K'} {f : α → β} {g : β → γ} (hg : LipschitzWith K g)
    (hg' : AntilipschitzWith K' g) (g0 : g 0 = 0) : Integrable (g ∘ f) μ ↔ Integrable f μ := by
  simp [← memLp_one_iff_integrable, hg.memLp_comp_iff_of_antilipschitz hg' g0]

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