OAI/Probability/GammaPassage/BKContinuous.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.BK.bitFamily_subset line 11
2. lemma OAI.GammaFPP.BK.bitDisjointFamily_subset line 16
3. lemma OAI.GammaFPP.BK.single_mass_le line 22
4. lemma OAI.GammaFPP.BK.rounded_disjoint_mass_le line 46
5. lemma OAI.GammaFPP.BK.probabilities_nonneg line 75
6. lemma OAI.GammaFPP.BK.factors_le line 81
7. theorem OAI.GammaFPP.BK.gamma_rounded_strict_path_BK line 94
8. theorem OAI.GammaFPP.BK.gamma_strict_path_BK line 105

   Source documentation

   Finite-path repeated BK in the actual Gamma environment, for every positive real shape and rate. Fs may repeat and regions may overlap; only the chosen paths' undirected edge sets must be pairwise disjoint.

   theorem gamma_strict_path_BK (h : GammaEnvironment shape rate P τ)
       (hs : 0 < shape) (hr : 0 < rate) (S : Finset Edge)
       (Fs : List (Set StrictPathWitness)) :
       P.real {ω | StrictDisjointPaths S Fs (fun e => τ e ω)} ≤
         (Fs.map (fun F => P.real {ω | StrictPathEvent S F (fun e => τ e ω)})).prod := by
   …

   Mentions: OAI.GammaFPP.GammaEnvironment, OAI.GammaFPP.BK.StrictPathWitness, OAI.GammaFPP.BK.StrictDisjointPaths, OAI.GammaFPP.BK.StrictPathEvent