ConvexOptimality.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Optimality and uniqueness from a supporting potential

This packages the limiting-potential step of the arbitrary-target argument. The potential need only be Lipschitz on the source body and support the candidate map almost everywhere. Its restricted conjugate supplies the dual certificate, and Rademacher regularity makes its equality locus a graph.

theorem OAI.Problem358.isUniqueQuadraticOptimalMap_of_ae_differentiable_supporting_potential line 17

Source documentation

A continuous source potential, supporting the map almost everywhere and having almost everywhere unique differentiable interior slopes, certifies uniqueness among all transport plans.

theorem isUniqueQuadraticOptimalMap_of_ae_differentiable_supporting_potential
    {d : ℕ} {ρ μ : Measure (E d)} [IsFiniteMeasure ρ] [IsFiniteMeasure μ]
    {K Y : Set (E d)} {u : E d → ℝ} {T : E d → E d}
    (hK : IsCompact K) (hne : K.Nonempty) (hY : IsCompact Y)
    (hρ : IsSupported ρ K) (hμ : IsSupported μ Y)
    (hu : ContinuousOn u K) (hT : Measurable T) (hpush : Measure.map T ρ = μ)
    (hdiff : ∀ᵐ x ∂ρ, x ∈ interior K ∧ DifferentiableAt ℝ u x)
    (hs : ∀ᵐ x ∂ρ, ∀ z ∈ K, u x + inner ℝ (z - x) (T x) ≤ u z) :
    IsUniqueQuadraticOptimalMap ρ μ T := by
…

theorem OAI.Problem358.isUniqueQuadraticOptimalMap_uniform_of_supporting_potential line 61

Source documentation

For uniform convex sources, Rademacher and the null convex boundary discharge all differentiability assumptions of the preceding certificate.

theorem isUniqueQuadraticOptimalMap_uniform_of_supporting_potential
    {d : ℕ} {K Y : Set (E d)} {μ : Measure (E d)}
    [IsFiniteMeasure (uniformMeasure K)] [IsFiniteMeasure μ]
    {u : E d → ℝ} {T : E d → E d} {L : ℝ≥0}
    (hK : IsCompact K) (hne : K.Nonempty) (hconv : Convex ℝ K)
    (hY : IsCompact Y) (hμ : IsSupported μ Y)
    (hu : LipschitzOnWith L u K) (hT : Measurable T)
    (hpush : Measure.map T (uniformMeasure K) = μ)
    (hs : ∀ᵐ x ∂uniformMeasure K, ∀ z ∈ K,
      u x + inner ℝ (z - x) (T x) ≤ u z) :
    IsUniqueQuadraticOptimalMap (uniformMeasure K) μ T := by
…

theorem OAI.Problem358.isUniqueQuadraticOptimalMap_of_supporting_potential line 100

Source documentation

A measurable map supported by a Lipschitz potential on a compact convex source is the unique quadratic optimal plan to its compactly supported law.

theorem isUniqueQuadraticOptimalMap_of_supporting_potential
    {d : ℕ} {K Y : Set (E d)} {μ : Measure (E d)} [IsProbabilityMeasure μ]
    {u : E d → ℝ} {T : E d → E d} {L : ℝ≥0}
    (hK : IsCompact K) (hKconv : Convex ℝ K) (hKne : K.Nonempty)
    (hY : IsCompact Y) (hμ : IsSupported μ Y)
    (hu : LipschitzOnWith L u K) (hT : Measurable T)
    (hpush : Measure.map T (uniformMeasure K) = μ)
    (hsupport : ∀ᵐ x ∂uniformMeasure K,
      ∀ z ∈ K, u x + ⟪T x, z - x⟫ ≤ u z) :
    IsUniqueQuadraticOptimalMap (uniformMeasure K) μ T := by
…