OAI/NumberTheory/DukePrimeDegree/Geometry/ConjugationRadius.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quantitative conjugation of local matrix balls

The logarithmic displacement length gives an explicit exponential loss when a local quotient chart is transported by a group element.

  1. lemma OAI.DukePrimeDegree.matrix_entry_abs_le_operator_norm line 17
  2. lemma OAI.DukePrimeDegree.matrix_operator_norm_le_card_mul line 26
  3. lemma OAI.DukePrimeDegree.specialLinear_norm_le_exp_length line 38
  4. lemma OAI.DukePrimeDegree.conjugation_matrixBall_exp_bound line 46
  5. lemma OAI.DukePrimeDegree.localInjectivityAt_exp_translate line 87
  6. theorem OAI.DukePrimeDegree.exists_uniform_logarithmic_injectivity_radius line 93

    Source documentation

    Explicit exponential chart radii on every logarithmic-distance ball.

    theorem exists_uniform_logarithmic_injectivity_radius {n : ℕ} (hn : 0 < n) :
    ∃ r > 0, ∀ (R : ℝ) (x : X n),
      quotientLogDistance (Quotient.mk _ (1 : G n)) x ≤ R →
      LocalInjectivityAt (r/(2*(n:ℝ)*Real.exp (2*(R+1)))) x := by
…

    Mentions: OAI.DukePrimeDegree.quotientLogDistance, OAI.DukePrimeDegree.LocalInjectivityAt