GaussCoordinates.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.AffineBernstein.homogeneousSupport line 17
Source comment
The one-homogeneous extension of the literal spherical support function.
```
def homogeneousSupport (K : Set E) (e : E) : ℝ :=
…
```
def OAI.AffineBernstein.gaussPoint line 21
Source comment
The actual support point, reconstructed by the derivative of the support value.
```
def gaussPoint (K : Set E) (e : E) : E := gradient (homogeneousSupport K) e
```
Mentions: OAI.AffineBernstein.homogeneousSupport
theorem OAI.AffineBernstein.homogeneousSupport_le line 23
theorem OAI.AffineBernstein.homogeneousSupport_eq_of_max line 27
theorem OAI.AffineBernstein.gaussPoint_eq_of_max line 35
theorem OAI.AffineBernstein.gaussPoint_mem_support line 51
theorem OAI.AffineBernstein.homogeneousSupport_euler line 60
theorem OAI.AffineBernstein.homogeneousSupport_hessian_radial line 69
Source comment
Euler's identity differentiates to the radial null direction of the support Hessian. This is the ambient version of the spherical radius matrix.
```
theorem homogeneousSupport_hessian_radial {K : Set E} (hK : IsCompact K)
    (hne : K.Nonempty) {e : E} (hh : ContDiffAt ℝ ∞ (homogeneousSupport K) e)
    (v : E) : fderiv ℝ (fderiv ℝ (homogeneousSupport K)) e v e = 0 := by
…
```
Mentions: OAI.AffineBernstein.homogeneousSupport
theorem OAI.AffineBernstein.contDiffAt_gaussPoint_fibers line 89
theorem OAI.AffineBernstein.contDiffAt_homogeneousSupport_fibers line 96

theorem OAI.AffineBernstein.affineEpigraph_gauss_smooth line 109

Source comment

Actual smooth Gauss coordinates of each affine epigraph tube.

theorem affineEpigraph_gauss_smooth [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) :
    ContDiffAt ℝ ∞ (fun q : S × E =>
      gaussPoint {y | (q.1, y) ∈ affineEpigraphPullback Ω u a L} q.2) (s,e) := by
…

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