OAI/Analysis/AffineBernstein/ParametricBasis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.parametricAreaDensity_change_basis line 16
2. theorem OAI.AffineBernstein.affineMaximal_flatSupport_local_stationary line 39

   Source comment

   The literal PDE supplies stationarity on every actual flat-normal support chart. The chart inverse and conormal orientation are derived, not assumed.

   theorem affineMaximal_flatSupport_local_stationary {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 × ℝ))
       {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})
       (q₀ : S × E) (d : E) (hd : inner ℝ q₀.2 d = 1)
       (J : Space n →L[ℝ] (S × E)) (hi : Function.Injective J)
       (hJ : ∀ v, inner ℝ (J v).2 d = 0)
       (b : Module.Basis (Fin n ⊕ Unit) ℝ (S × E))
   …

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