SourceLabeledUniformErrorTail.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The original physical error tail, uniform before choosing the packet family and the reference line. Fixed selector multiplicity and Lipschitz bounds absorb the source-amplitude factor in one polynomial power.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_uniform_physicalAngularError_tail line 17

Source documentation

Uniform physical error tail with its source-amplitude budget discharged. The geometric hypotheses are exactly those of the labeled error family.

theorem eventually_uniform_physicalAngularError_tail
    (q rate M Lip : ℝ) (hq : 0 ≤ q) (hrate : 0 ≤ rate)
    (hM : 0 ≤ M) (hLip : 0 ≤ Lip) (K H J₀ : ℕ) :
    ∀ᶠ L : ℝ in atTop,
    ∀ (N : ℕ) (κ : Type) (Label : Fin N → Type) (Item : ∀ j, Label j → Type)
      [Fintype κ] [∀ j l, Fintype (Item j l)]
      (P : SourceLabeledLattice N κ Label Item) (_horder : 6 ≤ P.order),
      P.absoluteConstant ≤ L^q →
    ∀ (t a c Cwide radius : ℝ) (E J : ℕ)
      (_ha : 0 < a) (_hc : 0 < c) (_hc1 : c ≤ 1)
      (_hC : Cwide ≤ c*(2:ℝ)^J) (_hwide : 1 ≤ Cwide*((2:ℝ)^E)^4)
      (_hradius : radius ≤ K)
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice