CoreCrossing.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform crossing from a compact physical core

This supplies the geometric input to the length-payment argument in the generic-level-continua lemma. A compact core inside the physical domain has a uniform ball neighborhood there. Uniform continuity of the quotient map makes these balls too small to contain a large quotient continuum.

theorem OAI.CircleDomainRigidity.continuum_meets_core_of_small_open_cover line 25

Source documentation

A connected continuum covered off a core by disjoint open sets of small diameter must meet that core. In the application the ambient compact metric space is the level union itself.

theorem continuum_meets_core_of_small_open_cover
    {X ι : Type*} [MetricSpace X] [CompactSpace X]
    {F C : Set X} (U : ι → Set X) (hopen : ∀ i, IsOpen (U i))
    (hdisj : Pairwise (Disjoint on U)) (hcover : Fᶜ ⊆ ⋃ i, U i)
    {ε : ℝ} (hsmall : ∀ i, diam (U i) < ε)
    (hconn : IsConnected C) (hdiam : ε ≤ diam C) : (C ∩ F).Nonempty := by
…

theorem OAI.CircleDomainRigidity.uniform_ball_crossing_of_compact_core line 61

Source documentation

A compact physical core meeting every sufficiently large quotient continuum supplies uniformly sized physical balls that those continua must exit.

theorem uniform_ball_crossing_of_compact_core
    {X Y : Type*} [MetricSpace X] [MetricSpace Y] [CompactSpace Y]
    (π : Y → X) (hπ : Continuous π) (hsurj : Function.Surjective π)
    {G K : Set Y} (hG : IsOpen G) (hK : IsCompact K) (hKG : K ⊆ G)
    {ε : ℝ} (hε : 0 < ε)
    (hcore : ∀ C : Set X, IsCompact C → IsConnected C → ε ≤ diam C →
      (C ∩ π '' K).Nonempty) :
    ∃ r : ℝ, 0 < r ∧ ∀ C : Set X,
      IsCompact C → IsConnected C → ε ≤ diam C →
      ∃ p ∈ π ⁻¹' C, closedBall p r ⊆ G ∧ ∃ q ∈ π ⁻¹' C, r < dist q p := by
…

theorem OAI.CircleDomainRigidity.finite_large_continuum_bound_of_compact_cores line 101

Source documentation

Finite physical level length and arbitrarily fine compact cores give the finite large-continuum bound in the quotient. The core-intersection hypothesis is explicit; the radius choice, ball crossing, Hausdorff payment, and cardinal estimate are all derived.

theorem finite_large_continuum_bound_of_compact_cores
    {X Y : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
    [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y]
    (π : Y → X) (hπ : Continuous π) (hsurj : Function.Surjective π)
    (hfiber : ∀ x, IsConnected (π ⁻¹' {x})) {G : Set Y} (hG : IsOpen G)
    (hlength : (μH[1] : Measure Y) G < ∞)
    (hcores : ∀ ε : ℝ, 0 < ε → ∃ K : Set Y,
      IsCompact K ∧ K ⊆ G ∧
      ∀ C : Set X, IsCompact C → IsConnected C → ε ≤ diam C →
        (C ∩ π '' K).Nonempty) : HasFiniteLargeContinuumBound X := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound

theorem OAI.CircleDomainRigidity.finite_large_continuum_bound_of_small_open_core_covers line 120

Source documentation

The form used for generic level unions: outside a compact physical core, the quotient is covered by disjoint relatively open dust disks of arbitrarily small diameter. Finite physical length then bounds the number of disjoint large subcontinua.

theorem finite_large_continuum_bound_of_small_open_core_covers
    {X Y ι : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [CompactSpace X]
    [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y]
    (π : Y → X) (hπ : Continuous π) (hsurj : Function.Surjective π)
    (hfiber : ∀ x, IsConnected (π ⁻¹' {x})) {G : Set Y} (hG : IsOpen G)
    (hlength : (μH[1] : Measure Y) G < ∞)
    (hcovers : ∀ ε : ℝ, 0 < ε → ∃ (K : Set Y) (U : ι → Set X),
      IsCompact K ∧ K ⊆ G ∧ (∀ i, IsOpen (U i)) ∧
      Pairwise (Disjoint on U) ∧ (π '' K)ᶜ ⊆ ⋃ i, U i ∧ ∀ i, diam (U i) < ε) :
    HasFiniteLargeContinuumBound X := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound