AutoSamplingTheory.TechnicalLemmas.Measure.ProbabilityCouplingCompactness

- Probability-measure version of the fixed-marginal coupling predicate. It is definitionally adapted to the weak topology, whose continuous maps are the `ProbabilityMeasure.map` operations.

def IsProbabilityCoupling
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (gamma : ProbabilityMeasure (X × Y))
    (mu : ProbabilityMeasure X) (nu : ProbabilityMeasure Y) : Prop :=
  ProbabilityMeasure.map gamma measurable_fst.aemeasurable = mu ∧
    ProbabilityMeasure.map gamma measurable_snd.aemeasurable = nu

/-- Fixed-marginal probability couplings as a subset of the weak probability
measure space. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ProbabilityCouplingCompactness.lean:43published source at 0e31a3cda412

- Fixed-marginal probability couplings as a subset of the weak probability measure space.

def probabilityCouplingSet
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (mu : ProbabilityMeasure X) (nu : ProbabilityMeasure Y) :
    Set (ProbabilityMeasure (X × Y)) :=
  {gamma | IsProbabilityCoupling gamma mu nu}

/-- The topology-facing probability coupling predicate agrees exactly with
Samplinglib's raw-measure `Transport.IsCoupling`. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ProbabilityCouplingCompactness.lean:52published source at 0e31a3cda412

- The topology-facing probability coupling predicate agrees exactly with Samplinglib's raw-measure `Transport.IsCoupling`.

theorem isProbabilityCoupling_iff_isCoupling_toMeasure
    {X Y : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    {gamma : ProbabilityMeasure (X × Y)}
    {mu : ProbabilityMeasure X} {nu : ProbabilityMeasure Y} :
    IsProbabilityCoupling gamma mu nu ↔
      Transport.IsCoupling (gamma : Measure (X × Y))
        (mu : Measure X) (nu : Measure Y) := by
  constructor
  · intro h
    constructor
    · have h' := congrArg ProbabilityMeasure.toMeasure h.1
      simpa [Measure.fst] using h'
    · have h' := congrArg ProbabilityMeasure.toMeasure h.2
      simpa [Measure.snd] using h'
  · intro h
    constructor
    · apply ProbabilityMeasure.toMeasure_injective
      simpa [Measure.fst] using h.1
    · apply ProbabilityMeasure.toMeasure_injective
      simpa [Measure.snd] using h.2

section Closed

variable {X Y : Type*}
  [MeasurableSpace X] [MetricSpace X] [SecondCountableTopology X] [BorelSpace X]
  [MeasurableSpace Y] [MetricSpace Y] [SecondCountableTopology Y] [BorelSpace Y]

/-- Fixed marginal constraints are closed in the weak topology on probability
measures. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ProbabilityCouplingCompactness.lean:60published source at 0e31a3cda412

- Fixed marginal constraints are closed in the weak topology on probability measures.

theorem isClosed_probabilityCouplingSet
    (mu : ProbabilityMeasure X) (nu : ProbabilityMeasure Y) :
    IsClosed (probabilityCouplingSet mu nu) := by
  rw [probabilityCouplingSet]
  change IsClosed
    ({gamma : ProbabilityMeasure (X × Y) |
        ProbabilityMeasure.map gamma measurable_fst.aemeasurable = mu} ∩
      {gamma : ProbabilityMeasure (X × Y) |
        ProbabilityMeasure.map gamma measurable_snd.aemeasurable = nu})
  apply IsClosed.inter
  · exact isClosed_eq (ProbabilityMeasure.continuous_map continuous_fst) continuous_const
  · exact isClosed_eq (ProbabilityMeasure.continuous_map continuous_snd) continuous_const

end Closed

section Tight

variable {X Y : Type*}
  [MeasurableSpace X] [MetricSpace X] [CompleteSpace X]
  [SecondCountableTopology X] [BorelSpace X]
  [MeasurableSpace Y] [MetricSpace Y] [CompleteSpace Y]
  [SecondCountableTopology Y] [BorelSpace Y]

/-- All raw couplings of two fixed probability measures form a tight family.
This is the reusable fixed-marginal tightness statement behind Prokhorov. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ProbabilityCouplingCompactness.lean:89published source at 0e31a3cda412

- All raw couplings of two fixed probability measures form a tight family. This is the reusable fixed-marginal tightness statement behind Prokhorov.

theorem isTightMeasureSet_couplingSet
    (mu : Measure X) (nu : Measure Y)
    [IsProbabilityMeasure mu] [IsProbabilityMeasure nu] :
    IsTightMeasureSet (Transport.couplingSet mu nu) := by
  apply IsTightMeasureSet.prodMk
  · apply (isTightMeasureSet_singleton (μ := mu)).subset
    rintro rho ⟨gamma, hgamma, rfl⟩
    change gamma.fst = mu
    exact hgamma.1
  · apply (isTightMeasureSet_singleton (μ := nu)).subset
    rintro rho ⟨gamma, hgamma, rfl⟩
    change gamma.snd = nu
    exact hgamma.2

/-- The underlying raw measures of the probability-coupling set are tight. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ProbabilityCouplingCompactness.lean:114published source at 0e31a3cda412

- The underlying raw measures of the probability-coupling set are tight.

theorem isTightMeasureSet_probabilityCouplingSet
    (mu : ProbabilityMeasure X) (nu : ProbabilityMeasure Y) :
    IsTightMeasureSet
      {((gamma : ProbabilityMeasure (X × Y)) : Measure (X × Y)) |
        gamma ∈ probabilityCouplingSet mu nu} := by
  apply (isTightMeasureSet_couplingSet (mu : Measure X) (nu : Measure Y)).subset
  rintro rho ⟨gamma, hgamma, rfl⟩
  exact (isProbabilityCoupling_iff_isCoupling_toMeasure.mp hgamma)

/-- Probability couplings with two fixed marginals are compact for weak
convergence. -/

AutoSamplingTheory/TechnicalLemmas/Measure/ProbabilityCouplingCompactness.lean:129published source at 0e31a3cda412

- Probability couplings with two fixed marginals are compact for weak convergence.

theorem isCompact_probabilityCouplingSet
    (mu : ProbabilityMeasure X) (nu : ProbabilityMeasure Y) :
    IsCompact (probabilityCouplingSet mu nu) := by
  have htight := isTightMeasureSet_probabilityCouplingSet mu nu
  have hcompact : IsCompact (closure (probabilityCouplingSet mu nu)) :=
    isCompact_closure_of_isTightMeasureSet htight
  have hclosed : IsClosed (probabilityCouplingSet mu nu) :=
    isClosed_probabilityCouplingSet mu nu
  rwa [hclosed.closure_eq] at hcompact

end Tight

end

end ProbabilityCouplingCompactness
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/ProbabilityCouplingCompactness.lean:140published source at 0e31a3cda412