SupportGeometry.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.supportValue line 19
Source comment
The literal support value, not a freely chosen support coordinate.
```
def supportValue (K : Set E) (ℓ : E →L[ℝ] ℝ) : ℝ := sSup (ℓ '' K)
```

theorem OAI.AffineBernstein.convex_first_order line 22

Source comment

A supporting first-order inequality for an arbitrary differentiable convex function.

theorem convex_first_order {W : Set E} {F : E → ℝ} (hF : ConvexOn ℝ W F)
    {x y : E} (hx : x ∈ W) (hy : y ∈ W) (hd : DifferentiableAt ℝ F x) :
    fderiv ℝ F x (y - x) ≤ F y - F x := by
…

theorem OAI.AffineBernstein.sublevel_max_on_level line 41

Source comment

A nonzero linear functional cannot attain its sublevel maximum below the level.

theorem sublevel_max_on_level {W : Set E} (hW : IsOpen W) {F : E → ℝ}
    {ℓ : E →L[ℝ] ℝ} (hℓ : ℓ ≠ 0) {z : E} (hz : z ∈ W)
    (hzF : F z ≤ 0) (hc : ContinuousAt F z)
    (hmax : IsMaxOn ℓ {y | y ∈ W ∧ F y ≤ 0} z) : F z = 0 := by
…

theorem OAI.AffineBernstein.exists_support_multiplier line 54

Source comment

The support maximum of a compact smooth convex sublevel has a positive Lagrange multiplier. This includes dimension one without a sphere convention.

theorem exists_support_multiplier [CompleteSpace E] {W : Set E} (hW : IsOpen W) {F : E → ℝ}
    (hcv : ConvexOn ℝ W F) (hF : ContDiffOn ℝ ∞ F W)
    {x₀ : E} (hx₀ : x₀ ∈ W) (hneg : F x₀ < 0)
    (hK : IsCompact {y | y ∈ W ∧ F y ≤ 0})
    {ℓ : E →L[ℝ] ℝ} (hℓ : ℓ ≠ 0) :
    ∃ z ∈ W, F z = 0 ∧ ∃ lam : ℝ, 0 < lam ∧
      fderiv ℝ F z = lam • ℓ ∧
      (∀ y ∈ W, F y ≤ 0 → ℓ y ≤ ℓ z) ∧
      supportValue {y | y ∈ W ∧ F y ≤ 0} ℓ = ℓ z := by
…

Mentions: OAI.AffineBernstein.supportValue

def OAI.AffineBernstein.supportJacobian line 106

Source comment

Linearization of the actual support equations `F(y)=0`, `DF(y)=lam*ell`.

def supportJacobian (d : E →L[ℝ] ℝ) (H : E →L[ℝ] (E →L[ℝ] ℝ))
    (ℓ : E →L[ℝ] ℝ) : (E × ℝ) →L[ℝ] (ℝ × (E →L[ℝ] ℝ)) :=
…

theorem OAI.AffineBernstein.supportJacobian_apply line 112

theorem OAI.AffineBernstein.supportJacobian_injective line 117

Source comment

Positive curvature gives the missing transversality of the support equations.

theorem supportJacobian_injective {d : E →L[ℝ] ℝ}
    {H : E →L[ℝ] (E →L[ℝ] ℝ)} {ℓ : E →L[ℝ] ℝ} {lam : ℝ}
    (hℓ : ℓ ≠ 0) (hlam : lam ≠ 0) (hd : d = lam • ℓ)
    (hH : ∀ v : E, v ≠ 0 → 0 < H v v) :
    Function.Injective (supportJacobian d H ℓ) := by
…

Mentions: OAI.AffineBernstein.supportJacobian

theorem OAI.AffineBernstein.supportJacobian_isInvertible line 139
def OAI.AffineBernstein.fiberGradient line 159
Source comment
Fiber derivatives of the actual defining function.
```
def fiberGradient (F : S × E → ℝ) (p : S × E) : E →L[ℝ] ℝ :=
…
```
def OAI.AffineBernstein.supportEquations line 162
theorem OAI.AffineBernstein.contDiffAt_fiberGradient line 166
theorem OAI.AffineBernstein.contDiffAt_supportEquations line 171
theorem OAI.AffineBernstein.supportEquations_partial line 185

theorem OAI.AffineBernstein.supportValue_of_equations line 210

Source comment

A solution of the support equations with positive multiplier is a global, not merely local, support point.

theorem supportValue_of_equations {W : Set E} {F : E → ℝ}
    (hcv : ConvexOn ℝ W F) {z : E} (hz : z ∈ W) (hzF : F z = 0)
    (hd : DifferentiableAt ℝ F z) {ℓ : E →L[ℝ] ℝ} {lam : ℝ}
    (hlam : 0 < lam) (he : fderiv ℝ F z = lam • ℓ) :
    supportValue {y | y ∈ W ∧ F y ≤ 0} ℓ = ℓ z := by
…

Mentions: OAI.AffineBernstein.supportValue

theorem OAI.AffineBernstein.contDiffAt_supportValue_fibers line 228

Source comment

Smooth dependence of the literal support value on base and conormal. The IFT is applied to the actual defining function and its actual Hessian.

theorem contDiffAt_supportValue_fibers [FiniteDimensional ℝ E] [CompleteSpace S]
    {B : Set S} (hB : IsOpen B) {W : Set (S × E)} (hW : IsOpen W)
    {F : S × E → ℝ} (hF : ContDiffOn ℝ ∞ F W)
    (hcv : ∀ s ∈ B, ConvexOn ℝ {y | (s, y) ∈ W} (fun y => F (s, y)))
    {s : S} (hs : s ∈ B) {x₀ : E} (hx₀ : (s, x₀) ∈ W) (hneg : F (s, x₀) < 0)
    (hK : IsCompact {y | (s, y) ∈ W ∧ F (s, y) ≤ 0})
    (hH : ∀ y, (s, y) ∈ W → F (s, y) = 0 → ∀ v : E, v ≠ 0 →
      0 < fderiv ℝ (fderiv ℝ (fun z => F (s, z))) y v v)
    {ℓ : E →L[ℝ] ℝ} (hℓ : ℓ ≠ 0) :
    ContDiffAt ℝ ∞ (fun q : S × (E →L[ℝ] ℝ) =>
      supportValue {y | (q.1, y) ∈ W ∧ F (q.1, y) ≤ 0} q.2) (s, ℓ) := by
…

Mentions: OAI.AffineBernstein.supportValue

theorem OAI.AffineBernstein.le_supportValue line 278
Source comment
Finiteness of the literal support value on a compact fiber.
```
theorem le_supportValue {K : Set E} (hK : IsCompact K) {z : E} (hz : z ∈ K)
    (ℓ : E →L[ℝ] ℝ) : ℓ z ≤ supportValue K ℓ := by
…
```
Mentions: OAI.AffineBernstein.supportValue

theorem OAI.AffineBernstein.supportValue_fderiv line 284

Source comment

The envelope identity recovers the Gauss parametrization from the literal support function; no choice of a surrogate support coordinate is involved.

theorem supportValue_fderiv {K : Set E} (hK : IsCompact K)
    {z : E} (hz : z ∈ K) {ℓ : E →L[ℝ] ℝ}
    (hmax : supportValue K ℓ = ℓ z) (hd : DifferentiableAt ℝ (supportValue K) ℓ) :
    fderiv ℝ (supportValue K) ℓ = ContinuousLinearMap.apply ℝ ℝ z := by
…

Mentions: OAI.AffineBernstein.supportValue

theorem OAI.AffineBernstein.supportValue_pos line 298