OAI/Analysis/AffineBernstein/AmbientStraightening.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.ambientCoordinates line 11
2. lemma OAI.AffineBernstein.ambientCoordinates_inl line 14
3. lemma OAI.AffineBernstein.ambientCoordinates_inr line 18
4. def OAI.AffineBernstein.ambientSwap line 22
5. lemma OAI.AffineBernstein.ambientSwap_coordinates line 26
6. lemma OAI.AffineBernstein.ambientSwap_involutive line 32
7. lemma OAI.AffineBernstein.abs_det_involutive line 39
8. lemma OAI.AffineBernstein.abs_det_trans line 52
9. theorem OAI.AffineBernstein.bounded_ambient_straightening line 62

   Source documentation

   A determinant-one-in-absolute-value coordinate change straightens any nonzero vector upwards, with a uniform factor two bound on coordinate boxes. No Euclidean structure is falsely assigned to the max-norm product.

   theorem bounded_ambient_straightening {n : ℕ} {e : Space n × ℝ} (he : e ≠ 0) :
       ∃ (A : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (c : ℝ),
         0 < c ∧ A e = (0,c) ∧ |A.toContinuousLinearMap.det| = 1 ∧
         ∀ {R : ℝ}, 0 ≤ R → ∀ z : Space n × ℝ,
           (∀ i, |z.1 i| ≤ R) → |z.2| ≤ R →
           (∀ i, |(A z).1 i| ≤ 2*R) ∧ |(A z).2| ≤ 2*R := by
   …

   Mentions: OAI.AffineBernstein.Space