SourceLabeledGoodEvents.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Measurable reference events for the original error, positive main square and full masked variation. All three thresholds are fixed before the angular path or mass cutoff is selected.

def OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceEvent line 24
def OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceBad line 29
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceEvent_measurable line 32
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceBad_measurable line 41
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceBad_compl_bounds line 45
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceEvent_line_zero line 62
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceEvent_line_one line 68
theorem OAI.LipschitzHilbert.SourceLabeledLattice.physicalReferenceEvent_line_two line 76

theorem OAI.LipschitzHilbert.SourceLabeledLattice.eventually_physicalReferenceBad_tail line 86

Source documentation

The three actual reference tails lose one unit of exponential rate. There is no dependence on the number of packets or angular depth.

theorem eventually_physicalReferenceBad_tail (rate : ℝ) :
    ∀ᶠ 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)
      (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 a : ℝ) (b : ∀ j, P.labels j → κ → ℝ → ℂ)
      (v : ℝ×ℝ → ℝ) (g : ℝ×ℝ → EuclideanSpace ℂ κ)
      (T : ∀ j (l : P.labels j), Item j l → SlopeBox)
      (A e s r y u W : ℝ), 0 < W →
      (volume.restrict (Ico u (u+W)))
…

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