def
definition
bayesFactorModerate
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Statistics.BayesianUpdateFromJCost on GitHub at line 60.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
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
74 moderate_gt_two : (2 : ℝ) < bayesFactorModerate
75
76noncomputable def cert : BayesianUpdateCert where
77 cost_at_null := bayesFactorCost_at_null
78 cost_nonneg := bayesFactorCost_nonneg
79 threshold_gt_one := bayesFactorThreshold_gt_one
80 moderate_gt_two := bayesFactorModerate_gt_two
81
82theorem cert_inhabited : Nonempty BayesianUpdateCert := ⟨cert⟩
83
84end
85end BayesianUpdateFromJCost
86end Statistics
87end IndisputableMonolith