BKPrimitives.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.GammaFPP.BK.pathEdges line 11
Source documentation
The same physical support used by the crossing and spatial events.
```
abbrev pathEdges := GammaFPP.CrossingBridge.pathEdges
```
Mentions: OAI.GammaFPP.CrossingBridge.pathEdges
theorem OAI.GammaFPP.BK.pathEdges_eq_crossing line 13
theorem OAI.GammaFPP.BK.pathCost_eq_of_agree line 16
structure OAI.GammaFPP.BK.StrictPathWitness line 27
Source documentation
A labelled strict finite path. Different bounds on the same path are retained as different witnesses.
```
structure StrictPathWitness where
…
```
def OAI.GammaFPP.BK.StrictPathWitness.edges line 34
def OAI.GammaFPP.BK.StrictPathWitness.bits line 36
def OAI.GammaFPP.BK.dyadicSurvival line 42
Source documentation
The bits in x are the zero bits of the manuscript's uniform expansion. This is exactly 1-U^(t); zero is the cell whose rounded cost is infinity.
```
noncomputable def dyadicSurvival (t : ℕ) (x : Finset (Edge × Fin t)) (e : Edge) : ℝ :=
…
```
lemma OAI.GammaFPP.BK.dyadicSurvival_nonneg line 45
lemma OAI.GammaFPP.BK.dyadicSurvival_mono line 51
lemma OAI.GammaFPP.BK.dyadicSurvival_eq line 60
lemma OAI.GammaFPP.BK.pathCost_le_of_edges line 67
lemma OAI.GammaFPP.BK.StrictPathWitness.disjoint_bits line 75
def OAI.GammaFPP.BK.StrictPathWitness.Good line 81
def OAI.GammaFPP.BK.StrictDisjointPaths line 85
Source documentation
Original strict witnesses with pairwise disjoint physical edge supports.
```
def StrictDisjointPaths (S : Finset Edge) (Fs : List (Set StrictPathWitness)) (w : Edge → ℝ) : Prop :=
…
```
Mentions: OAI.GammaFPP.BK.StrictPathWitness
lemma OAI.GammaFPP.BK.dyadicRank_sum line 90
lemma OAI.GammaFPP.BK.dyadicSurvival_eq_rank line 103
Source documentation
Exact binary representation of the source rounded survival probability.
```
lemma dyadicSurvival_eq_rank (t : ℕ) (x : Finset (Edge × Fin t)) (e : Edge) :
    dyadicSurvival t x e = (dyadicRank t x e : ℝ)/(2:ℝ)^t := by
…
```
Mentions: OAI.GammaFPP.BK.dyadicSurvival, OAI.GammaFPP.dyadicRank
def OAI.GammaFPP.BK.StrictPathEvent line 120
Source documentation
Existence of a strict path witness with support in a prescribed finite edge set.
```
def StrictPathEvent (S : Finset Edge) (F : Set StrictPathWitness) (w : Edge → ℝ) : Prop :=
…
```
Mentions: OAI.GammaFPP.BK.StrictPathWitness
theorem OAI.GammaFPP.BK.StrictPathWitness.edges_eq_crossing line 123