The theorem of Rockafellar and… to The twist theorem at a point

TheoremThe theorem of Rockafellar and Rüschendorf#

Every c-cyclically monotone set is contained in the c-superdifferential of a c-concave potential: there is a φ with φ x + φᶜ y = c (x, y) at every point (x, y) of the set, where φᶜ is the infimal c-transform of φ.

TauCeti.IsCyclicallyMonotone.exists_isCConcave_subset_cSuperdifferential.{u, v} {X : Type u}
  {Y : Type v} {c : X × Y → ℝ} {S : Set (X × Y)} (hS : TauCeti.IsCyclicallyMonotone c S) :
  ∃ φ, TauCeti.IsCConcave c φ ∧ S ⊆ TauCeti.cSuperdifferential c φ
Lean

Formalized in Tau Ceti as TauCeti.IsCyclicallyMonotone.exists_isCConcave_subset_cSuperdifferential.

Sources
LeanTauCeti.IsCyclicallyMonotone.exists_isCConcave_subset_cSuperdifferential
Used by 5
Used byThe Benamou–Brenier lower bound · Bounded-Lipschitz duality in supremum form · Bounded-Lipschitz Kantorovich–Rubinstein duality with attainment · Rockafellar's theorem · Strong Kantorovich duality for probability measures

TheoremThe twist theorem#

If the cost is differentiable in its first variable at contact partners and y ↦ Dₓ c (x, y) is injective among differentiable sections at almost every x, and a dual feasible pair has a first potential finite near, and differentiable at, μ-almost every point, then the contact fibres {y | (x, y) ∈ contactSet c φ ψ} are subsingletons for μ-almost every x. Combined with TauCeti.IsCoupling.ae_exists_condKernel_eq_dirac, a finite coupling of μ concentrated on the contact set has, for μ-almost every x, the Dirac mass at the unique contact partner of x as its conditional law.

TauCeti.ae_subsingleton_setOf_mem_contactSet.{u_1, u_2} {E : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} {φ : E → EReal} {ψ : Y → EReal}
  [MeasurableSpace E] (μ : MeasureTheory.Measure E)
  (hfeas : ∀ (x : E) (y : Y), φ x + ψ y ≤ ↑(c (x, y)))
  (hφ :
    ∀ᵐ (x : E) ∂μ,
      (∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) ∧ DifferentiableAt ℝ (fun x' => (φ x').toReal) x)
  (hc :
    ∀ᵐ (x : E) ∂μ,
      ∀ (y : Y), (x, y) ∈ TauCeti.contactSet c φ ψ → DifferentiableAt ℝ (fun x' => c (x', y)) x)
  (htwist :
    ∀ᵐ (x : E) ∂μ,
      Set.InjOn (fun y => fderiv ℝ (fun x' => c (x', y)) x)
        {y | DifferentiableAt ℝ (fun x' => c (x', y)) x}) :
  ∀ᵐ (x : E) ∂μ, {y | (x, y) ∈ TauCeti.contactSet c φ ψ}.Subsingleton
Lean

Formalized in Tau Ceti as TauCeti.ae_subsingleton_setOf_mem_contactSet.

Sources
LeanTauCeti.ae_subsingleton_setOf_mem_contactSet
Uses 1
Proof usesThe twist theorem at a point

TheoremThe twist theorem at a point#

Suppose the cost is twisted at x: the map y ↦ Dₓ c (x, y) is injective on the set of y for which the section c (·, y) is differentiable at x. If the potential is differentiable at x, finite near x, and satisfies the dual constraint near x, and the cost sections of the contact partners of x are differentiable at x, then x has at most one contact partner.

TauCeti.subsingleton_setOf_mem_contactSet.{u_1, u_2} {E : Type u_1} {Y : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℝ E] {c : E × Y → ℝ} {φ : E → EReal} {ψ : Y → EReal} {x : E}
  (hfeas : ∀ (y : Y), ∀ᶠ (x' : E) in nhds x, φ x' + ψ y ≤ ↑(c (x', y)))
  (hfin : ∀ᶠ (x' : E) in nhds x, φ x' ≠ ⊥) (hφ : DifferentiableAt ℝ (fun x' => (φ x').toReal) x)
  (hc : ∀ (y : Y), (x, y) ∈ TauCeti.contactSet c φ ψ → DifferentiableAt ℝ (fun x' => c (x', y)) x)
  (htwist :
    Set.InjOn (fun y => fderiv ℝ (fun x' => c (x', y)) x)
      {y | DifferentiableAt ℝ (fun x' => c (x', y)) x}) :
  {y | (x, y) ∈ TauCeti.contactSet c φ ψ}.Subsingleton
Lean

Formalized in Tau Ceti as TauCeti.subsingleton_setOf_mem_contactSet.

Sources
LeanTauCeti.subsingleton_setOf_mem_contactSet
Used by 1
Used byThe twist theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.