AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalSupportCyclic

- Finite-measure core of the direct Brenier perturbation: an optimal quadratic coupling between two finite-second-moment marginals has support satisfying every distinct finite pairing-cycle inequality.

theorem pairingDistinctCycleMonotone_support_of_quadraticOptimal_finite
    (gamma : FiniteMeasure (E × E))
    {mu0 mu1 : Measure E}
    (hopt : IsQuadraticOptimalCoupling (gamma : Measure (E × E)) mu0 mu1)
    (hmu0 : Integrable (fun x : E => ‖x‖ ^ 2) mu0)
    (hmu1 : Integrable (fun y : E => ‖y‖ ^ 2) mu1) :
    PairingDistinctCycleMonotone ((gamma : Measure (E × E)).support) := by
  intro n p hp hsupp
  change cycleValue p ≤ 0
  by_contra hnot
  have hcycle : 0 < cycleValue p := lt_of_not_ge hnot
  obtain ⟨localBlock, hlocalPos, hlocalLe, hlocalCost⟩ :=
    exists_localBlocks_cyclicReplacement_lt_of_cycleValue_pos
      gamma hp hcycle hsupp
  let sigmaInv : Equiv.Perm (Fin (n + 1)) :=
    (cycleSuccessorPerm (n := n)).symm
  let removed : FiniteMeasure (E × E) := commonSliceRemoved localBlock
  let replacement : FiniteMeasure (E × E) :=
    commonSlicePermutationReplacement localBlock sigmaInv
  let remainder : FiniteMeasure (E × E) :=
    finiteRemainder gamma removed
  let xi : FiniteMeasure (E × E) :=
    canonicalGlobalCompetitor gamma localBlock sigmaInv

  have hpres := canonicalGlobalCompetitor_preserves_marginals
    gamma localBlock hlocalPos hlocalLe sigmaInv
  have hxiCoupling : IsCoupling (xi : Measure (E × E)) mu0 mu1 := by
    constructor
    · change (xi : Measure (E × E)).map Prod.fst = mu0
      calc
        (xi : Measure (E × E)).map Prod.fst =
            (gamma : Measure (E × E)).map Prod.fst := by
          have hmap := congrArg
            (fun eta : FiniteMeasure E => (eta : Measure E)) hpres.1
          simpa [xi] using hmap
        _ = mu0 := by
          simpa [Measure.fst] using hopt.1.1
    · change (xi : Measure (E × E)).map Prod.snd = mu1
      calc
        (xi : Measure (E × E)).map Prod.snd =
            (gamma : Measure (E × E)).map Prod.snd := by
          have hmap := congrArg
            (fun eta : FiniteMeasure E => (eta : Measure E)) hpres.2
          simpa [xi] using hmap
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalSupportCyclic.lean:51published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.

- Ordinary-measure wrapper. A probability first marginal forces an optimal coupling to be a probability measure and hence a finite measure, after which the finite-measure core applies.

theorem pairingDistinctCycleMonotone_support_of_quadraticOptimal
    {gamma : Measure (E × E)} {mu0 mu1 : Measure E}
    [IsProbabilityMeasure mu0]
    (hopt : IsQuadraticOptimalCoupling gamma mu0 mu1)
    (hmu0 : Integrable (fun x : E => ‖x‖ ^ 2) mu0)
    (hmu1 : Integrable (fun y : E => ‖y‖ ^ 2) mu1) :
    PairingDistinctCycleMonotone gamma.support := by
  letI : IsProbabilityMeasure gamma :=
    isProbabilityMeasure_of_isCoupling_left hopt.1
  let gammaFinite : FiniteMeasure (E × E) := ⟨gamma, by infer_instance⟩
  simpa [gammaFinite] using
    pairingDistinctCycleMonotone_support_of_quadraticOptimal_finite
      gammaFinite hopt hmu0 hmu1

/-- Source-facing `P₂,ac` specialization.  Absolute continuity is not used by
the support-cyclical-monotonicity perturbation itself, but this is the endpoint
shape consumed by the later Brenier/Rockafellar construction in Chewi's
Euclidean setting. -/

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalSupportCyclic.lean:162published source at 0e31a3cda412

- Source-facing `P₂,ac` specialization. Absolute continuity is not used by the support-cyclical-monotonicity perturbation itself, but this is the endpoint shape consumed by the later Brenier/Rockafellar construction in Chewi's Euclidean setting.

theorem pairingDistinctCycleMonotone_support_of_quadraticOptimal_p2ac
    {gamma : Measure (E × E)} {mu0 mu1 : Measure E}
    (hmu0 : IsAbsolutelyContinuousFiniteSecondMoment mu0)
    (hmu1 : IsAbsolutelyContinuousFiniteSecondMoment mu1)
    (hopt : IsQuadraticOptimalCoupling gamma mu0 mu1) :
    PairingDistinctCycleMonotone gamma.support := by
  letI : IsProbabilityMeasure mu0 := hmu0.1
  letI : IsProbabilityMeasure mu1 := hmu1.1
  exact pairingDistinctCycleMonotone_support_of_quadraticOptimal
    hopt hmu0.2.2 hmu1.2.2

end

end QuadraticOptimalSupportCyclic
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalSupportCyclic.lean:180published source at 0e31a3cda412