def
definition
eventRatio
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.LogicAsFunctionalEquation.BooleanRatioBridge on GitHub at line 52.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
49 exact lt_of_lt_of_le h_i0_pos h_le_sum
50
51/-- Likelihood ratio of two events. -/
52noncomputable def eventRatio {n : Nat} (R : FiniteBooleanReality n)
53 (A B : Fin n → Bool) : ℝ :=
54 R.eventWeight A / R.eventWeight B
55
56/-- Nonempty event comparisons land in positive ratios. -/
57theorem eventRatio_pos {n : Nat} (R : FiniteBooleanReality n)
58 (A B : Fin n → Bool)
59 (hA : EventNonempty A) (hB : EventNonempty B) :
60 0 < R.eventRatio A B := by
61 unfold eventRatio
62 exact div_pos (eventWeight_pos R A hA) (eventWeight_pos R B hB)
63
64/-- Finite Boolean comparison embeds into the positive-ratio domain whenever
65both compared events have positive measure. -/
66theorem finite_boolean_logic_embeds_into_positive_ratios {n : Nat}
67 (R : FiniteBooleanReality n)
68 (A B : Fin n → Bool)
69 (hA : EventNonempty A) (hB : EventNonempty B) :
70 ∃ r : ℝ, 0 < r ∧ r = R.eventRatio A B :=
71 ⟨R.eventRatio A B, eventRatio_pos R A B hA hB, rfl⟩
72
73end FiniteBooleanReality
74
75end LogicAsFunctionalEquation
76end Foundation
77end IndisputableMonolith