OAI/Probability/GammaPassage/GoodSiteTrials.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.trialOffset line 10
2. def OAI.GammaFPP.CrossingBridge.trialTranslate line 13
3. theorem OAI.GammaFPP.CrossingBridge.nearest_integer_error line 17
4. theorem OAI.GammaFPP.CrossingBridge.trialTranslate_error line 23
5. theorem OAI.GammaFPP.CrossingBridge.trialSpacing_bounds line 32
6. theorem OAI.GammaFPP.CrossingBridge.trialOffset_bound line 41
7. theorem OAI.GammaFPP.CrossingBridge.trial_strip_in_window line 56

   Source documentation

   Every translated strip of half-width R*s lies inside its S₀/4 window, including the half-unit lattice-phase error.

   theorem trial_strip_in_window (b : ℝ) (X : ℤ) (Y : ℝ)
       (M : ℕ) (R s : ℝ) (j : Fin M) (hR : 0 ≤ R) (hs : 1 ≤ s)
       (p : Vertex) (hp : |transverse b p-transverse b (trialTranslate b X Y M R s j)| ≤ R*s) :
       |transverse b p-Y| ≤ trialWindow M R s/4 := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.trialTranslate, OAI.GammaFPP.CrossingBridge.trialWindow

8. theorem OAI.GammaFPP.CrossingBridge.trial_centers_separated line 78

   Source documentation

   Distinct trials have strictly disjoint transverse strips, uniformly in both the longitudinal column and the real transverse phase.

   theorem trial_centers_separated (b : ℝ) (X : ℤ) (Y : ℝ)
       (M : ℕ) (R s : ℝ) (j l : Fin M) (hjl : j ≠ l) (hR : 0 ≤ R) (hs : 1 ≤ s) :
       2*R*s < |transverse b (trialTranslate b X Y M R s j)-
         transverse b (trialTranslate b X Y M R s l)| := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.trialTranslate

9. theorem OAI.GammaFPP.CrossingBridge.rareFastTrials_disjoint line 103
10. theorem OAI.GammaFPP.CrossingBridge.rareFastTrials_failure_bound line 128

    Source documentation

    Disjoint translated trials amplify the original crossing success probability.

    theorem rareFastTrials_failure_bound (h : GammaEnvironment shape rate P τ)
        (b m a A R ε s p0 : ℝ) (n X : ℤ) (Y : ℝ) (M : ℕ)
        (hR : 0 ≤ R) (hs : 1 ≤ s)
        (hp0 : p0 ≤ P.real {ω | (fun e => τ e ω) ∈ rareFastEvent b m a A R ε s n 0}) :
        P.real {ω | ∀ j : Fin M, (fun e => τ e ω) ∉ rareFastEvent b m a A R ε s n
          (trialTranslate b X Y M R s j)} ≤ (1-p0)^M := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.rareFastEvent, OAI.GammaFPP.CrossingBridge.trialTranslate