OAI/Analysis/AffineBernstein/FlatInverseMetric.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.inverseMatrixPair_equiv line 18
2. lemma OAI.AffineBernstein.parametricSecondForm_flatSupport line 32
3. theorem OAI.AffineBernstein.parametricInverseMetric_flat_base line 60

   Source comment

   The inverse second-form norm of a base affine coordinate in the literal flat support chart is exactly the inverse-B contraction, not a surrogate.

   theorem parametricInverseMetric_flat_base {n : ℕ} {H : S × E → ℝ} {Y : S × E → E}
       (q₀ : S × E) (J : Space n →L[ℝ] (S × E)) {x : Space n}
       (hH : ContDiffAt ℝ ∞ H (q₀+J x)) (hY : ContDiffAt ℝ ∞ Y (q₀+J x))
       (heul : H =ᶠ[nhds (q₀+J x)] (fun q => inner ℝ q.2 (Y q)))
       (hgrad : ∀ᶠ q in nhds (q₀+J x), ∀ z : E, fderiv ℝ H q (0,z) = inner ℝ (Y q) z)
       (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
       (e : Fin n ≃ ι ⊕ κ) (hJ : ∀ i, J (coordinateVector n i) = tubeTangent bS bE (e i))
       (hB : (tubeBaseMatrix H (q₀+J x) bS).det ≠ 0)
       (hR : (tubeRadiusMatrix H (q₀+J x) bE).det ≠ 0) (ℓ : S →L[ℝ] ℝ) :
       parametricInverseMetric (fun y => supportParam Y (q₀+J y))
         (supportConormal H (q₀+J x)) (fun y => ℓ (q₀+J y).1) x =
         inverseMatrixPair (tubeBaseMatrix H (q₀+J x) bS)
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.coordinateVector, OAI.AffineBernstein.tubeTangent, OAI.AffineBernstein.tubeBaseMatrix, OAI.AffineBernstein.tubeRadiusMatrix, OAI.AffineBernstein.parametricInverseMetric, OAI.AffineBernstein.supportParam, OAI.AffineBernstein.supportConormal, OAI.AffineBernstein.inverseMatrixPair