Theorems · Theorem · measure theory

MeasureTheory.MeasurePreserving.skew_product

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {δ : Type u_4} [inst_3 : MeasurableSpace δ] {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {μc : MeasureTheory.Measure γ} {μd : MeasureTheory.Measure δ}
  [MeasureTheory.SFinite μa] [MeasureTheory.SFinite μc] {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    ∀ {g : α → γ → δ},
      Measurable (Function.uncurry g) →
        (∀ᵐ (a : α) ∂μa, MeasureTheory.Measure.map (g a) μc = μd) →
          MeasureTheory.MeasurePreserving (fun p => (f p.1, g p.1 p.2)) (μa.prod μc) (μb.prod μd)

Let f : α → β be a measure-preserving map. For a.e. all a, let g a : γ → δ be a measure-preserving map. Also suppose that g is measurable as a function of two arguments. Then the map fun (a, c) ↦ (f a, g a c) is a measure-preserving map for the product measures on α × γ and β × δ. Some authors call a map of the form fun (a, c) ↦ (f a, g a c) a skew product over f, thus the choice of a name.

Defined in

Mathlib.MeasureTheory.Measure.Prod

Cited by

5 results in Mathlib

Foundations

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

Assumes

MeasurableSpaceMeasurableSpaceMeasurableSpaceMeasurableSpaceMeasureTheory.SFiniteMeasureTheory.SFinite