AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassProductMap

- A measurable pushforward of a finite measure preserves its total mass.

theorem mass_map_eq
    (mu : FiniteMeasure X) (f : X → X') (hf : Measurable f) :
    (mu.map f).mass = mu.mass := by
  unfold FiniteMeasure.mass
  rw [FiniteMeasure.map_apply mu hf MeasurableSet.univ]
  simp

/-- `commonMassProduct` commutes with applying measurable maps to its two
coordinates. -/

AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassProductMap.lean:27published source at 0e31a3cda412

- `commonMassProduct` commutes with applying measurable maps to its two coordinates.

theorem commonMassProduct_map_prodMap
    (mu : FiniteMeasure X) (nu : FiniteMeasure Y)
    (f : X → X') (g : Y → Y')
    (hf : Measurable f) (hg : Measurable g) :
    (commonMassProduct mu nu).map (Prod.map f g) =
      commonMassProduct (mu.map f) (nu.map g) := by
  rw [commonMassProduct, commonMassProduct, FiniteMeasure.map_smul,
    mass_map_eq mu f hf]
  rw [FiniteMeasure.map_prod_map mu nu hf hg]

end

end CommonMassProductMap
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassProductMap.lean:36published source at 0e31a3cda412