eventRatio_pos

formal source

  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