OAI/Probability/GammaPassage/WitnessEntropy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.CrossingBridge.spatialNeighbors line 11
2. lemma OAI.GammaFPP.CrossingBridge.spatialNeighbors_card line 14
3. lemma OAI.GammaFPP.CrossingBridge.mem_spatialNeighbors line 18
4. def OAI.GammaFPP.CrossingBridge.spatialItineraries line 24
5. lemma OAI.GammaFPP.CrossingBridge.spatialItineraries_card line 28
6. lemma OAI.GammaFPP.CrossingBridge.mem_spatialItineraries line 39
7. def OAI.GammaFPP.CrossingBridge.increaseFirst line 51
8. def OAI.GammaFPP.CrossingBridge.compositionCandidates line 56

   Source documentation

   Pascal recursion gives a finite cover of all weak compositions.

   noncomputable def compositionCandidates : ℕ → ℕ → Finset (List ℕ)
     | 0,t => {[t]}
     | n+1,0 => {List.replicate (n+2) 0}
     | n+1,t+1 => (compositionCandidates n (t+1)).image (List.cons 0) ∪
         (compositionCandidates (n+1) t).image increaseFirst
   termination_by n t => n+t

   Mentions: OAI.GammaFPP.CrossingBridge.increaseFirst

9. lemma OAI.GammaFPP.CrossingBridge.compositionCandidates_card line 63
10. lemma OAI.GammaFPP.CrossingBridge.mem_compositionCandidates line 77
11. def OAI.GammaFPP.CrossingBridge.compositionCover line 119
12. lemma OAI.GammaFPP.CrossingBridge.mem_compositionCover line 122
13. lemma OAI.GammaFPP.CrossingBridge.compositionCover_card line 128

    Source documentation

    The source 4^N bound, without counting any witnessing paths.

    lemma compositionCover_card (n t : ℕ) (ht : t ≤ n) : (compositionCover n t).card ≤ 4^n := by
    …

    Mentions: OAI.GammaFPP.CrossingBridge.compositionCover