ActualBaseCurvature.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.affineDefining line 17
Source comment
The genuine defining function for any affine coordinates of the graph.
```
def affineDefining {n : ℕ} (u : Space n → ℝ) (a : Space n × ℝ)
    (L : V ≃L[ℝ] (Space n × ℝ)) (p : V) : ℝ := u (a + L p).1 - (a + L p).2
```
Mentions: OAI.AffineBernstein.Space
theorem OAI.AffineBernstein.affineDefining_deriv line 20
theorem OAI.AffineBernstein.affineDefining_second line 33

theorem OAI.AffineBernstein.affineDefining_tangent_curvature line 44

Source comment

Positive curvature on the tangent hyperplane, including affine maps that mix the original vertical direction with the new base and fiber coordinates.

theorem affineDefining_tangent_curvature {n : ℕ} {u : Space n → ℝ} (a : Space n × ℝ)
    (L : V ≃L[ℝ] (Space n × ℝ)) {p : V}
    (hu : ContDiffAt ℝ ∞ u (a + L p).1) (hp : (hessian u (a + L p).1).PosDef)
    {v : V} (hv : v ≠ 0) (ht : fderiv ℝ (affineDefining u a L) p v = 0) :
    0 < fderiv ℝ (fderiv ℝ (affineDefining u a L)) p v v := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineDefining

theorem OAI.AffineBernstein.affineEpigraph_gauss_equations line 64

Source comment

The actual support point is on the original graph and its fiber conormal is positive. No Gauss inverse or support-equation hypotheses are assumed.

theorem affineEpigraph_gauss_equations [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) :
    let Y := gaussPoint {y | (s,y) ∈ affineEpigraphPullback Ω u a L} e
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.gaussPoint

theorem OAI.AffineBernstein.affineEpigraph_base_hessian_negative line 149

Source comment

Strict negativity of the base Hessian of the literal support function. This is the other positive block of the genuine tube second fundamental form.

theorem affineEpigraph_base_hessian_negative [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 : S} (hv : v ≠ 0) :
    fderiv ℝ (fderiv ℝ (fun r => homogeneousSupport
      {y | (r,y) ∈ affineEpigraphPullback Ω u a L} e)) s v v < 0 := by
…

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