Theorems · Theorem · measure theory

ContinuousWithinAt.compMeasurePreservingLp

∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] [R1Space X]
  [inst_4 : TopologicalSpace Y] [inst_5 : MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X}
  {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {E : Type u_3}
  [inst_10 : NormedAddCommGroup E] {p : ENNReal} [inst_11 : Fact (1 ≤ p)] {Z : Type u_4} [inst_12 : TopologicalSpace Z]
  {f : Z → ↥(MeasureTheory.Lp E p ν)} {g : Z → C(X, Y)} {s : Set Z} {z : Z},
  ContinuousWithinAt f s z →
    ContinuousWithinAt g s z →
      ∀ (hgm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(g z)) μ ν),
        p ≠ ⊤ → ContinuousWithinAt (fun z => (MeasureTheory.Lp.compMeasurePreserving ⇑(g z) ⋯) (f z)) s z

Defined in

Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving

Cited by

1 results in Mathlib

Foundations

Depth 241 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceR1SpaceTopologicalSpaceMeasurableSpaceBorelSpaceR1SpaceMeasureTheory.Measure.InnerRegularCompactLTTopMeasureTheory.IsLocallyFiniteMeasureNormedAddCommGroupFactTopologicalSpace