OAI/Analysis/AffineBernstein/ActualAmbientFEquation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.affineMaximal_flat_invariant_f_equation line 21
2. theorem OAI.AffineBernstein.affineMaximal_invariant_tube_f_equation line 130

   Source comment

   The invariant support f-equation, with all flat-normal chart data produced from the actual frames. At a unit normal it is the round-sphere equation, since the actual invariant scalar has zero radial derivative.

   theorem affineMaximal_invariant_tube_f_equation {n : ℕ} {Ω : Set (Space n)}
       (hΩ : IsOpen Ω) (hcv : Convex ℝ Ω) {u : Space n → ℝ}
       (hu : ContDiffOn ℝ ∞ u Ω) (hp : ∀ x ∈ Ω, (hessian u x).PosDef)
       (hm : AffineMaximalOn Ω u)
       (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ))
       {D : Set S} (hD : IsOpen D)
       (hK : ∀ s ∈ D, IsCompact {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
       (hzero : ∀ s ∈ D, (0 : E) ∈ interior {y | (s,y) ∈ affineEpigraphPullback Ω u a L})
       {s : S} (hs : s ∈ D) {e : E}
       (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
       (he : bE (Sum.inr ()) = e) :
       let H := fun q : S × E => homogeneousSupport {y | (q.1,y) ∈ affineEpigraphPullback Ω u a L} q.2
   …

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