AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalUniqueness

- Two quadratic-optimal couplings with the same marginals are equal when the first marginal is absolutely continuous and both marginals have finite second moments.

theorem eq_of_quadraticOptimal
    {gamma₀ gamma₁ : Measure (E × E)} {mu₀ mu₁ : Measure E}
    [IsProbabilityMeasure mu₀]
    (h₀ : IsQuadraticOptimalCoupling gamma₀ mu₀ mu₁)
    (h₁ : IsQuadraticOptimalCoupling gamma₁ mu₀ mu₁)
    (hmu₀ac : mu₀ ≪ (volume : Measure E))
    (hmu₀ : Integrable (fun x : E => ‖x‖ ^ 2) mu₀)
    (hmu₁ : Integrable (fun y : E => ‖y‖ ^ 2) mu₁) :
    gamma₀ = gamma₁ := by
  have hmid :
      IsQuadraticOptimalCoupling (midpointMeasure gamma₀ gamma₁) mu₀ mu₁ :=
    isQuadraticOptimalCoupling_midpoint h₀ h₁
  letI : IsProbabilityMeasure (midpointMeasure gamma₀ gamma₁) :=
    isProbabilityMeasure_of_isCoupling_left hmid.1
  have hmid_ne : midpointMeasure gamma₀ gamma₁ ≠ 0 := by
    intro hzero
    have hmass : midpointMeasure gamma₀ gamma₁ Set.univ = 1 := measure_univ
    simpa [hzero] using hmass
  rcases Measure.nonempty_support hmid_ne with ⟨base, hbase⟩
  let T : E → E :=
    gradient
      (finitePart
        (properRockafellarPotential base (midpointMeasure gamma₀ gamma₁).support))
  have hmidGraph :
      ∀ᵐ z ∂midpointMeasure gamma₀ gamma₁, z.2 = T z.1 := by
    simpa [T] using
      (ae_snd_eq_gradient_of_quadraticOptimal_of_base
        hmid hmu₀ac hmu₀ hmu₁ hbase)
  have hhalf : (2 : ℝ≥0∞)⁻¹ ≠ 0 := by
    norm_num
  have hgamma₀Graph : ∀ᵐ z ∂gamma₀, z.2 = T z.1 := by
    apply ae_of_ae_smul_add_left
      (μ := gamma₀) (ν := (2 : ℝ≥0∞)⁻¹ • gamma₁) hhalf
    simpa [midpointMeasure] using hmidGraph
  have hgamma₁Graph : ∀ᵐ z ∂gamma₁, z.2 = T z.1 := by
    apply ae_of_ae_add_smul_right
      (μ := (2 : ℝ≥0∞)⁻¹ • gamma₀) (ν := gamma₁) hhalf
    simpa [midpointMeasure] using hmidGraph
  have hT : Measurable T := by
    dsimp [T]
    exact measurable_gradient _
  calc
    gamma₀ = Measure.map (fun x : E => (x, T x)) mu₀ :=
      eq_map_graph_of_isCoupling_of_ae_snd_eq h₀.1 hT hgamma₀Graph
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalUniqueness.lean:48published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.

- `P₂,ac` wrapper on the source law. The target is deliberately not assumed absolutely continuous; only its finite second moment enters the uniqueness proof.

theorem eq_of_quadraticOptimal_p2ac_source
    {gamma₀ gamma₁ : Measure (E × E)} {mu₀ mu₁ : Measure E}
    (hmu₀ : IsAbsolutelyContinuousFiniteSecondMoment mu₀)
    (hmu₁ : Integrable (fun y : E => ‖y‖ ^ 2) mu₁)
    (h₀ : IsQuadraticOptimalCoupling gamma₀ mu₀ mu₁)
    (h₁ : IsQuadraticOptimalCoupling gamma₁ mu₀ mu₁) :
    gamma₀ = gamma₁ := by
  letI : IsProbabilityMeasure mu₀ := hmu₀.1
  exact eq_of_quadraticOptimal h₀ h₁ hmu₀.2.1 hmu₀.2.2 hmu₁

end

end QuadraticOptimalUniqueness
end Measure
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalUniqueness.lean:98published source at 0e31a3cda412