OAI/Analysis/AffineBernstein/ActualFlatInverse.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.pulledBaseGraphFunction line 20
2. lemma OAI.AffineBernstein.contDiffAt_pulledBaseGraphFunction line 25
3. theorem OAI.AffineBernstein.affineEpigraph_flat_inverseMetric_transport line 35

   Source comment

   Actual pointwise inverse-B identity in every smooth flat support chart. The conormal normalization is derived from the original graph and support Gauss equations. There is no assumed inverse-metric or stationarity law.

   theorem affineEpigraph_flat_inverseMetric_transport {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})
       (q₀ : S × E) (J : Space n →L[ℝ] (S × E))
       (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
       (e : Fin n ≃ ι ⊕ κ) (hJe : ∀ i, J (coordinateVector n i) = tubeTangent bS bE (e i))
       {φ : Space n → Space n} {x : Space n} (hφ : ContDiffAt ℝ ∞ φ x)
       (hJφ : (parametricJacobian φ x).det ≠ 0) (hx : (q₀+J x).1 ∈ B)
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.affineEpigraphPullback, OAI.AffineBernstein.coordinateVector, OAI.AffineBernstein.tubeTangent, OAI.AffineBernstein.parametricJacobian