OAI/Probability/GammaPassage/BKPathMeasurability.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GammaFPP.BK.continuous_pathCost line 11
2. def OAI.GammaFPP.BK.PositiveStrictDisjointPaths line 18

   Source documentation

   Positive survival probabilities separate finite quantile costs from infinity cells.

   def PositiveStrictDisjointPaths (S : Finset Edge) (Fs : List (Set StrictPathWitness))
       (z : (Edge → ℝ) × (Edge → ℝ)) : Prop :=
   …

   Mentions: OAI.GammaFPP.BK.StrictPathWitness

3. lemma OAI.GammaFPP.BK.isOpen_positiveStrictDisjointPaths line 27

   Source documentation

   Arbitrary labelled families are allowed: openness handles unions over the bounds without incorrectly requiring their labels to form a countable set.

   lemma isOpen_positiveStrictDisjointPaths (S : Finset Edge) (Fs : List (Set StrictPathWitness)) :
       IsOpen {z | PositiveStrictDisjointPaths S Fs z} := by
   …

   Mentions: OAI.GammaFPP.BK.StrictPathWitness, OAI.GammaFPP.BK.PositiveStrictDisjointPaths

4. lemma OAI.GammaFPP.BK.strictDisjointPaths_positive_iff line 50
5. lemma OAI.GammaFPP.BK.isOpen_strictDisjointPaths line 59
6. lemma OAI.GammaFPP.BK.measurableSet_strictDisjointPaths line 65
7. lemma OAI.GammaFPP.BK.isOpen_strictPathEvent line 68
8. lemma OAI.GammaFPP.BK.measurableSet_strictPathEvent line 78
9. lemma OAI.GammaFPP.BK.measurable_gammaRoundedSurvival line 82
10. lemma OAI.GammaFPP.BK.measurable_gammaRoundedCost line 89
11. lemma OAI.GammaFPP.BK.measurableSet_roundedDisjoint line 94