OAI/Analysis/CircleDomains/Rigidity/TraceLineTails.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Tonelli's theorem selects lines with finite total interval cost. The union of the remaining active intervals consequently has vanishing outer length. Overlaps between the intervals require no disjointness.

  1. theorem OAI.CircleDomainRigidity.ae_finite_line_incidence line 17
  2. def OAI.CircleDomainRigidity.lineTailIntervals line 27
  3. theorem OAI.CircleDomainRigidity.lineTailIntervals_measurable line 30
  4. theorem OAI.CircleDomainRigidity.lineTailIntervals_volume_tendsto line 39
  5. theorem OAI.CircleDomainRigidity.ae_lineTailIntervals_volume_tendsto line 52
  6. theorem OAI.CircleDomainRigidity.ae_balloon_line_tails line 61

    Source documentation

    Square-summable interval lengths and balloon radii pay for almost all transverse lines. The center positions are unrestricted.

     theorem ae_balloon_line_tails {I : ℕ → Set ℝ} {d : ℕ → ℝ}
    (hd : ∀ j, 0 ≤ d j) (c : ℕ → ℝ)
    (hI : ∀ j, volume (I j) ≠ ∞)
    (hIsq : Summable (fun j => volume.real (I j)^2))
    (hdsq : Summable (fun j => d j^2)) :
    ∀ᵐ t ∂volume, Tendsto (fun N => volume
      (lineTailIntervals I (fun j => Ioo (c j-d j) (c j+d j)) t N)) atTop (𝓝 0) := by
…

    Mentions: OAI.CircleDomainRigidity.lineTailIntervals