LevelQuotient.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Restricting the quotient to a compact level union

The original quotient acts on the whole compact physical space. For a compact level union H, restrict it to π ⁻¹' H → H. Connected fibers remain connected, omitted points still map into compact totally disconnected dust, and the induced-metric Hausdorff length is exactly the physical length of (π ⁻¹' H) ∩ G.

def OAI.CircleDomainRigidity.levelQuotientMap line 20
theorem OAI.CircleDomainRigidity.continuous_levelQuotientMap line 23
theorem OAI.CircleDomainRigidity.surjective_levelQuotientMap line 29
theorem OAI.CircleDomainRigidity.connected_fibers_levelQuotientMap line 36

theorem OAI.CircleDomainRigidity.finite_large_continuum_bound_on_level line 60

Source documentation

The finite-continuum bound on an actual compact quotient level set, from its physical level length.

theorem finite_large_continuum_bound_on_level
    {X Y : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
    [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y]
    (π : Y → X) (hπ : Continuous π) (hsurj : Surjective π)
    (hfiber : ∀ x, IsConnected (π ⁻¹' {x}))
    {G : Set Y} (hG : IsOpen G) {B H : Set X}
    (hB : IsCompact B) (hTD : IsTotallyDisconnected B) (hdust : π '' Gᶜ ⊆ B)
    (hH : IsCompact H)
    (hlength : (μH[1] : Measure Y) ((π ⁻¹' H) ∩ G) < ∞) :
    HasFiniteLargeContinuumBound H := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound

theorem OAI.CircleDomainRigidity.level_topology_of_finite_physical_length line 100

Source documentation

Countability and local connectedness for the actual compact level union, without replacing the whole physical space by an unspecified finite-length ambient space.

theorem level_topology_of_finite_physical_length
    {X Y : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
    [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y]
    (π : Y → X) (hπ : Continuous π) (hsurj : Surjective π)
    (hfiber : ∀ x, IsConnected (π ⁻¹' {x}))
    {G : Set Y} (hG : IsOpen G) {B H : Set X}
    (hB : IsCompact B) (hTD : IsTotallyDisconnected B) (hdust : π '' Gᶜ ⊆ B)
    (hH : IsCompact H)
    (hlength : (μH[1] : Measure Y) ((π ⁻¹' H) ∩ G) < ∞) :
    HasFiniteLargeContinuumBound H ∧
      {C : Set H | (∃ x, C = connectedComponent x) ∧ C.Nontrivial}.Countable ∧
      ∀ C : Set H, IsCompact C → IsConnected C → LocallyConnectedSpace C := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound