PeriodizedLevels.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Periodizing scalar coarea lengths

A scalar coarea estimate controls the integral of the physical length of real level sets. Integer translates of [0,1) partition the real line, so the sum of these lengths over all lifts of a mod-one level has the same integral on [0,1). Countable subadditivity then gives finite physical length for almost every mod-one level.

theorem OAI.CircleDomainRigidity.unitAddCircle_eq_iff_exists_int line 29
Source documentation
Equality modulo one is equality up to an integer translation.
```
theorem unitAddCircle_eq_iff_exists_int {a b : ℝ} :
    (a : UnitAddCircle) = (b : UnitAddCircle) ↔ ∃ k : ℤ, a = b + (k : ℝ) := by
…
```
theorem OAI.CircleDomainRigidity.unitAddCircle_level_eq_iUnion_integer_levels line 37
Source documentation
The actual mod-one fiber of any real coordinate is the countable union of its integer-translated scalar fibers.
```
theorem unitAddCircle_level_eq_iUnion_integer_levels {Z : Type*} (f : Z → ℝ) (t : ℝ) :
    {x | (f x : UnitAddCircle) = (t : UnitAddCircle)} =
      ⋃ k : ℤ, {x | f x = t + (k : ℝ)} := by
…
```
theorem OAI.CircleDomainRigidity.unitAddCircle_level_inter_eq_iUnion_integer_levels line 43
def OAI.CircleDomainRigidity.periodizedLevelLength line 49
theorem OAI.CircleDomainRigidity.iUnion_integer_Ico line 52
theorem OAI.CircleDomainRigidity.pairwise_disjoint_integer_Ico line 57
theorem OAI.CircleDomainRigidity.measurable_periodizedLevelLength line 70
theorem OAI.CircleDomainRigidity.lintegral_periodizedLevelLength line 76
Source documentation
Tonelli and the integer translates of a unit interval give the exact periodized coarea integral.
```
theorem lintegral_periodizedLevelLength (L : ℝ → ℝ≥0∞) (hL : Measurable L) :
    ∫⁻ t in Ico (0 : ℝ) 1, periodizedLevelLength L t = ∫⁻ t, L t := by
…
```
Mentions: OAI.CircleDomainRigidity.periodizedLevelLength
theorem OAI.CircleDomainRigidity.ae_finite_periodizedLevelLength line 93

theorem OAI.CircleDomainRigidity.ae_finite_hausdorffMeasure_mod_one_levels line 103

Source documentation

A mod-one physical level is a union of its scalar lifts. Its Hausdorff length is bounded by the periodized scalar coarea bound and is therefore finite almost everywhere on the fundamental interval.

theorem ae_finite_hausdorffMeasure_mod_one_levels
    {Z : Type*} [MetricSpace Z] [MeasurableSpace Z] [BorelSpace Z]
    (L : ℝ → ℝ≥0∞) (hL : Measurable L) (hfinite : ∫⁻ t, L t < ∞)
    (A H : ℝ → Set Z)
    (hcover : ∀ t, H t ⊆ ⋃ k : ℤ, A (t + (k : ℝ)))
    (hlength : ∀ r, (μH[1] : Measure Z) (A r) ≤ L r) :
    ∀ᵐ t ∂volume.restrict (Ico (0 : ℝ) 1), (μH[1] : Measure Z) (H t) < ∞ := by
…

theorem OAI.CircleDomainRigidity.ae_finite_hausdorffMeasure_scalar_mod_one_levels line 121

Source documentation

Applying the periodization argument to actual scalar and circle fibers removes the countable-union premise. The real-level estimate is exactly the specialization supplied by scalar coarea.

theorem ae_finite_hausdorffMeasure_scalar_mod_one_levels
    {Z : Type*} [MetricSpace Z] [MeasurableSpace Z] [BorelSpace Z]
    (f : Z → ℝ) (D : Set Z) (L : ℝ → ℝ≥0∞) (hL : Measurable L)
    (hfinite : ∫⁻ t, L t < ∞)
    (hlength : ∀ r, (μH[1] : Measure Z) (D ∩ {x | f x = r}) ≤ L r) :
    ∀ᵐ (t : ℝ) ∂volume.restrict (Ico (0 : ℝ) 1),
      (μH[1] : Measure Z) (D ∩ {x | (f x : UnitAddCircle) = (t : UnitAddCircle)}) < ∞ := by
…