BandMeasure.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Haar measure of a projected band

The projection of a real interval of length b - a is contained in the circle ball with midpoint (a + b) / 2 and radius (b - a) / 2. This gives the manuscript's band-incidence bound, including long bands.

theorem OAI.CircleDomainRigidity.addCircle_image_Icc_subset_closedBall line 19
theorem OAI.CircleDomainRigidity.volume_addCircle_image_Icc_le line 28
theorem OAI.CircleDomainRigidity.circleBandGraph_fiber_eq_image_realFiber line 36
theorem OAI.CircleDomainRigidity.measurableSet_circleBandIncidence line 50

theorem OAI.CircleDomainRigidity.volume_circleBandGraph_incidence_le_budget line 58

Source documentation

The band-incidence estimate in the coordinates used by the paper: the budget bounds the difference of the actual upper and lower limits.

theorem volume_circleBandGraph_incidence_le_budget
    {X : Type*} [TopologicalSpace X] [FirstCountableTopology X]
    [CompactSpace X] [T2Space X]
    {G : Set X} {f : X → ℝ} {M : ℝ} (hM : ∀ y ∈ G, |f y| ≤ M)
    {x : X} (hx : x ∈ closure G) {a : ℝ}
    (hbudget : Filter.limsup f (𝓝[G] x) - Filter.liminf f (𝓝[G] x) ≤ a) :
    volume {t : AddCircle (1 : ℝ) | (x, t) ∈ circleBandGraph G f} ≤
      ENNReal.ofReal a := by
…

Mentions: OAI.CircleDomainRigidity.circleBandGraph

theorem OAI.CircleDomainRigidity.volume_circleBandGraph_fiber_le line 73

Source documentation

The bound required by weighted dust incidence, specialized to the actual compact interval fibers of the band graph.

theorem volume_circleBandGraph_fiber_le
    {X : Type*} [TopologicalSpace X] [CompactSpace X] [T2Space X]
    {G : Set X} {f : X → ℝ} {M : ℝ} (hM : ∀ y ∈ G, |f y| ≤ M)
    {x : X} (hx : x ∈ closure G) {a : ℝ}
    (hbudget : sSup {t : ℝ | (x, t) ∈ clusterGraph G f} -
      sInf {t : ℝ | (x, t) ∈ clusterGraph G f} ≤ a) :
    volume {t : AddCircle (1 : ℝ) | (x, t) ∈ circleBandGraph G f} ≤
      ENNReal.ofReal a := by
…

Mentions: OAI.CircleDomainRigidity.clusterGraph, OAI.CircleDomainRigidity.circleBandGraph