SourceLabeledGoodTail.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble the original error, narrow main square and narrow centered variation tails into the physical bad-reference event. Polynomial powers and exponential losses are fixed before the family is selected.

theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalAngularError_nonneg line 18

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_physical_reference_good_tail line 31

Source documentation

The actual three-reference event has a uniform tail, provided the three already proved component tails are supplied two rates stronger.

theorem eventually_physical_reference_good_tail (a q p 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), 6 ≤ P.order → P.absoluteConstant ≤ L^a →
    ∀ (alt : ∀ j (l : P.labels j), Item j l → κ → SchwartzMap (ℝ×ℝ) ℂ)
      (hAlt : ∀ j l u k, planarProfileConstant (alt j l u k) (2*P.order) ≤ P.profileBound)
      (t c : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ)
      (_hb : ∀ j l k, Measurable (b j l k)) (_hb1 : ∀ j l k s, ‖b j l k s‖ ≤ 1)
      (v : ℝ×ℝ → ℝ) (_hv : Measurable v)
      (g : ℝ×ℝ → EuclideanSpace ℂ κ) (_hg : Measurable g) (_hg1 : ∀ z, ‖g z‖ ≤ 1)
      (T : ∀ j (l : P.labels j), Item j l → SlopeBox) (A y u W : ℝ), 0 < W →
…

Mentions: OAI.LipschitzHilbert.SourceLabeledLattice, OAI.LipschitzHilbert.planarProfileConstant, OAI.LipschitzHilbert.SlopeBox