IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.DeltaProbability

   1/-
   2  PrimitiveRecognitionCalculus/DeltaProbability.lean
   3
   4  Delta-native probability.
   5
   6  Probability is not introduced as a real-valued measure on an arbitrary
   7  sigma-algebra. The native object here is finite: a finite distinction space,
   8  events as finite tests, and rational probabilities computed by counting.
   9
  10  This is the first probability layer needed by Delta-native analysis:
  11
  12  * `Event N`       : a finite distinction event on `Fin (N+1)`;
  13  * `prob E`        : the uniform rational probability of `E`;
  14  * `prob_empty`    : impossible event has probability zero;
  15  * `prob_univ`     : certain event has probability one;
  16  * `prob_nonneg`   : finite probabilities are nonnegative;
  17  * `prob_le_one`   : finite probabilities are bounded by one;
  18  * `prob_mono`     : finite probabilities are monotone under event inclusion;
  19  * `prob_disjoint_or`: finite additivity for disjoint events;
  20  * `expectation`   : finite rational expectation;
  21  * `delta_probability_headline` : exact finite-counting status.
  22
  23  No project-local axioms. No sorry.
  24-/
  25
  26import Mathlib
  27
  28namespace IndisputableMonolith
  29namespace Foundation
  30namespace PrimitiveRecognitionCalculus
  31namespace DeltaProbability
  32
  33/-- A finite distinction event on the nonempty finite space `Fin (N+1)`. -/
  34abbrev Event (N : ℕ) := Fin (N + 1) → Prop
  35
  36/-- Count the points satisfying a finite event. -/
  37noncomputable def count {N : ℕ} (E : Event N) : ℕ :=
  38  by
  39    classical
  40    exact (Finset.univ.filter fun i : Fin (N + 1) => E i).card
  41
  42/-- The finite set selected by an event. -/
  43noncomputable def eventFinset {N : ℕ} (E : Event N) : Finset (Fin (N + 1)) :=
  44  by
  45    classical
  46    exact Finset.univ.filter fun i : Fin (N + 1) => E i
  47
  48/-- Uniform finite probability, as a rational counting ratio. -/
  49noncomputable def prob {N : ℕ} (E : Event N) : ℚ :=
  50  (count E : ℚ) / (N + 1 : ℚ)
  51
  52theorem count_empty (N : ℕ) : count (N := N) (fun _ => False) = 0 := by
  53  classical
  54  simp [count]
  55
  56theorem count_univ (N : ℕ) : count (N := N) (fun _ => True) = N + 1 := by
  57  classical
  58  simp [count]
  59
  60theorem count_eq_card {N : ℕ} (E : Event N) : count E = (eventFinset E).card := by
  61  rfl
  62
  63/-- The impossible event has probability zero. -/
  64theorem prob_empty (N : ℕ) : prob (N := N) (fun _ => False) = 0 := by
  65  classical
  66  simp [prob, count_empty]
  67
  68/-- The certain event has probability one. -/
  69theorem prob_univ (N : ℕ) : prob (N := N) (fun _ => True) = 1 := by
  70  classical
  71  have h : ((N + 1 : ℚ) ≠ 0) := by positivity
  72  rw [prob, count_univ]
  73  rw [show (((N + 1 : ℕ) : ℚ)) = (N + 1 : ℚ) by norm_num]
  74  exact div_self h
  75
  76/-- Finite distinction probabilities are nonnegative. -/
  77theorem prob_nonneg {N : ℕ} (E : Event N) : 0 ≤ prob E := by
  78  classical
  79  unfold prob
  80  positivity
  81
  82/-- Finite distinction probabilities are bounded by one. -/
  83theorem prob_le_one {N : ℕ} (E : Event N) : prob E ≤ 1 := by
  84  classical
  85  unfold prob count
  86  have hcard : (Finset.univ.filter fun i : Fin (N + 1) => E i).card ≤ (Finset.univ : Finset (Fin (N + 1))).card :=
  87    Finset.card_filter_le _ _
  88  have hcard' : (Finset.univ.filter fun i : Fin (N + 1) => E i).card ≤ N + 1 := by
  89    simpa using hcard
  90  have hden : (0 : ℚ) < (N + 1 : ℚ) := by positivity
  91  have hcast : (((Finset.univ.filter fun i : Fin (N + 1) => E i).card : ℚ) ≤ ((N + 1 : ℕ) : ℚ)) := by
  92    exact_mod_cast hcard'
  93  rw [div_le_iff₀ hden]
  94  simpa using hcast
  95
  96/-- Event inclusion gives count monotonicity. -/
  97theorem count_mono {N : ℕ} {E F : Event N} (h : ∀ i, E i → F i) : count E ≤ count F := by
  98  classical
  99  unfold count
 100  apply Finset.card_le_card
 101  intro i hi
 102  simp only [Finset.mem_filter, Finset.mem_univ, true_and] at hi ⊢
 103  exact h i hi
 104
 105/-- Event inclusion gives probability monotonicity. -/
 106theorem prob_mono {N : ℕ} {E F : Event N} (h : ∀ i, E i → F i) : prob E ≤ prob F := by
 107  unfold prob
 108  have hden : (0 : ℚ) < (N + 1 : ℚ) := by positivity
 109  have hcount : ((count E : ℚ) ≤ (count F : ℚ)) := by
 110    exact_mod_cast count_mono h
 111  exact div_le_div_of_nonneg_right hcount (le_of_lt hden)
 112
 113/-- Disjoint finite events have additive counts. -/
 114theorem count_disjoint_or {N : ℕ} {E F : Event N}
 115    (hdisj : ∀ i, ¬ (E i ∧ F i)) :
 116    count (fun i => E i ∨ F i) = count E + count F := by
 117  classical
 118  have hunion : eventFinset (fun i : Fin (N + 1) => E i ∨ F i) = eventFinset E ∪ eventFinset F := by
 119    ext i
 120    simp [eventFinset, and_or_left]
 121  have hdf : Disjoint (eventFinset E) (eventFinset F) := by
 122    rw [Finset.disjoint_left]
 123    intro i hiE hiF
 124    simp [eventFinset] at hiE hiF
 125    exact hdisj i ⟨hiE, hiF⟩
 126  rw [count_eq_card, count_eq_card, count_eq_card, hunion]
 127  exact Finset.card_union_of_disjoint hdf
 128
 129/-- Disjoint finite events have additive probability. -/
 130theorem prob_disjoint_or {N : ℕ} {E F : Event N}
 131    (hdisj : ∀ i, ¬ (E i ∧ F i)) :
 132    prob (fun i => E i ∨ F i) = prob E + prob F := by
 133  unfold prob
 134  rw [count_disjoint_or hdisj]
 135  rw [Nat.cast_add]
 136  ring
 137
 138/-- Finite rational expectation of an observable on a finite distinction space. -/
 139noncomputable def expectation {N : ℕ} (X : Fin (N + 1) → ℚ) : ℚ :=
 140  ((Finset.univ.sum X) : ℚ) / (N + 1 : ℚ)
 141
 142theorem expectation_const {N : ℕ} (c : ℚ) :
 143    expectation (N := N) (fun _ => c) = c := by
 144  have h : ((N + 1 : ℚ) ≠ 0) := by positivity
 145  simp [expectation, Finset.sum_const]
 146  field_simp [h]
 147
 148/-- **Delta-native probability headline.** Probability at the native finite layer
 149is rational counting over finite distinction alternatives: impossible event zero,
 150certain event one, and every event has probability in `[0,1]`. -/
 151theorem delta_probability_headline (N : ℕ) :
 152    prob (N := N) (fun _ => False) = 0
 153      ∧ prob (N := N) (fun _ => True) = 1
 154      ∧ (∀ E : Event N, 0 ≤ prob E ∧ prob E ≤ 1)
 155      ∧ (∀ E F : Event N, (∀ i, E i → F i) → prob E ≤ prob F)
 156      ∧ (∀ E F : Event N, (∀ i, ¬ (E i ∧ F i)) →
 157          prob (fun i => E i ∨ F i) = prob E + prob F) :=
 158  ⟨prob_empty N, prob_univ N, fun E => ⟨prob_nonneg E, prob_le_one E⟩,
 159    fun _ _ h => prob_mono h, fun _ _ h => prob_disjoint_or h⟩
 160
 161end DeltaProbability
 162end PrimitiveRecognitionCalculus
 163end Foundation
 164end IndisputableMonolith
 165