OAI/GroupTheory/Thompson/CorrectionData.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Elementary inputs and explicit formula for the tube correction

Every field below is a scalar, curve, or rotation identity/estimate. In particular, no property of the corrected map is included in the inputs.

  1. structure OAI.ThompsonNonamenability.Analytic.CorrectionData line 26
  2. def OAI.ThompsonNonamenability.Analytic.CorrectionData.change line 52

    Source documentation

    The additive change on the actual, uniquely parameterized open tube.

    def change (x : C.tube) : E :=
…
  3. def OAI.ThompsonNonamenability.Analytic.CorrectionData.inside line 57

    Source documentation

    The actual correction inside the tube.

    def inside (x : C.tube) : E := (x : E) + D.change x
  4. def OAI.ThompsonNonamenability.Analytic.CorrectionData.G line 60

    Source documentation

    Gluing to the identity outside the open tube, including its boundary.

    def G (x : E) : E := by
…
  5. theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.G_of_mem line 64
  6. theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.G_of_not_mem line 67
  7. theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_radial line 70
  8. theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.curve_zero line 84
  9. theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.norm_curve line 87
  10. theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.q_eq_zero line 90
  11. theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.radial_eq_min line 93