OAI/Analysis/LipschitzHilbert/Trees/SourceLabeledErrorPhysicalTail.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_physicalAngularError_tail line 31

   Source documentation

   The original physical positive error sum has the uniform interval tail supplied by its actual labeled dyadic family.

   theorem eventually_physicalAngularError_tail (p rate : ℝ) (hp : 0 ≤ p)
       (hrate : 0 ≤ rate) (J₀ : ℕ) :
       ∀ᶠ L : ℝ in Filter.atTop,
         (P.angularErrorFamily horder t a c Cwide M Lip radius E J K H ha hc hc1 hC hwide
           hM hLip hradius hlocal b hb hbM hsupport hnear hfar v hv g hg hg1).sourceAmplitude ≤ L^p →
         J ≤ J₀ → E = SourceParameters.stepExponent L*SourceParameters.blockCount L →
         ∀ (y u W : ℝ), 0 < W → (∀ j (l : P.labels j) (_i : Item j l), P.length j ≤ W) →
         (volume.restrict (Set.Ico u (u+W)))
           {x | L^(p+7) ≤ P.physicalAngularError t a b v g (x,y+t*x)} ≤
             ENNReal.ofReal (Real.exp (-rate*L))*ENNReal.ofReal W := by
   …

   Mentions: OAI.LipschitzHilbert.SourceParameters.stepExponent, OAI.LipschitzHilbert.SourceParameters.blockCount