OAI/Analysis/CircleDomains/Selection/BandStability.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Stability of bands under boundary-vanishing approximation

The smoothing step in Section 6 changes a coordinate by an error tending to zero at every dust point. Its cluster values, interval bands and mod-one level incidences at those points are therefore exactly preserved. No regularity of either coordinate on the dust is required.

  1. theorem OAI.CircleDomainRigidity.tendsto_difference_of_vanishing_tolerance line 22
  2. theorem OAI.CircleDomainRigidity.tendsto_difference_of_distance_to_dust line 33

    Source documentation

    The distance-to-dust tolerance used for smoothing really vanishes at every dust point, including accumulation points of the dust.

    theorem tendsto_difference_of_distance_to_dust
    {X : Type*} [MetricSpace X] {G B : Set X} {f g : X → ℝ}
    {x : X} (hx : x ∈ B) {C : ℝ}
    (herror : ∀ y ∈ G, |f y - g y| ≤ C * Metric.infDist y B) :
    Tendsto (fun y => f y - g y) (𝓝[G] x) (𝓝 0) := by
…
  3. theorem OAI.CircleDomainRigidity.mapClusterPt_of_vanishing_difference line 43
  4. theorem OAI.CircleDomainRigidity.clusterGraph_fiber_eq_of_vanishing_difference line 54
  5. theorem OAI.CircleDomainRigidity.intervalBand_fiber_eq_of_vanishing_difference line 66
  6. theorem OAI.CircleDomainRigidity.circleBand_fiber_eq_of_vanishing_difference line 78