ActualAngularSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AffineBernstein.homogeneousSupport_cofactor_divergence line 18
theorem OAI.AffineBernstein.gaussPoint_sublevel_equations line 26

theorem OAI.AffineBernstein.support_hessian_pos_of_equations line 46

Source comment

Local differential form of strict curvature duality: the Hessian of a one-homogeneous support is positive on every nonzero tangent vector.

theorem support_hessian_pos_of_equations {H F lam : E → ℝ} {e : E}
    (hh : ContDiffAt ℝ ∞ H e) (hF : ContDiffAt ℝ ∞ F (gradient H e))
    (hl : DifferentiableAt ℝ lam e) (hlpos : 0 < lam e)
    (heq : (fun q => fderiv ℝ F (gradient H q)) =ᶠ[𝓝 e]
      (fun q => lam q • InnerProductSpace.toDual ℝ E q))
    (hlevel : (fun q => F (gradient H q)) =ᶠ[𝓝 e] (fun _ => (0 : ℝ)))
    (hpos : ∀ z : E, z ≠ 0 → 0 <
      fderiv ℝ (fderiv ℝ F) (gradient H e) z z)
    {v : E} (hv : v ≠ 0) (ht : inner ℝ e v = 0) :
    0 < fderiv ℝ (fderiv ℝ H) e v v := by
…

theorem OAI.AffineBernstein.homogeneousSupport_hessian_pos line 95

Source comment

Strict positivity of the actual homogeneous support Hessian on tangent vectors. The multiplier is constructed from the actual Gauss point, not given as a differential identity hypothesis.

theorem homogeneousSupport_hessian_pos {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 : E} (he : e ≠ 0)
    (hh : ContDiffAt ℝ ∞ (homogeneousSupport {y | y ∈ W ∧ F y ≤ 0}) e)
    (hpos : ∀ y ∈ W, F y = 0 → ∀ z : E, z ≠ 0 →
      0 < fderiv ℝ (fderiv ℝ F) y z z)
    {v : E} (hv : v ≠ 0) (ht : inner ℝ e v = 0) :
    0 < fderiv ℝ (fderiv ℝ (homogeneousSupport {y | y ∈ W ∧ F y ≤ 0})) e v v := by
…

Mentions: OAI.AffineBernstein.homogeneousSupport

theorem OAI.AffineBernstein.affineEpigraph_radius_positive line 156

Source comment

Positive angular radius comes from the actual original graph Hessian, after any invertible affine change of coordinates with compact centered fibers.

theorem affineEpigraph_radius_positive [FiniteDimensional ℝ E] [Nontrivial E]
    {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω)
    {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
    (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
    {B : Set S} (hB : IsOpen B)
    (hK : ∀ s ∈ B, IsCompact {y | (s, y) ∈ affineEpigraphPullback Ω u a L})
    (hzero : ∀ s ∈ B, (0 : E) ∈ interior {y | (s, y) ∈ affineEpigraphPullback Ω u a L})
    {s : S} (hs : s ∈ B) {e : E} (he : e ≠ 0)
    {v : E} (hv : v ≠ 0) (ht : inner ℝ e v = 0) :
    0 < sphereRadius (homogeneousSupport
      {y | (s,y) ∈ affineEpigraphPullback Ω u a L}) e v v := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.sphereRadius, OAI.AffineBernstein.homogeneousSupport