OAI/Analysis/AffineBernstein/ParametricInverseMetric.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.inverseMatrixPair_congruence line 16

   Source comment

   Covector contraction with the inverse second form is unchanged by an invertible coordinate change. This uses the actual matrix inverse.

   lemma inverseMatrixPair_congruence (A J : Matrix ι ι ℝ) (hJ : J.det ≠ 0)
       (v w : ι → ℝ) :
       inverseMatrixPair (J.transpose*A*J) (J.transpose.mulVec v) (J.transpose.mulVec w) =
         inverseMatrixPair A v w := by
   …

   Mentions: OAI.AffineBernstein.inverseMatrixPair

2. lemma OAI.AffineBernstein.inverseMatrixPair_smul_matrix line 30
3. lemma OAI.AffineBernstein.inverseMatrixPair_block_base line 43
4. def OAI.AffineBernstein.parametricInverseMetric line 58

   Source comment

   Inverse metric of an actual parametrization and an actual test function.

   def parametricInverseMetric {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       {n : ℕ} (X : Space n → E) (ν : E →L[ℝ] ℝ) (f : Space n → ℝ) (x : Space n) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

5. lemma OAI.AffineBernstein.derivative_coordinates_comp line 64
6. lemma OAI.AffineBernstein.parametricInverseMetric_comp line 77

   Source comment

   Exact coordinate invariance of the inverse second-form norm.

   lemma parametricInverseMetric_comp {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
       {n : ℕ} {X : Space n → E} {φ : Space n → Space n} {f : Space n → ℝ}
       {x : Space n} (hX : ContDiffAt ℝ ∞ X (φ x)) (hφ : ContDiffAt ℝ ∞ φ x)
       (hf : DifferentiableAt ℝ f (φ x)) (ν : E →L[ℝ] ℝ)
       (hν : ν.comp (fderiv ℝ X (φ x)) = 0) (hJ : (parametricJacobian φ x).det ≠ 0) :
       parametricInverseMetric (X ∘ φ) ν (f ∘ φ) x = parametricInverseMetric X ν f (φ x) := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.parametricJacobian, OAI.AffineBernstein.parametricInverseMetric