OAI/Probability/CriticalZ3/ConditionalQuality.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.InfiniteConditioning.conditionalProbability line 13
2. theorem OAI.InfiniteConditioning.conditionalProbability_determined line 18
3. theorem OAI.InfiniteConditioning.conditional_failure_mass line 26

   Source documentation

   Reveal-wise tower/Markov bound, valid also for histories of zero mass.

   theorem conditional_failure_mass (p : E → Set.Icc (0 : ℝ) 1) (J : Finset E)
       (H C : Set (E → Bool))
       (hH : ProductCylinder.DeterminedBy (F := Prop) J (fun ω => ω ∈ H))
   …

   Mentions: OAI.ProductCylinder.DeterminedBy

4. theorem OAI.InfiniteConditioning.conditional_failure_bound line 77