OAI/Analysis/AffineBernstein/ActualInverseMetric.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.graphConormalAt line 15
2. lemma OAI.AffineBernstein.graphConormalAt_null line 20
3. lemma OAI.AffineBernstein.parametricSecondForm_graph line 26
4. lemma OAI.AffineBernstein.parametricInverseMetric_graph line 42
5. theorem OAI.AffineBernstein.graph_chart_inverseMetric_transport line 55

   Source comment

   Pointwise norm transport in an arbitrary smooth graph chart. The factor is the norm of the ACTUAL conormal, not its vertical component.

   theorem graph_chart_inverseMetric_transport {n : ℕ} {u f : Space n → ℝ}
       {φ : Space n → Space n} {x : Space n}
       (hu : ContDiffAt ℝ ∞ u (φ x)) (hφ : ContDiffAt ℝ ∞ φ x)
       (hH : (hessian u (φ x)).det ≠ 0) (hJ : (parametricJacobian φ x).det ≠ 0)
       (hf : DifferentiableAt ℝ f (φ x))
       {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       (L : E ≃L[ℝ] (Space n × ℝ)) (a : Space n × ℝ)
       {X : Space n → E} (he : (fun y => a+L (X y)) =ᶠ[nhds x] (fun y => (φ y,u (φ y))))
       (c : ℝ) (hc : 0 < c) :
       let ζ := (graphConormalAt u (φ x)).comp L.toContinuousLinearMap
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.parametricJacobian, OAI.AffineBernstein.graphConormalAt