WitnessSelection.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.CrossingBridge.takeWitnessPacks line 10

Source documentation

Preserve every chunk position while truncating the concatenated witness list.

def takeWitnessPacks {α : Type*} : ℕ → List (List α) → List (List α)
  | _,[] => []
  | t,ws::packs => ws.take t :: takeWitnessPacks (t-ws.length) packs

lemma OAI.GammaFPP.CrossingBridge.takeWitnessPacks_length line 14
lemma OAI.GammaFPP.CrossingBridge.takeWitnessPacks_flatten line 20
lemma OAI.GammaFPP.CrossingBridge.takeWitnessPacks_assign line 26

lemma OAI.GammaFPP.CrossingBridge.long_path_witness_count line 36

Source documentation

The exact source selection threshold, with a convenient sufficient N≥4.

lemma long_path_witness_count (H a : ℝ) (ha : 0 < a) (N M : ℕ) (hN : 4 ≤ N)
    (hlower : ((N : ℝ)-1)*a-4*a*M ≤ H) (hcheap : H < N*a/2) :
    N/16 ≤ M := by
…

def OAI.GammaFPP.CrossingBridge.witnessLabels line 47
Source documentation
A list of event labels determined only by the ordered chunk indices and by the number of selected witnesses in each position.
```
def witnessLabels : List ℕ → List (ℤ×ℤ) → List (ℤ×ℤ)
  | [],_ => []
  | _,[] => []
  | n::ns,i::is => List.replicate n i ++ witnessLabels ns is
```
lemma OAI.GammaFPP.CrossingBridge.witnessLabels_length line 52
theorem OAI.GammaFPP.CrossingBridge.witnessPacks_strictDisjoint line 61