OAI/Analysis/AffineBernstein/LinearNormalizationCalculus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.cleMatrix line 18

   Source documentation

   The actual square matrix in the frozen Euclidean coordinates.

   def cleMatrix {n : ℕ} (A : Space n ≃L[ℝ] Space n) : Matrix (Fin n) (Fin n) ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

2. lemma OAI.AffineBernstein.cleMatrix_apply line 21
3. lemma OAI.AffineBernstein.cleMatrix_det_ne_zero line 25
4. def OAI.AffineBernstein.normalizedFunction line 40

   Source documentation

   Center-preserving horizontal normalization and positive vertical scaling.

   def normalizedFunction {n : ℕ} (u : Space n → ℝ) (A : Space n ≃L[ℝ] Space n)
       (t : ℝ) (y : Space n) : ℝ := t⁻¹ * u (A y)

   Mentions: OAI.AffineBernstein.Space

5. lemma OAI.AffineBernstein.normalizedFunction_eq_pullback line 43
6. lemma OAI.AffineBernstein.contDiff_normalizedFunction line 49
7. lemma OAI.AffineBernstein.hessian_normalizedFunction line 53
8. lemma OAI.AffineBernstein.posDef_hessian_normalizedFunction line 60
9. lemma OAI.AffineBernstein.affineMaximalOn_normalizedFunction line 67
10. lemma OAI.AffineBernstein.fderiv_normalizedFunction line 75
11. lemma OAI.AffineBernstein.tangentHeight_normalizedFunction line 80
12. lemma OAI.AffineBernstein.sectionBalance_normalizedFunction line 88