BandCoarea.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted coarea with the actual boundary-band incidences

The abstract dust events in the weighted-level estimate are here the actual circle-band fibers. Their measurability and measure bounds are proved from the compact band graph and its liminf–limsup budget. The final theorem applies this to the finite-plane part of a bounded real coordinate on the concrete Riemann sphere.

def OAI.CircleDomainRigidity.unitIntervalBandIncidence line 23
theorem OAI.CircleDomainRigidity.measurableSet_unitIntervalBandIncidence line 27
theorem OAI.CircleDomainRigidity.measure_unitIntervalBandIncidence_le line 34

theorem OAI.CircleDomainRigidity.weighted_level_bound_of_real_sphere_coordinate line 59

Source documentation

The weighted physical-plus-dust level bound for a bounded real coordinate on the sphere. Only the scalar coarea formula is a published input; the actual dust-incidence bound is derived from its band budget. The physical term here uses the finite-plane chart and Euclidean H¹.

theorem weighted_level_bound_of_real_sphere_coordinate
    {S : Type*} [Countable S]
    (hcoarea : WeightedPlanarScalarCoarea)
    {G : Set Sphere} (hG : IsOpen G) (f : Sphere → ℝ) {M : ℝ}
    (hM : ∀ y ∈ G, |f y| ≤ M)
    (hf : ContDiffOn ℝ 1 (fun z : ℂ => f (z : Sphere))
      (((↑) : ℂ → Sphere) ⁻¹' G))
    (p : S → Sphere) (hp : ∀ s, p s ∈ closure G)
    (m a : S → ℝ) (hm : ∀ s, 0 ≤ m s) (ha : ∀ s, 0 ≤ a s)
    (hbudget : ∀ s, Filter.limsup f (𝓝[G] (p s)) -
      Filter.liminf f (𝓝[G] (p s)) ≤ a s)
    (hm2 : Summable (fun s => m s ^ 2)) (ha2 : Summable (fun s => a s ^ 2))
…

Mentions: OAI.CircleDomainRigidity.WeightedPlanarScalarCoarea, OAI.CircleDomainRigidity.Sphere