Theorems · Theorem · measure theory

MeasureTheory.Lp.compMeasurePreserving_continuous

∀ {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)],
  p ≠ ⊤ → Continuous fun gf => (MeasureTheory.Lp.compMeasurePreserving ⇑↑gf.2 ⋯) gf.1

Let X and Y be R₁ topological spaces with Borel σ-algebras and measures μ and ν, respectively. Suppose that μ is inner regular for finite measure sets with respect to compact sets and ν is a locally finite measure. Let 1 ≤ p < ∞ be an extended nonnegative real number. Then the composition of a function g : Lp E p ν and a measure-preserving continuous function f : C(X, Y) is continuous in both variables.

Defined in

Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceMeasurableSpaceBorelSpaceR1SpaceTopologicalSpaceMeasurableSpaceBorelSpaceR1SpaceMeasureTheory.Measure.InnerRegularCompactLTTopMeasureTheory.IsLocallyFiniteMeasureNormedAddCommGroupFact