70structure BayesianUpdateCert where 71 cost_at_null : ∀ p : ℝ, p ≠ 0 → bayesFactorCost p p = 0 72 cost_nonneg : ∀ l p : ℝ, 0 < l → 0 < p → 0 ≤ bayesFactorCost l p 73 threshold_gt_one : 1 < bayesFactorThreshold 74 moderate_gt_two : (2 : ℝ) < bayesFactorModerate 75
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.