English
If s is measurable in β with μb(s) finite, c ∈ E, and f: α → β preserves measure from μ to μb, then composing Lp-indicatorConstLp on α with f gives the Lp-indicatorConstLp on the preimage of s under f, with the appropriate measurability proof carried over.
Русский
Если s измеримо в β, и μb(s) конечна, c ∈ E, а f: α → β сохраняет меру (μ → μb), тогда композиция Lp-indicatorConstLp с f равна Lp-indicatorConstLp на предобразе s по f, с надлежащим доказательством измеримости.
LaTeX
$$$\\mathrm{Lp.compMeasurePreserving}\;f\\;hf\\; (\\mathrm{indicatorConstLp}\\; p\\; hs\\; hμs\\; c) \\\\ = \\; \\mathrm{indicatorConstLp}\\; p\\; (hs.preimage hf.measurable)\\; (hf.measure_preimage hs.nullMeasurableSet)\\; c$$$
Lean4
theorem indicatorConstLp_compMeasurePreserving {s : Set β} (hs : MeasurableSet s) (hμs : μb s ≠ ∞) (c : E)
(hf : MeasurePreserving f μ μb) :
Lp.compMeasurePreserving f hf (indicatorConstLp p hs hμs c) =
indicatorConstLp p (hs.preimage hf.measurable) (by rwa [hf.measure_preimage hs.nullMeasurableSet]) c :=
rfl
