EventNonempty

formal source

  26  ∑ i, if event i then R.weight i else 0
  27
  28/-- A positive witness for an event. -/
  29def EventNonempty {n : Nat} (event : Fin n → Bool) : Prop :=
  30  ∃ i, event i = true
  31
  32/-- Nonempty finite Boolean events have positive weight. -/
  33theorem eventWeight_pos {n : Nat} (R : FiniteBooleanReality n)
  34    (event : Fin n → Bool) (hNonempty : EventNonempty event) :
  35    0 < R.eventWeight event := by
  36  rcases hNonempty with ⟨i₀, hi₀⟩
  37  unfold eventWeight
  38  have h_nonneg : ∀ i : Fin n, 0 ≤ (if event i then R.weight i else 0) := by
  39    intro i
  40    by_cases h : event i
  41    · simp [h, le_of_lt (R.positive_weight i)]
  42    · simp [h]
  43  have h_i0_pos : 0 < (if event i₀ then R.weight i₀ else 0) := by
  44    simp [hi₀, R.positive_weight i₀]
  45  have h_le_sum :
  46      (if event i₀ then R.weight i₀ else 0) ≤
  47        ∑ i, if event i then R.weight i else 0 := by
  48    exact Finset.single_le_sum (fun i _ => h_nonneg i) (Finset.mem_univ i₀)
  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) :