ContactObstruction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem356.ae_contact_of_graphCost_eq line 14

Source documentation

A contact condition for optimal couplings also holds along any optimal admissible graph. This needs no measurable-set hypothesis on Contact.

lemma ae_contact_of_graphCost_eq {mu : Measure E3} [IsProbabilityMeasure mu]
    {Contact : Triple → Prop}
    (hcontact : ∀ pi : Measure Triple, IsThreeCoupling mu pi →
      (∫⁻ t, coulombCost t ∂pi) = kantorovichValue mu → ∀ᵐ t ∂pi, Contact t)
    {T2 T3 : E3 → E3} (h2 : Preserves mu T2) (h3 : Preserves mu T3)
    (hopt : graphCost mu T2 T3 = kantorovichValue mu) :
    ∀ᵐ x ∂mu, Contact (graphMap T2 T3 x) := by
…

Mentions: OAI.Problem356.E3, OAI.Problem356.Triple, OAI.Problem356.IsThreeCoupling, OAI.Problem356.coulombCost, OAI.Problem356.kantorovichValue, OAI.Problem356.Preserves, OAI.Problem356.graphCost, OAI.Problem356.graphMap

lemma OAI.Problem356.noMongeOptimizer_of_contact_obstruction line 27

lemma OAI.Problem356.noMongeOptimizer_of_selection_obstruction line 43

Source documentation

Abstract branch-selection endgame. A contact triple whose first coordinate lies in B forces its second coordinate to satisfy Select. If no preserving map can satisfy that selection almost everywhere for an absolutely continuous submeasure, no admissible graph is optimal.

lemma noMongeOptimizer_of_selection_obstruction
    (mu nu : Measure E3) [IsProbabilityMeasure mu]
    (hnu : nu ≪ mu) {B : Set E3} (hB : ∀ᵐ x ∂nu, x ∈ B)
    {Contact : Triple → Prop} {Select : E3 → E3 → Prop}
    (hcontact : ∀ pi : Measure Triple, IsThreeCoupling mu pi →
      (∫⁻ t, coulombCost t ∂pi) = kantorovichValue mu → ∀ᵐ t ∂pi, Contact t)
    (hselect : ∀ x y z : E3, x ∈ B → Contact (x, (y, z)) → Select x y)
    (hobstruction : ∀ T : E3 → E3, Preserves mu T →
      ¬ (∀ᵐ x ∂nu, Select x (T x))) :
    NoMongeOptimizer mu := by
…