bayesFactorCost_at_null

formal source

  40def bayesFactorCost (likelihood prior : ℝ) : ℝ :=
  41  Jcost (likelihood / prior)
  42
  43theorem bayesFactorCost_at_null (p : ℝ) (h : p ≠ 0) :
  44    bayesFactorCost p p = 0 := by
  45  unfold bayesFactorCost; rw [div_self h]; exact Jcost_unit0
  46
  47theorem bayesFactorCost_nonneg (l p : ℝ) (hl : 0 < l) (hp : 0 < p) :
  48    0 ≤ bayesFactorCost l p := by
  49  unfold bayesFactorCost; exact Jcost_nonneg (div_pos hl hp)
  50
  51/-- Barely-convincing Bayes factor: B = φ. -/
  52def bayesFactorThreshold : ℝ := phi
  53
  54theorem bayesFactorThreshold_gt_one : 1 < bayesFactorThreshold := one_lt_phi
  55
  56theorem bayesFactorThreshold_cost : Jcost bayesFactorThreshold = phi - 3 / 2 := by
  57  unfold bayesFactorThreshold; exact Jcost_phi_val
  58
  59/-- Moderate evidence: B = φ². -/
  60def bayesFactorModerate : ℝ := phi ^ (2 : ℕ)
  61
  62theorem bayesFactorModerate_pos : 0 < bayesFactorModerate := by
  63  unfold bayesFactorModerate; exact pow_pos phi_pos _
  64
  65theorem bayesFactorModerate_gt_two : (2 : ℝ) < bayesFactorModerate := by
  66  unfold bayesFactorModerate
  67  have h := phi_squared_bounds
  68  linarith [h.1]
  69
  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