OAI/GroupTheory/PolycyclicRecognition/Analysis/SupportTemplates.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Support exponents of compact templates

The support exponent is the finite maximum of word-basis exponents, with each letter allowed its own supporting point. Balance gives translation invariance, and segments recover the support norm.

  1. def OAI.PolycyclicRecognition.SupportDatum.weightSupport line 26
  2. def OAI.PolycyclicRecognition.SupportDatum.basisTemplateSupport line 28
  3. def OAI.PolycyclicRecognition.SupportDatum.templateSupport line 31
  4. theorem OAI.PolycyclicRecognition.SupportDatum.weight_le_weightSupport line 35
  5. theorem OAI.PolycyclicRecognition.SupportDatum.exists_weightSupport_point line 40
  6. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_translate line 45
  7. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_convexHull line 60
  8. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_segment line 76
  9. theorem OAI.PolycyclicRecognition.SupportDatum.basisTemplateSupport_translate line 86
  10. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_translate line 92
  11. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_convexHull line 96
  12. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_segment line 104
  13. theorem OAI.PolycyclicRecognition.SupportDatum.basisTemplateSupport_nonneg line 112
  14. theorem OAI.PolycyclicRecognition.SupportDatum.basisTemplateSupport_le line 121
  15. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_le line 126
  16. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_nonneg line 130
  17. theorem OAI.PolycyclicRecognition.SupportDatum.weightSupport_le_of_nearby line 138

    Source documentation

    Nearby support positions change each letter exponent by at most the operator norm of that letter times the error in position.

    theorem weightSupport_le_of_nearby {E F : Set W} (hE : IsCompact E) (hneE : E.Nonempty)
    (hF : IsCompact F) {δ : ℝ}
    (hnear : ∀ x ∈ E, ∃ y ∈ F, ‖x - y‖ ≤ δ) (i : I) :
    D.weightSupport E i ≤ D.weightSupport F i + ‖(D.weight i).toContinuousLinearMap‖ * δ := by
…
  18. def OAI.PolycyclicRecognition.SupportDatum.templateSupportConstant line 154

    Source documentation

    A fixed Lipschitz constant for the full template support.

    def templateSupportConstant : ℝ :=
…
  19. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupportConstant_nonneg line 158
  20. theorem OAI.PolycyclicRecognition.SupportDatum.templateSupport_le_of_nearby line 162
  21. theorem OAI.PolycyclicRecognition.SupportDatum.abs_templateSupport_sub_le_of_nearby line 189

    Source documentation

    The form needed when the two compact height ranges approximate one another, as in the forward/inverse stationary path comparison.

    theorem abs_templateSupport_sub_le_of_nearby {E F : Set W}
    (hE : IsCompact E) (hneE : E.Nonempty) (hF : IsCompact F) (hneF : F.Nonempty)
    {δ : ℝ} (hδ : 0 ≤ δ)
    (hEF : ∀ x ∈ E, ∃ y ∈ F, ‖x - y‖ ≤ δ)
    (hFE : ∀ y ∈ F, ∃ x ∈ E, ‖y - x‖ ≤ δ) :
    |D.templateSupport E - D.templateSupport F| ≤ D.templateSupportConstant * δ := by
…
  22. theorem OAI.PolycyclicRecognition.SupportDatum.abs_templateSupport_sub_le_hausdorffDist line 201

    Source documentation

    The template exponent is Lipschitz for Hausdorff distance on nonempty compact sets, with one constant depending only on the finite word data.

    theorem abs_templateSupport_sub_le_hausdorffDist {E F : Set W}
    (hE : IsCompact E) (hneE : E.Nonempty) (hF : IsCompact F) (hneF : F.Nonempty) :
    |D.templateSupport E - D.templateSupport F| ≤
      D.templateSupportConstant * Metric.hausdorffDist E F := by
…