OAI/Probability/GammaPassage/GoodSiteBlocks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.blockLayer line 10
2. def OAI.GammaFPP.CrossingBridge.blockLevel line 12
3. def OAI.GammaFPP.CrossingBridge.blockX line 14
4. def OAI.GammaFPP.CrossingBridge.blockY line 16
5. def OAI.GammaFPP.CrossingBridge.blockRegion line 18
6. theorem OAI.GammaFPP.CrossingBridge.centers_close_of_point line 22
7. theorem OAI.GammaFPP.CrossingBridge.blockRegion_common_indices line 32

   Source documentation

   Sharing one support vertex bounds both transformed lattice indices. Crucially these bounds contain neither M nor D0.

   theorem blockRegion_common_indices (b A : ℝ) (n d : ℤ) (σ S : ℝ)
       (hn : 0 < n) (hd : 0 ≤ d) (hσ : |σ|=1) (hS : 0 < S)
       (v w p : Vertex) (hv : p ∈ blockRegion b A n d σ S v)
       (hw : p ∈ blockRegion b A n d σ S w) :
       |((blockLayer v-blockLayer w : ℤ) : ℝ)| ≤ 2*(A+3) ∧
       |((blockLevel v-blockLevel w : ℤ) : ℝ)| ≤ 8 := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.blockRegion, OAI.GammaFPP.CrossingBridge.blockLayer, OAI.GammaFPP.CrossingBridge.blockLevel

8. theorem OAI.GammaFPP.CrossingBridge.blockRegion_common_near line 57
9. theorem OAI.GammaFPP.CrossingBridge.blockRegion_disjoint line 94

   Source documentation

   A radius uniform in the connector gap works at every positive scale.

   theorem blockRegion_disjoint (b A : ℝ) (n d : ℤ) (σ S : ℝ)
       (hn : 0 < n) (hd : 0 ≤ d) (hσ : |σ|=1) (hS : 0 < S) (hA : 0 < A)
       (v w : Vertex) (hvw : ¬latticeNear (⌈4*(A+3)+8⌉₊+1) v w) :
       Disjoint (blockRegion b A n d σ S v) (blockRegion b A n d σ S w) := by
   …

   Mentions: OAI.GammaFPP.CrossingBridge.blockRegion

10. theorem OAI.GammaFPP.CrossingBridge.blockRegion_finite line 106
11. def OAI.GammaFPP.CrossingBridge.blockVertices line 110
12. theorem OAI.GammaFPP.CrossingBridge.mem_blockVertices line 113
13. theorem OAI.GammaFPP.CrossingBridge.block_supported_tests_independent line 122

    Source documentation

    Tests supported on sufficiently separated finite block regions are jointly independent, as required by Lemma cr:oriented-paths.

    theorem block_supported_tests_independent (h : GammaEnvironment shape rate P τ)
        (b A : ℝ) (n d : ℤ) (σ S : ℝ)
        (hn : 0 < n) (hd : 0 ≤ d) (hσ : |σ|=1) (hS : 0 < S) (hA : 0 < A)
        (E : Vertex → Set (Edge → ℝ)) (hE : ∀ v, MeasurableSet (E v))
        (hsupport : ∀ v, DependsOnEdges (E v) (internalEdges (blockVertices b A n d σ S v))) :
        SeparatedGoodIndependent P (fun v => {ω | (fun e => τ e ω) ∈ E v})
          (⌈4*(A+3)+8⌉₊+1) := by
    …

    Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.CrossingBridge.DependsOnEdges, OAI.GammaFPP.CrossingBridge.internalEdges, OAI.GammaFPP.CrossingBridge.blockVertices