Conjugacy.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Supporting slopes at differentiability points

The elementary local step used to identify the equality locus of a Fenchel certificate. No convexity assumption is needed once a supporting inequality is supplied.

def OAI.Problem358.restrictedConjugate line 15
Source documentation
The convex conjugate with the source variable restricted to K.
```
def restrictedConjugate (K : Set V) (u : V → ℝ) (y : V) : ℝ :=
…
```
lemma OAI.Problem358.restrictedConjugate_eq_of_isMaxOn line 18
lemma OAI.Problem358.restrictedConjugate_attained line 27
lemma OAI.Problem358.restrictedConjugate_fenchel line 36

lemma OAI.Problem358.restrictedConjugate_eq_iff_support line 48

Source documentation

Fenchel equality is exactly the supporting-slope inequality on the source set.

lemma restrictedConjugate_eq_iff_support
    {K : Set V} {u : V → ℝ} (hK : IsCompact K)
    (hu : ContinuousOn u K) {x y : V} (hx : x ∈ K) :
    inner ℝ x y = u x + restrictedConjugate K u y ↔
      ∀ z ∈ K, u x + inner ℝ (z - x) y ≤ u z := by
…

Mentions: OAI.Problem358.restrictedConjugate

lemma OAI.Problem358.restrictedConjugate_sub_le line 68
lemma OAI.Problem358.restrictedConjugate_lipschitz line 81
lemma OAI.Problem358.restrictedConjugate_continuous line 95
lemma OAI.Problem358.restrictedConjugate_convex line 104
Source documentation
Restricting the source variable does not prevent convexity in the dual variable.
```
lemma restrictedConjugate_convex
    {K : Set V} {u : V → ℝ} (hK : IsCompact K) (hne : K.Nonempty)
    (hu : ContinuousOn u K) : ConvexOn ℝ Set.univ (restrictedConjugate K u) := by
…
```
Mentions: OAI.Problem358.restrictedConjugate

lemma OAI.Problem358.restrictedConjugate_supporting_slope_eq_fderiv line 122

Source documentation

A supporting slope at an interior differentiability point is the derivative.

