OAI/Analysis/AffineBernstein/GaussSurjectivity.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.convex_sublevel_gradient_support line 22

   Source documentation

   The gradient of a convex defining function at a zero level point is an outward supporting covector, and cannot vanish when a strict sublevel point exists.

   lemma convex_sublevel_gradient_support {W : Set E} {F : E → ℝ}
       (hcv : ConvexOn ℝ W F) {y z : E} (hy : y ∈ W) (hz : z ∈ W)
       (hyF : F y = 0) (hzF : F z < 0) (hd : DifferentiableAt ℝ F y) :
       gradient F y ≠ 0 ∧ IsMaxOn (fun x => inner ℝ (gradient F y) x)
         {x | x ∈ W ∧ F x ≤ 0} y := by
   …

2. lemma OAI.AffineBernstein.gaussPoint_convex_sublevel line 44

   Source documentation

   Every zero-level boundary point is the true support gradient in its nonzero outward gradient direction; no parametrization surjectivity is assumed.

   lemma gaussPoint_convex_sublevel {W : Set E} {F : E → ℝ}
       (hcv : ConvexOn ℝ W F) {y z : E} (hy : y ∈ W) (hz : z ∈ W)
       (hyF : F y = 0) (hzF : F z < 0) (hd : DifferentiableAt ℝ F y)
       (hK : IsCompact {x | x ∈ W ∧ F x ≤ 0})
       (hh : DifferentiableAt ℝ (homogeneousSupport {x | x ∈ W ∧ F x ≤ 0})
         (gradient F y)) :
       gaussPoint {x | x ∈ W ∧ F x ≤ 0} (gradient F y) = y := by
   …

   Mentions: OAI.AffineBernstein.homogeneousSupport, OAI.AffineBernstein.gaussPoint