OAI/Analysis/CircleDomains/Selection/BandGraph.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

+# Compact interval-band graphs for bounded real coordinates

Take the closure of the physical graph and fill the interval between cluster values in each fiber. This constructs a compact band graph; on the open physical domain it is exactly the original graph. Its projection modulo one consequently gives compact level sets with the correct physical fibers.

  1. def OAI.CircleDomainRigidity.clusterGraph line 19
  2. def OAI.CircleDomainRigidity.intervalFiberHull line 22
  3. theorem OAI.CircleDomainRigidity.isCompact_clusterGraph line 27
  4. theorem OAI.CircleDomainRigidity.isCompact_intervalFiberHull line 36
  5. theorem OAI.CircleDomainRigidity.mem_intervalFiberHull_iff line 44
  6. theorem OAI.CircleDomainRigidity.subset_intervalFiberHull line 57
  7. theorem OAI.CircleDomainRigidity.isCompact_real_fiber line 63
  8. theorem OAI.CircleDomainRigidity.intervalFiberHull_fiber_eq_Icc line 81

    Source documentation

    The interpolated fiber is exactly the interval between the smallest and largest cluster values, with the endpoints attained in the compact original fiber.

    theorem intervalFiberHull_fiber_eq_Icc
    {X : Type*} [TopologicalSpace X] [T2Space X] {K : Set (X × ℝ)}
    (hK : IsCompact K) (x : X) (hne : {t : ℝ | (x, t) ∈ K}.Nonempty) :
    {t : ℝ | (x, t) ∈ intervalFiberHull K} =
      Icc (sInf {t : ℝ | (x, t) ∈ K}) (sSup {t : ℝ | (x, t) ∈ K}) := by
…

    Mentions: OAI.CircleDomainRigidity.intervalFiberHull

  9. theorem OAI.CircleDomainRigidity.clusterGraph_fiber_nonempty_of_mem_closure line 112
  10. theorem OAI.CircleDomainRigidity.clusterGraph_fiber_eq_of_continuousAt line 124
  11. theorem OAI.CircleDomainRigidity.intervalFiberHull_clusterGraph_on_open line 134
  12. def OAI.CircleDomainRigidity.circleBandGraph line 148
  13. theorem OAI.CircleDomainRigidity.isCompact_circleBandGraph line 153
  14. theorem OAI.CircleDomainRigidity.circleBandGraph_on_open line 159
  15. theorem OAI.CircleDomainRigidity.isCompact_circleBandLevel line 171
  16. theorem OAI.CircleDomainRigidity.isCompact_circleBandIncidence line 176