lemma restrictedConjugate_supporting_slope_eq_fderiv
    {K : Set V} {u : V → ℝ} {x y : V} {u' : V →L[ℝ] ℝ}
    (hx : x ∈ interior K) (hu : HasFDerivAt u u' x)
    (hs : ∀ z ∈ K, u x + inner ℝ (z - x) y ≤ u z) :
    u' = innerSL ℝ y := by
…

lemma OAI.Problem358.restrictedConjugate_supporting_slope_unique line 139

lemma OAI.Problem358.supporting_slope_of_tendsto line 149

Source documentation

Supporting inequalities survive simultaneous pointwise potential and slope limits.

lemma supporting_slope_of_tendsto
    {ι : Type*} {l : Filter ι} [l.NeBot]
    {K : Set V} {u : V → ℝ} {un : ι → V → ℝ} {pn : ι → V} {x p : V}
    (hux : Tendsto (fun n => un n x) l (𝓝 (u x)))
    (hu : ∀ z ∈ K, Tendsto (fun n => un n z) l (𝓝 (u z)))
    (hp : Tendsto pn l (𝓝 p))
    (hs : ∀ᶠ n in l, ∀ z ∈ K, un n x + inner ℝ (z - x) (pn n) ≤ un n z) :
    ∀ z ∈ K, u x + inner ℝ (z - x) p ≤ u z := by
…

lemma OAI.Problem358.restrictedConjugate_quadratic_dual_le line 162

Source documentation

Continuous quadratic-cost dual potentials obtained from the restricted conjugate.

lemma restrictedConjugate_quadratic_dual_le
    {K : Set V} {u : V → ℝ} (hK : IsCompact K) (hu : ContinuousOn u K)
    {x : V} (hx : x ∈ K) (y : V) :
    (‖x‖ ^ 2 - 2 * u x) + (‖y‖ ^ 2 - 2 * restrictedConjugate K u y) ≤
      ‖x - y‖ ^ 2 := by
…

Mentions: OAI.Problem358.restrictedConjugate

lemma OAI.Problem358.restrictedConjugate_quadratic_dual_eq_iff line 171

theorem OAI.Problem358.ae_mem_interior_uniformMeasure line 191

Source documentation

A convex source gives full measure to its interior.

theorem ae_mem_interior_uniformMeasure {d : ℕ} {K : Set (E d)}
    (hK : Convex ℝ K) (hKm : MeasurableSet K) :
    ∀ᵐ x ∂uniformMeasure K, x ∈ interior K := by
…

theorem OAI.Problem358.ae_differentiableAt_uniformMeasure line 202

Source documentation

Rademacher's theorem on a convex source, upgraded from within-derivatives using the nullity of the boundary of a convex set. No regular boundary is needed.

theorem ae_differentiableAt_uniformMeasure {d : ℕ} {K : Set (E d)}
    {u : E d → ℝ} {L : ℝ≥0}
    (hK : Convex ℝ K) (hKm : MeasurableSet K)
    (hu : LipschitzOnWith L u K) :
    ∀ᵐ x ∂uniformMeasure K, x ∈ interior K ∧ DifferentiableAt ℝ u x := by
…

theorem OAI.Problem358.hasFDerivAt_eq_innerSL_of_supporting line 235

Source documentation

A supporting slope on a neighborhood is the derivative.

theorem hasFDerivAt_eq_innerSL_of_supporting
    {u : H → ℝ} {D : H →L[ℝ] ℝ} {K : Set H} {x p : H}
    (hu : HasFDerivAt u D x) (hx : x ∈ interior K)
    (hp : ∀ z ∈ K, u x + ⟪p, z - x⟫ ≤ u z) :
    D = innerSL ℝ p := by
…

theorem OAI.Problem358.hasFDerivAt_apply_eq_inner_of_supporting line 250

Source documentation

Evaluated form of the supporting-slope identification.

theorem hasFDerivAt_apply_eq_inner_of_supporting
    {u : H → ℝ} {D : H →L[ℝ] ℝ} {K : Set H} {x p : H}
    (hu : HasFDerivAt u D x) (hx : x ∈ interior K)
    (hp : ∀ z ∈ K, u x + ⟪p, z - x⟫ ≤ u z) (v : H) :
    D v = ⟪p, v⟫ := by
…

theorem OAI.Problem358.supporting_slope_unique line 259

Source documentation

Supporting slopes are unique at an interior differentiability point.

theorem supporting_slope_unique
    {u : H → ℝ} {K : Set H} {x p q : H}
    (hu : DifferentiableAt ℝ u x) (hx : x ∈ interior K)
    (hp : ∀ z ∈ K, u x + ⟪p, z - x⟫ ≤ u z)
    (hq : ∀ z ∈ K, u x + ⟪q, z - x⟫ ≤ u z) : p = q := by
…

theorem OAI.Problem358.supporting_of_fenchel_eq line 270

Source documentation

Equality in a Fenchel inequality produces a supporting slope.

theorem supporting_of_fenchel_eq
    {u : H → ℝ} {v : H → ℝ} {K : Set H} {x y : H}
    (hdual : ∀ z ∈ K, ⟪z, y⟫ ≤ u z + v y)
    (heq : ⟪x, y⟫ = u x + v y) :
    ∀ z ∈ K, u x + ⟪y, z - x⟫ ≤ u z := by
…

theorem OAI.Problem358.eq_supporting_slope_of_fenchel_eq line 282

Source documentation

At an interior differentiability point, equality in a Fenchel certificate forces the target coordinate to equal any known supporting slope.

theorem eq_supporting_slope_of_fenchel_eq
    {u : H → ℝ} {v : H → ℝ} {K : Set H} {x p y : H}
    (hu : DifferentiableAt ℝ u x) (hx : x ∈ interior K)
    (hp : ∀ z ∈ K, u x + ⟪p, z - x⟫ ≤ u z)
    (hdual : ∀ z ∈ K, ⟪z, y⟫ ≤ u z + v y)
    (heq : ⟪x, y⟫ = u x + v y) : y = p :=
…

theorem OAI.Problem358.uniform_ae_supporting_slope_unique line 308

Source documentation

Source-a.e. supporting-slope uniqueness for the exact uniform normalization.

theorem uniform_ae_supporting_slope_unique
    {d : ℕ} {K : Set (E d)} {u : E d → ℝ} {L : ℝ≥0}
    (hK : Convex ℝ K) (hKm : MeasurableSet K) (hu : LipschitzOnWith L u K) :
    ∀ᵐ x ∂uniformMeasure K, ∀ p q : E d,
      (∀ z ∈ K, u x + ⟪p, z - x⟫ ≤ u z) →
      (∀ z ∈ K, u x + ⟪q, z - x⟫ ≤ u z) → p = q := by
…

theorem OAI.Problem358.uniform_ae_eq_supporting_map_of_fenchel_eq line 320

Source documentation

A Fenchel equality locus is the graph of a known supporting map, source-almost everywhere. This is the pointwise input for uniqueness of plans.

theorem uniform_ae_eq_supporting_map_of_fenchel_eq
    {d : ℕ} {K Y : Set (E d)} {u v : E d → ℝ} {T : E d → E d} {L : ℝ≥0}
    (hK : Convex ℝ K) (hKm : MeasurableSet K) (hu : LipschitzOnWith L u K)
    (hT : ∀ᵐ x ∂uniformMeasure K, ∀ z ∈ K, u x + ⟪T x, z - x⟫ ≤ u z)
    (hdual : ∀ y ∈ Y, ∀ z ∈ K, ⟪z, y⟫ ≤ u z + v y) :
    ∀ᵐ x ∂uniformMeasure K, ∀ y ∈ Y,
      ⟪x, y⟫ = u x + v y → y = T x := by
…