production module

`AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassProductMap`

2 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassProductMap.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.CommonMass

Imported by

AutoSamplingTheory.TechnicalLemmas.Measure.PermutedReplacementQuadraticCostTests.CommonMassProductMap

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassProductMap.mass_map_eq Partial Not mapped

- 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 ed709a7f320d

theorem AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassProductMap.commonMassProduct_map_prodMap Partial Not mapped

- `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 ed709a7f320d

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/Measure/CommonMassProductMap.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Measure.CommonMass

/-!
# Naturality of the common-mass product under measurable maps

The canonical equal-mass product is compatible with measurable pushforwards.
This is the measure-algebra bridge needed to turn a product law on two local
pair blocks into the source-target replacement block used by the Brenier
competitor.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace Measure
namespace CommonMassProductMap

open MeasureTheory
open CommonMass

noncomputable section

variable {X Y X' Y' : Type*}
  [MeasurableSpace X] [MeasurableSpace Y]
  [MeasurableSpace X'] [MeasurableSpace Y']

/-- 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. -/
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