CoareaLevels.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

From planar coarea charts to compact quotient-level topology

A finite collection of Lipschitz parameterizations covers the physical part of each level. Scalar coarea in each parameter domain gives finite Hausdorff length almost everywhere. The quotient-level argument then gives the finite-continuum bound, countably many nondegenerate components, and local connectedness of every subcontinuum.

The chart-cover inclusion and the compactness of the level are geometric hypotheses; PlanarScalarCoarea supplies the analytic identity.

def OAI.CircleDomainRigidity.finiteLevelUnion line 28
Source documentation
A finite list may repeat labels: its entries still have independent level parameters.
```
def finiteLevelUnion {X J Λ : Type*} (H : Λ → ℝ → Set X) (labels : J → Λ)
    (θ : J → ℝ) : Set X :=
…
```

theorem OAI.CircleDomainRigidity.ae_finite_hausdorffMeasure_level_union line 34

Source documentation

Almost-everywhere finite length for each label passes to an actual finite union under the independent product of the level measures.

theorem ae_finite_hausdorffMeasure_level_union
    {Y J Λ : Type*} [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [Fintype J]
    (μ : Measure ℝ) [SigmaFinite μ] (A : Λ → ℝ → Set Y) (labels : J → Λ)
    (hfinite : ∀ l, ∀ᵐ t ∂μ, (μH[1] : Measure Y) (A l t) < ∞) :
    ∀ᵐ θ ∂Measure.pi (fun _ : J => μ),
      (μH[1] : Measure Y) (finiteLevelUnion A labels θ) < ∞ := by
…

Mentions: OAI.CircleDomainRigidity.finiteLevelUnion

theorem OAI.CircleDomainRigidity.ae_finite_physical_levels_of_planar_coarea line 50

Source documentation

Finite Lipschitz chart covers preserve the almost-everywhere finite length conclusion of planar coarea.

theorem ae_finite_physical_levels_of_planar_coarea
    {Y ι : Type*} [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [Fintype ι]
    (hcoarea : PlanarScalarCoarea)
    (D : ι → Set ℂ) (f : ι → ℂ → ℝ) (χ : ι → ℂ → Y) (K : ι → ℝ≥0)
    (hD : ∀ i, IsOpen (D i)) (hf : ∀ i, ContDiffOn ℝ 1 (f i) (D i))
    (hχ : ∀ i, LipschitzWith (K i) (χ i))
    (harea : ∀ i, volume (D i) < ∞)
    (henergy : ∀ i, (∫⁻ z in D i, ENNReal.ofReal (‖fderiv ℝ (f i) z‖ ^ 2)) < ∞)
    (A : ℝ → Set Y)
    (hcover : ∀ t, A t ⊆ ⋃ i, χ i ''
      (D i ∩ {z | (f i z : UnitAddCircle) = (t : UnitAddCircle)})) :
    ∀ᵐ (t : ℝ) ∂volume.restrict (Ico (0 : ℝ) 1), (μH[1] : Measure Y) (A t) < ∞ := by
…

Mentions: OAI.CircleDomainRigidity.PlanarScalarCoarea

theorem OAI.CircleDomainRigidity.ae_level_topology_of_planar_coarea line 75

Source documentation

The actual compact quotient-level conclusions obtained from Federer's scalar coarea input and a finite planar chart cover.

theorem ae_level_topology_of_planar_coarea
    {X Y ι : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
    [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y] [Fintype ι]
    (hcoarea : PlanarScalarCoarea)
    (π : Y → X) (hπ : Continuous π) (hsurj : Surjective π)
    (hfiber : ∀ x, IsConnected (π ⁻¹' {x}))
    {G : Set Y} (hG : IsOpen G) {B : Set X}
    (hB : IsCompact B) (hTD : IsTotallyDisconnected B) (hdust : π '' Gᶜ ⊆ B)
    (D : ι → Set ℂ) (f : ι → ℂ → ℝ) (χ : ι → ℂ → Y) (K : ι → ℝ≥0)
    (hD : ∀ i, IsOpen (D i)) (hf : ∀ i, ContDiffOn ℝ 1 (f i) (D i))
    (hχ : ∀ i, LipschitzWith (K i) (χ i))
    (harea : ∀ i, volume (D i) < ∞)
…

Mentions: OAI.CircleDomainRigidity.PlanarScalarCoarea

theorem OAI.CircleDomainRigidity.ae_finite_level_union_topology_of_planar_coarea line 107

Source documentation

Generic finite level unions, including repeated labels, satisfy the physical-length and continuum-topology conclusions. The probability law is the independent product of Lebesgue measure on [0,1).

This is the coarea-to-topology part of the manuscript's Generic level continua lemma, items (i)--(iii). Arcwise connectedness is not asserted by this theorem. All chart geometry remains explicit.

theorem ae_finite_level_union_topology_of_planar_coarea
    {X Y J Λ ι : Type*} [MetricSpace X] [MeasurableSpace X] [BorelSpace X]
    [MetricSpace Y] [MeasurableSpace Y] [BorelSpace Y] [CompactSpace Y]
    [Fintype J] [Fintype ι]
    (hcoarea : PlanarScalarCoarea)
    (π : Y → X) (hπ : Continuous π) (hsurj : Surjective π)
    (hfiber : ∀ x, IsConnected (π ⁻¹' {x}))
    {G : Set Y} (hG : IsOpen G) {B : Set X}
    (hB : IsCompact B) (hTD : IsTotallyDisconnected B) (hdust : π '' Gᶜ ⊆ B)
    (D : Λ → ι → Set ℂ) (f : Λ → ι → ℂ → ℝ)
    (χ : Λ → ι → ℂ → Y) (K : Λ → ι → ℝ≥0)
    (hD : ∀ l i, IsOpen (D l i))
…

Mentions: OAI.CircleDomainRigidity.PlanarScalarCoarea

theorem OAI.CircleDomainRigidity.weighted_level_bound_of_planar_coarea line 156

Source documentation

The weighted-level numerical estimate: coarea supplies the physical term, and Tonelli plus the band-incidence bound supplies the countable dust term. Their sum is finite under the two spatial L² assumptions and the two square-summable dust sequences.

The events E and their measure bound are geometric hypotheses, and weighted scalar coarea supplies the analytic identity.

theorem weighted_level_bound_of_planar_coarea
    {S : Type*} [Countable S]
    (hcoarea : WeightedPlanarScalarCoarea) {D : Set ℂ} (hD : IsOpen D)
    {f q : ℂ → ℝ} (hf : ContDiffOn ℝ 1 f D)
    (hq : Measurable q) (hq0 : ∀ z, 0 ≤ q z)
    (hq2 : (∫⁻ z in D, ENNReal.ofReal (q z ^ 2)) < ∞)
    (hf2 : (∫⁻ z in D, ENNReal.ofReal (‖fderiv ℝ f z‖ ^ 2)) < ∞)
    (E : S → Set ℝ) (m a : S → ℝ)
    (hE : ∀ s, MeasurableSet (E s)) (hm : ∀ s, 0 ≤ m s) (ha : ∀ s, 0 ≤ a s)
    (hband : ∀ s, (volume.restrict (Ico (0 : ℝ) 1)) (E s) ≤ ENNReal.ofReal (a s))
    (hm2 : Summable (fun s => m s ^ 2)) (ha2 : Summable (fun s => a s ^ 2)) :
    (∫⁻ t in Ico (0 : ℝ) 1,
…

Mentions: OAI.CircleDomainRigidity.WeightedPlanarScalarCoarea