OAI/Analysis/LipschitzHilbert/Trees/SourcePhysicalGoodPath.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LipschitzHilbert.PhysicalReferenceData line 15
2. def OAI.LipschitzHilbert.PhysicalReferenceData.bad line 33
3. theorem OAI.LipschitzHilbert.PhysicalReferenceData.bad_measurable line 37
4. theorem OAI.LipschitzHilbert.PhysicalReferenceData.good_bounds line 41
5. theorem OAI.LipschitzHilbert.eventually_physical_reference_good_path_area line 54

   Source documentation

   All shifts of each actual physical reference family enter one weighted good set. Its removed area depends on total top area, while a good path satisfies the three original quantitative reference bounds.

   theorem eventually_physical_reference_good_path_area (K D a : ℝ)
       (hK : 1 ≤ K) (hD : 2 < D) :
       ∀ᶠ L : ℝ in atTop, ∀ (ι σ : Type*) (tops : Finset ι) (T : ι → SlopeBox)
         (events : ι → Finset σ) (N : ℕ) (κ : Type) (Label : Fin N → Type)
         (Item : ∀ j, Label j → Type) [Fintype κ] [∀ j l, Fintype (Item j l)]
         (P : ι → σ → PhysicalReferenceData N κ Label Item)
         (A e s r : ℝ) (base : Set (ℝ×ℝ)),
         MeasurableSet base → (∀ 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) ∈ (P t i).bad L A e s r} ≤
           ENNReal.ofReal (Real.exp (-12*L))*
   …

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