OAI/Analysis/AffineBernstein/FixedBasisCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.targetBasisCoordinates line 14
2. lemma OAI.AffineBernstein.targetBasisCoordinates_map line 17
3. lemma OAI.AffineBernstein.targetBasisCoordinates_det line 20
4. lemma OAI.AffineBernstein.pulledBaseGraphFunction_coefficients line 47

   Source documentation

   Restriction of a pulled target-base covector to the original graph is literally affine in the original ambient coordinates. The coefficients are derived, not postulated.

   lemma pulledBaseGraphFunction_coefficients {n : ℕ} (u : Space n → ℝ)
       (a : Space n × ℝ) (L : (S × E) ≃L[ℝ] (Space n × ℝ)) (ℓ : S →L[ℝ] ℝ) :
       ∃ (α : Space n →L[ℝ] ℝ) (β d : ℝ),
         pulledBaseGraphFunction u a L ℓ = graphAffineFunction u α β d ∧
         ∀ p : Space n × ℝ, ℓ (L.symm (p-a)).1 = α p.1 + β*p.2+d := by
   …

   Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.pulledBaseGraphFunction, OAI.AffineBernstein.graphAffineFunction

5. lemma OAI.AffineBernstein.inverseMatrixPair_graphAffineFunction line 73