HausdorffPayment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Length payment by crossing a ball

The generic-level-continua proof in Section 1 of 047-02 uses radial distance on a subcontinuum crossing a ball contained in the physical domain. Its image contains the radius interval, so one-dimensional Hausdorff measure pays at least the ball radius.

theorem OAI.CircleDomainRigidity.dist_le_hausdorffMeasure_one_of_preconnected line 23

Source documentation

Radial distance is one-Lipschitz and maps a connected set containing two points onto an interval of length their distance.

theorem dist_le_hausdorffMeasure_one_of_preconnected
    {X : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
    {C : Set X} (hC : IsPreconnected C) {p q : X} (hp : p ∈ C) (hq : q ∈ C) :
    ENNReal.ofReal (dist q p) ≤ (μH[1] : Measure X) C := by
…

theorem OAI.CircleDomainRigidity.radius_le_hausdorffMeasure_inter_of_exits_closedBall line 43

Source documentation

A compact continuum through the center and exiting a closed ball pays at least the radius in physical Hausdorff length, provided the ball lies in the physical domain. No local connectedness is assumed.

theorem radius_le_hausdorffMeasure_inter_of_exits_closedBall
    {X : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
    {C G : Set X} (hcompact : IsCompact C) (hconn : IsConnected C)
    {p : X} (hp : p ∈ C) {r : ℝ} (hr : 0 < r)
    (hball : closedBall p r ⊆ G) (hexit : ∃ q ∈ C, r < dist q p) :
    ENNReal.ofReal r ≤ (μH[1] : Measure X) (C ∩ G) := by
…

theorem OAI.CircleDomainRigidity.finite_large_continuum_bound_of_quotient_length line 86

Source documentation

The physical length on G, pushed through a monotone quotient, gives the finite bound on large quotient continua. The remaining geometric hypothesis supplies a uniformly sized physical ball crossed by each sufficiently large quotient continuum.

theorem finite_large_continuum_bound_of_quotient_length
    {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}
    (hlength : (μH[1] : Measure Y) G < ∞)
    (hcross : ∀ ε : ℝ, 0 < ε → ∃ r : ℝ, 0 < r ∧
      ∀ C : Set X, IsCompact C → IsConnected C → ε ≤ diam C →
        ∃ p ∈ π ⁻¹' C, closedBall p r ⊆ G ∧ ∃ q ∈ π ⁻¹' C, r < dist q p) :
    HasFiniteLargeContinuumBound X := by
…

Mentions: OAI.CircleDomainRigidity.HasFiniteLargeContinuumBound