SphereLevels.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Applying finite-length level topology to the actual sphere quotient

Choose a compatible metric on OnePoint ℂ by its standard homeomorphism with the unit sphere in three-dimensional Euclidean space. This keeps the original topology definitionally unchanged. The quotient obtained from Moore's published decomposition input then satisfies the already proved finite-physical-length level theorem. No metric or level regularity of the quotient is left as an additional premise.

def OAI.CircleDomainRigidity.roundSphereEquiv line 22
abbrev OAI.CircleDomainRigidity.sphereMetric line 28
Source documentation
A fixed compatible sphere metric, pulled back from the Euclidean unit sphere. Its topology is the original one-point topology.
```
noncomputable abbrev sphereMetric : MetricSpace Sphere :=
…
```
Mentions: OAI.CircleDomainRigidity.Sphere
abbrev OAI.CircleDomainRigidity.sphereBorel line 33
theorem OAI.CircleDomainRigidity.roundSphereEquiv_isometry line 39

theorem OAI.CircleDomainRigidity.quotientSphere_with_finite_length_levels line 44

Source documentation

Moore's quotient on the concrete sphere, together with its complete finite-length level consequence. The displayed Hausdorff measure is for sphereMetric; all topology is the original sphere topology.

theorem quotientSphere_with_finite_length_levels (hMoore : MooreSphereDecomposition)
    {G : Set Sphere} (hG : IsOpen G) (hconn : IsConnected G) :
    ∃ π : Sphere → Sphere,
      Continuous π ∧ Function.Surjective π ∧
      (∀ x y, π x = π y ↔
        x = y ∨ (x ∈ Gᶜ ∧ y ∈ connectedComponentIn Gᶜ x)) ∧
      (∀ H : Set Sphere, IsCompact H →
        (μH[1] : Measure Sphere) ((π ⁻¹' 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.MooreSphereDecomposition, OAI.CircleDomainRigidity.Sphere, OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound