FiniteBooleanReality

formal source

  14namespace LogicAsFunctionalEquation
  15
  16/-- A finite weighted Boolean reality over `Fin n`. -/
  17structure FiniteBooleanReality (n : Nat) where
  18  weight : Fin n → ℝ
  19  positive_weight : ∀ i, 0 < weight i
  20
  21namespace FiniteBooleanReality
  22
  23/-- The weight of an event. -/
  24noncomputable def eventWeight {n : Nat} (R : FiniteBooleanReality n)
  25    (event : Fin n → Bool) : ℝ :=
  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