OAI/Probability/GammaPassage/SourceConnector.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.trialSpacing line 9
2. def OAI.GammaFPP.CrossingBridge.trialWindow line 10
3. def OAI.GammaFPP.CrossingBridge.contactSign line 12
4. theorem OAI.GammaFPP.CrossingBridge.abs_contactSign line 14
5. theorem OAI.GammaFPP.CrossingBridge.contactSide_of_sign line 17
6. theorem OAI.GammaFPP.CrossingBridge.trialWindow_scale_bounds line 21
7. def OAI.GammaFPP.CrossingBridge.sourceSupportCost line 34
8. theorem OAI.GammaFPP.CrossingBridge.gamma_source_connector_test line 42

   Source documentation

   The two source tests correspond to a=1 and a=2. D0 is fixed after M; the probability estimate is uniform over every column X and transverse phase Y. No geometric premise or connector-probability premise remains.

   theorem gamma_source_connector_test {Ω : Type*} [MeasurableSpace Ω]
       {P : Measure Ω} {τ : Edge → Ω → ℝ} {shape rate : ℝ} (h : GammaEnvironment shape rate P τ)
       (hshape : 0 < shape) (hrate : 0 < rate)
       (b : ℝ) (hb : |b| ≤ 1) (plus : Bool) (M : ℕ) (hM : 0 < M)
       (R ε : ℝ) (hR : 0 ≤ R) (hε : 0 < ε) :
       ∃ D0 : ℝ, 1 ≤ D0 ∧ ∀ κ > 0, ∀ᶠ s : ℝ in atTop,
         ∀ X : ℤ, ∀ Y a : ℝ, 1 ≤ a → a ≤ 2 →
         P.real {ω | (fun e => τ e ω) ∉ allPairsRegionEvent
           (connectorVertices b X ⌈D0*s⌉ Y (trialWindow M R s) s)
           (connectorWindow b X Y (trialWindow M R s))
           (connectorWindow b (X+⌈D0*s⌉)
             (Y+contactSign plus*a*trialWindow M R s) (trialWindow M R s))
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.allPairsRegionEvent, OAI.GammaFPP.CrossingBridge.connectorVertices, OAI.GammaFPP.CrossingBridge.trialWindow, OAI.GammaFPP.CrossingBridge.connectorWindow, OAI.GammaFPP.CrossingBridge.contactSign