SourceGoodPathArea.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual local reference tails, including every shift, give the full weighted good-path set with its prescribed area loss.

theorem OAI.LipschitzHilbert.eventually_source_good_path_area line 16

Source documentation

All spatial intervals are retained. The hypotheses concern individual reference events, while the conclusion is the original weighted good set.

theorem eventually_source_good_path_area (K D a : ℝ) (hK : 1 ≤ K) (hD : 2 < D) :
    ∀ᶠ L : ℝ in atTop, ∀ (ι σ : Type*) (tops : Finset ι) (T : ι → SlopeBox)
      (events : ι → Finset σ) (event : ι → σ → Set (ℝ×ℝ)) (bad : ι → Set (ℝ×ℝ))
      (base : Set (ℝ×ℝ)), MeasurableSet base →
      (∀ t ∈ tops, MeasurableSet (bad t)) →
      (∀ t ∈ tops, bad t ⊆ ⋃ i ∈ events t, event t i) →
      (∀ t ∈ tops, ((events t).card:ℝ) ≤ L^a) →
      (∀ t ∈ tops, ∀ᵐ y : ℝ ∂volume, ∀ k : ℤ, ∀ i ∈ events t,
        (volume.restrict (sourceLineTile (T t).length k))
          {x | (x,y+(T t).slope*x) ∈ event t i} ≤
        ENNReal.ofReal (Real.exp (-12*L))*
          (volume.restrict (sourceLineTile (T t).length k)) univ) →
…

Mentions: OAI.LipschitzHilbert.SlopeBox, OAI.LipschitzHilbert.sourceLineTile