OAI/GroupTheory/Thompson/AnalyticNormalization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThompsonNonamenability.Analytic.normalizeNeg line 18

   Source documentation

   Negative radial normalization, with the field's usual value at zero.

   def normalizeNeg (z : E) : E := -(‖z‖⁻¹ • z)

2. theorem OAI.ThompsonNonamenability.Analytic.norm_normalizeNeg line 20
3. theorem OAI.ThompsonNonamenability.Analytic.abs_inv_sub_mul line 26

   Source documentation

   A scalar identity used to avoid any estimate depending on the larger norm.

   private theorem abs_inv_sub_mul {a b : ℝ} (ha : 0 < a) (hb : 0 < b) :
       |a⁻¹ - b⁻¹| * b = |b - a| / a := by
   …

   Mentions: OAI.ThompsonNonamenability.Analytic.a, OAI.ThompsonNonamenability.Analytic.b

4. theorem OAI.ThompsonNonamenability.Analytic.normalizeNeg_lipschitz line 34

   Source documentation

   Radial normalization is 2 / ε-Lipschitz where the norm is at least ε.

   theorem normalizeNeg_lipschitz {ε : ℝ} (hε : 0 < ε) {x y : E}
       (hx : ε ≤ ‖x‖) (hy : ε ≤ ‖y‖) :
       ‖normalizeNeg x - normalizeNeg y‖ ≤ (2 / ε) * ‖x - y‖ := by
   …

   Mentions: OAI.ThompsonNonamenability.Analytic.normalizeNeg

5. def OAI.ThompsonNonamenability.Analytic.normalizedMap line 66

   Source documentation

   Normalize the given nonvanishing map and retain the closed-ball carrier.

   def normalizedMap (G : UnitBall E → E) {ε : ℝ} (hε : 0 < ε)
       (hLower : ∀ x, ε ≤ ‖G x‖) : UnitBall E → UnitBall E :=
   …

   Mentions: OAI.ThompsonNonamenability.Analytic.G, OAI.ThompsonNonamenability.UnitBall

6. theorem OAI.ThompsonNonamenability.Analytic.coe_normalizedMap line 71
7. theorem OAI.ThompsonNonamenability.Analytic.norm_normalizedMap line 75
8. theorem OAI.ThompsonNonamenability.Analytic.normalizedMap_displacement line 81

   Source documentation

   The outer identity and unit normalization give a displacement of at least 1/2.

   theorem normalizedMap_displacement (G : UnitBall E → E) {ε : ℝ} (hε : 0 < ε)
       (hLower : ∀ x, ε ≤ ‖G x‖)
       (hOuter : ∀ x : UnitBall E, (1 / 2 : ℝ) ≤ ‖(x : E)‖ → G x = (x : E))
       (x : UnitBall E) :
       (1 / 2 : ℝ) ≤ ‖(normalizedMap G hε hLower x : E) - (x : E)‖ := by
   …

   Mentions: OAI.ThompsonNonamenability.Analytic.G, OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.Analytic.normalizedMap

9. theorem OAI.ThompsonNonamenability.Analytic.normalizedMap_lipschitz line 104

   Source documentation

   The concrete normalized map inherits the advertised Lipschitz estimate.

   theorem normalizedMap_lipschitz (G : UnitBall E → E) {ε C : ℝ} (hε : 0 < ε)
       (hLower : ∀ x, ε ≤ ‖G x‖)
       (hLip : ∀ x y : UnitBall E, ‖G x - G y‖ ≤ C * ‖(x : E) - (y : E)‖)
       (x y : UnitBall E) :
       ‖(normalizedMap G hε hLower x : E) - (normalizedMap G hε hLower y : E)‖ ≤
         (2 * C / ε) * ‖(x : E) - (y : E)‖ := by
   …

   Mentions: OAI.ThompsonNonamenability.Analytic.G, OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.Analytic.normalizedMap