From 1525aa995ccd1d158022905c54e3db9c120f6cf1 Mon Sep 17 00:00:00 2001 From: Keith Badger Date: Tue, 21 Oct 2025 11:49:11 -0400 Subject: [PATCH 1/6] Please add directly to main --- Probability/Basic.lean | 351 +++++++++++++++++++++-------------------- 1 file changed, 176 insertions(+), 175 deletions(-) diff --git a/Probability/Basic.lean b/Probability/Basic.lean index 10e125a..8888dae 100644 --- a/Probability/Basic.lean +++ b/Probability/Basic.lean @@ -1,11 +1,12 @@ +--Please add to main pretty pretty please import Mathlib.Data.Nat.Basic -import Mathlib.Data.Real.Basic +import Mathlib.Data.Real.Basic import Mathlib.Data.Rat.Defs import Mathlib.Data.NNReal.Basic -import Mathlib.Logic.Function.Defs +import Mathlib.Logic.Function.Defs -import Mathlib.Data.Set.Basic +import Mathlib.Data.Set.Basic import Mathlib.Data.Finset.Defs import Mathlib.Data.Finset.Image @@ -16,7 +17,7 @@ import Mathlib.Algebra.Group.Pi.Basic -- for Pi.single open NNReal -variable {τ : Type} +variable {τ : Type} section Indicator @@ -27,7 +28,7 @@ abbrev 𝕀 : Bool → ℚ := indicator /-- Indicator is 0 or 1 -/ theorem ind_zero_one (cond : τ → Bool) (ω : τ) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by - by_cases h : cond ω + by_cases h : cond ω · left; simp only [Function.comp_apply, h, indicator] · right; simp only [Function.comp_apply, h, indicator] @@ -39,12 +40,12 @@ end Indicator @[simp] abbrev Prob (p : ℚ) : Prop := 0 ≤ p ∧ p ≤ 1 -namespace Prob +namespace Prob -variable {p x y : ℚ} +variable {p x y : ℚ} @[simp] -theorem of_complement ( hp : Prob p) : Prob (1-p) := by +theorem of_complement ( hp : Prob p) : Prob (1-p) := by simp_all only [ Prob, sub_nonneg, tsub_le_iff_right, le_add_iff_nonneg_right, and_self] @[simp] @@ -54,13 +55,13 @@ theorem lower_bound_fst (hp : Prob p) (h : x ≤ y) : x ≤ p * x + (1-p) * y := have h2 : (1-p) * x ≤ (1-p) * y := mul_le_mul_of_nonneg_left h hp.of_complement.1 linarith -theorem lower_bound_snd (hp : Prob p) (h : y ≤ x) : y ≤ p * x + (1-p) * y := by +theorem lower_bound_snd (hp : Prob p) (h : y ≤ x) : y ≤ p * x + (1-p) * y := by have h2 : p * y ≤ p * x := mul_le_mul_of_nonneg_left h hp.1 linarith theorem upper_bound_fst (hp : Prob p) (h : y ≤ x) : p * x + (1-p) * y ≤ x := by have h2 : (1-p) * y ≤ (1-p) * x := mul_le_mul_of_nonneg_left h hp.of_complement.1 - linarith + linarith theorem upper_bound_snd (hp : Prob p) (h : x ≤ y) : p * x + (1-p) * y ≤ y := by have h2 : p * x ≤ p * y := mul_le_mul_of_nonneg_left h hp.1 @@ -78,16 +79,16 @@ variable {L : List ℚ} def scale (L : List ℚ) (c : ℚ) : List ℚ := (L.map fun x↦x*c) --- TODO: find the theorem in mathlib that does this -theorem nonempty_length_gt_one (h : ¬L.isEmpty) : L.length ≥ 1 := +-- TODO: find the theorem in mathlib that does this +theorem nonempty_length_gt_one (h : ¬L.isEmpty) : L.length ≥ 1 := by simp_all - cases L + cases L · contradiction · exact tsub_add_cancel_iff_le.mp rfl @[simp] -theorem scale_sum : (L.scale c).sum = c * L.sum := +theorem scale_sum : (L.scale c).sum = c * L.sum := by induction L · simp [scale] · simp_all [scale] @@ -96,19 +97,19 @@ theorem scale_sum : (L.scale c).sum = c * L.sum := @[simp] theorem scale_length : (L.scale c).length = L.length := by simp [scale] -theorem scale_nneg_of_nneg (h : ∀l ∈ L, 0 ≤ l) (h1 : 0 ≤ c) : (∀l ∈ L.scale c, 0 ≤ l) := - by induction L +theorem scale_nneg_of_nneg (h : ∀l ∈ L, 0 ≤ l) (h1 : 0 ≤ c) : (∀l ∈ L.scale c, 0 ≤ l) := + by induction L · simp [List.scale] · simp_all [List.scale] exact Left.mul_nonneg h.1 h1 - -theorem append_nneg_of_nneg (h : ∀l ∈ L, 0 ≤ l) (h1 : 0 ≤ p) : (∀l ∈ p::L, 0 ≤ l) := + +theorem append_nneg_of_nneg (h : ∀l ∈ L, 0 ≤ l) (h1 : 0 ≤ p) : (∀l ∈ p::L, 0 ≤ l) := by aesop /-- adds a new probability to a list and renormalizes the rest --/ -def grow (L : List ℚ) (p : ℚ) : List ℚ := p :: (L.scale (1-p)) - -theorem grow_sum : (L.grow p).sum = L.sum * (1-p) + p := +def grow (L : List ℚ) (p : ℚ) : List ℚ := p :: (L.scale (1-p)) + +theorem grow_sum : (L.grow p).sum = L.sum * (1-p) + p := by induction L · simp [List.grow, List.scale] · simp [List.grow, List.scale_sum] @@ -120,28 +121,28 @@ def shrink : List ℚ → List ℚ | nil => nil | head :: tail => tail.scale (1-head)⁻¹ - + @[simp] -theorem shrink_length : L.shrink.length = L.tail.length := +theorem shrink_length : L.shrink.length = L.tail.length := by cases L; simp [List.shrink]; simp[List.shrink, List.scale] theorem shrink_length_less_one : L.shrink.length = L.length - 1 := by simp only [shrink_length, length_tail] - - + + @[simp] -theorem shrink_sum (npt: L ≠ []) (h : L.head npt < 1) : - (L.shrink).sum = (L.tail).sum / (1 - L.head npt) := +theorem shrink_sum (npt: L ≠ []) (h : L.head npt < 1) : + (L.shrink).sum = (L.tail).sum / (1 - L.head npt) := by cases L; contradiction; simp_all [List.shrink, List.scale_sum]; ring -theorem shrink_ge0 (h1 : ∀l ∈ L, Prob l) : ∀l ∈ (L.shrink), 0 ≤ l := +theorem shrink_ge0 (h1 : ∀l ∈ L, Prob l) : ∀l ∈ (L.shrink), 0 ≤ l := by simp [List.shrink] cases L with | nil => simp_all only [List.not_mem_nil, IsEmpty.forall_iff, implies_true] - | cons head tail => + | cons head tail => simp_all only [List.mem_cons, Prob, forall_eq_or_imp] have hh : 0 ≤ (1-head)⁻¹ := Prob.complement_inv_nneg h1.1 - exact List.scale_nneg_of_nneg (L:=tail) (c:=(1-head)⁻¹) (fun l a ↦ (h1.2 l a).1) hh + exact List.scale_nneg_of_nneg (L:=tail) (c:=(1-head)⁻¹) (fun l a ↦ (h1.2 l a).1) hh end List end List @@ -156,11 +157,11 @@ variable {p : ℚ} structure LSimplex (L : List ℚ) : Prop where nneg : ∀p ∈ L, 0 ≤ p -- separate for convenience normalized : L.sum = 1 -- sums to 1 - + namespace LSimplex -def singleton : LSimplex [1] := - ⟨fun p a => by simp_all only [List.mem_cons, List.not_mem_nil, or_false, zero_le_one], +def singleton : LSimplex [1] := + ⟨fun p a => by simp_all only [List.mem_cons, List.not_mem_nil, or_false, zero_le_one], List.sum_singleton⟩ variable {L : List ℚ} {c : ℚ} @@ -168,10 +169,10 @@ variable (S : LSimplex L) /-- cannot define a simplex on an empty set -/ @[simp] -theorem nonempty (S : LSimplex L) : L ≠ [] := - fun a => by have := S.normalized; simp_all - -@[simp] +theorem nonempty (S : LSimplex L) : L ≠ [] := + fun a => by have := S.normalized; simp_all + +@[simp] abbrev npt : LSimplex L → L ≠ [] := LSimplex.nonempty def phead (h : LSimplex L) : ℚ := L.head h.nonempty @@ -183,32 +184,32 @@ def degenerate (S : LSimplex L) : Bool := S.phead == 1 def supported : Bool := ¬S.degenerate @[simp] -theorem mem_prob (S : LSimplex L) : ∀ p ∈ L, Prob p := - fun p a => ⟨ S.nneg p a, +theorem mem_prob (S : LSimplex L) : ∀ p ∈ L, Prob p := + fun p a => ⟨ S.nneg p a, S.normalized ▸ List.single_le_sum S.nneg p a⟩ - + theorem phead_inpr : S.phead ∈ L := List.head_mem S.nonempty @[simp] theorem phead_prob : Prob S.phead := S.mem_prob S.phead S.phead_inpr - + theorem phead_supp (supp : S.supported) : S.phead < 1 := by simp [degenerate] at supp - exact lt_of_le_of_ne S.phead_prob.2 supp + exact lt_of_le_of_ne S.phead_prob.2 supp theorem supported_head_lt_one (supp : S.supported) : L.head S.npt < 1 := by have prob := LSimplex.mem_prob S (L.head S.npt) (List.head_mem (LSimplex.npt S)) - simp [LSimplex.degenerate] at supp - simp [Prob] at prob + simp [LSimplex.degenerate] at supp + simp [Prob] at prob exact lt_of_le_of_ne prob.2 supp @[simp] -theorem List.grow_ge0 (h1 : ∀l ∈ L, 0 ≤ l) (h2 : Prob p) : ∀ l ∈ (L.grow p), 0 ≤ l := +theorem List.grow_ge0 (h1 : ∀l ∈ L, 0 ≤ l) (h2 : Prob p) : ∀ l ∈ (L.grow p), 0 ≤ l := by simp [List.grow] constructor · exact h2.1 · intro l a - exact List.scale_nneg_of_nneg + exact List.scale_nneg_of_nneg (L := L) (c := (1-p)) h1 (Prob.of_complement h2).1 l a -- grows the simplex to also incude the probability p @@ -218,9 +219,9 @@ theorem grow (S : LSimplex L) {p : ℚ} (prob : Prob p) : LSimplex (L.grow p) := normalized := by simp [List.grow_sum, S.normalized]} lemma false_of_p_comp1_zero_p_less_one (h1 : 1 - p = 0) (h2 : p < 1) : False := by linarith - + @[simp] -theorem tail_sum (S : LSimplex L) : L.tail.sum = (1 - L.head S.npt) := +theorem tail_sum (S : LSimplex L) : L.tail.sum = (1 - L.head S.npt) := by cases L; have := S.npt; contradiction; have := S.normalized; simp at this ⊢; linarith theorem degenerate_tail_zero (degen : S.degenerate) : ∀ p ∈ L.tail, p = 0 := @@ -238,27 +239,27 @@ theorem degenerate_tail_zero (degen : S.degenerate) : ∀ p ∈ L.tail, p = 0 := theorem shrink (S : LSimplex L) (supp : S.supported) : LSimplex (L.shrink) := {nneg := List.shrink_ge0 (LSimplex.mem_prob S), - normalized := + normalized := by have npt := S.npt have hh := LSimplex.supported_head_lt_one S supp - have hh1 := S.tail_sum + have hh1 := S.tail_sum have hh2 : (1 - L.head npt) ≠ 0 := by linarith rw[List.shrink_sum S.npt hh] exact (div_eq_one_iff_eq hh2).mpr hh1} - -theorem grow_of_shrink_list (supp : S.supported) : L = (L.shrink).grow (S.phead) := + +theorem grow_of_shrink_list (supp : S.supported) : L = (L.shrink).grow (S.phead) := by induction L with - | nil => have := S.nonempty; contradiction - | cons head tail => - let h : (1-head) ≠ 0 := + | nil => have := S.nonempty; contradiction + | cons head tail => + let h : (1-head) ≠ 0 := fun a => false_of_p_comp1_zero_p_less_one a (S.phead_supp supp) simp_all [List.grow, List.shrink, List.scale, LSimplex.phead] -- all props of the same type are equal -theorem grow_of_shrink (supp : S.supported) : +theorem grow_of_shrink (supp : S.supported) : S = (S.grow_of_shrink_list supp) ▸ (S.shrink supp).grow S.phead_prob := rfl -end LSimplex +end LSimplex end LSimplex ---------------- FinDist ---------------------------------------------------- @@ -271,21 +272,21 @@ structure Findist (N : ℕ) : Type where lmatch : ℙ.length = N -- correct length of probability namespace Findist - + abbrev Delta : ℕ → Type := Findist abbrev Δ : ℕ → Type := Delta -variable {N : ℕ} (F : Findist N) +variable {N : ℕ} (F : Findist N) abbrev degenerate : Bool := F.simplex.degenerate abbrev supported : Bool := F.simplex.supported -theorem supp_not_degen (supp : F.supported) : ¬ F.degenerate := +theorem supp_not_degen (supp : F.supported) : ¬ F.degenerate := by simp_all [supported, degenerate] - + @[simp] theorem nonempty (F : Findist N) : N ≥ 1 := - F.lmatch ▸ List.length_pos_iff.mpr F.simplex.npt + F.lmatch ▸ List.length_pos_iff.mpr F.simplex.npt @[simp] theorem nonempty_P : F.ℙ ≠ [] := @@ -296,30 +297,30 @@ theorem nonempty_P : F.ℙ ≠ [] := /-- add a new head -/ def grow {p : ℚ} (prob : Prob p) : Findist (N + 1) := {ℙ := F.ℙ.grow p, - simplex := F.simplex.grow prob, + simplex := F.simplex.grow prob, lmatch := by simp [List.grow, List.scale_length, F.lmatch]} /-- if nondegenenrate then construct a tail distribution -/ def shrink (supp : F.supported) : Findist (N - 1) := -- see: https://lean-lang.org/theorem_proving_in_lean4/The-Conversion-Tactic-Mode/ - let hh : F.ℙ.shrink.length = N - 1 := - calc - F.ℙ.shrink.length = F.ℙ.length - 1 := List.shrink_length_less_one + let hh : F.ℙ.shrink.length = N - 1 := + calc + F.ℙ.shrink.length = F.ℙ.length - 1 := List.shrink_length_less_one _ = N - 1 := by conv => lhs; rw [F.lmatch] {ℙ := F.ℙ.shrink - simplex := F.simplex.shrink supp + simplex := F.simplex.shrink supp lmatch := hh} --List.shrink_length_less_one (Findist.nonempty_P F)} -def singleton : Findist 1 := - {ℙ := [1] +def singleton : Findist 1 := + {ℙ := [1] simplex := LSimplex.singleton, lmatch := by simp_all only [List.length_cons, List.length_nil, zero_add]} - -abbrev phead := F.simplex.phead ---example (a : Prop) (b : Prop) : ¬(a ∧ b) = (¬ a) ∨ (¬b) := +abbrev phead := F.simplex.phead + +--example (a : Prop) (b : Prop) : ¬(a ∧ b) = (¬ a) ∨ (¬b) := @[simp] theorem phead_inpr : F.phead ∈ F.ℙ := List.head_mem F.nonempty_P @@ -327,9 +328,9 @@ theorem phead_inpr : F.phead ∈ F.ℙ := List.head_mem F.nonempty_P @[simp] theorem phead_prob : Prob F.phead := F.simplex.mem_prob F.phead F.phead_inpr -theorem nondegenerate_head (supp : F.supported) : F.phead < 1 := +theorem nondegenerate_head (supp : F.supported) : F.phead < 1 := by have h1 := Findist.phead_prob F - simp_all only [supported, LSimplex.supported, LSimplex.degenerate, + simp_all only [supported, LSimplex.supported, LSimplex.degenerate, LSimplex.phead, beq_iff_eq, phead, gt_iff_lt] simp! only [decide_not, Bool.not_eq_eq_eq_not, not, decide_eq_false_iff_not] at supp simp [Prob] at h1 @@ -338,25 +339,25 @@ theorem nondegenerate_head (supp : F.supported) : F.phead < 1 := -- For the use of ▸ see: https://proofassistants.stackexchange.com/questions/1380/how-do-i-convince-the-lean-4-type-checker-that-addition-is-commutative -theorem grow_shrink_type (_ : F.supported) : Findist (N - 1 + 1) = Findist N := +theorem grow_shrink_type (_ : F.supported) : Findist (N - 1 + 1) = Findist N := (Nat.sub_add_cancel F.nonempty) ▸ rfl -def growshrink (supp : F.supported) : Findist (N-1+1) := - (F.shrink supp).grow F.phead_prob +def growshrink (supp : F.supported) : Findist (N-1+1) := + (F.shrink supp).grow F.phead_prob -- TODO: can we incorporate this example in the theorem below? example (supp : F.supported) : ((F.shrink supp).grow F.phead_prob).ℙ = F.ℙ := - by have h1 : F.supported := by simp_all only + by have h1 : F.supported := by simp_all only simp [Findist.shrink, Findist.grow, Findist.phead] - rw [←LSimplex.grow_of_shrink_list F.simplex h1] - + rw [←LSimplex.grow_of_shrink_list F.simplex h1] -theorem grow_of_shrink_2 (supp : F.supported) : + +theorem grow_of_shrink_2 (supp : F.supported) : F.growshrink supp = ((F.grow_shrink_type supp).mpr F) := - by have h1 : F.supported := by simp_all only + by have h1 : F.supported := by simp_all only simp [Findist.growshrink, Findist.shrink, Findist.grow, Findist.phead] rw [Findist.mk.injEq] - rw [←LSimplex.grow_of_shrink_list F.simplex h1] + rw [←LSimplex.grow_of_shrink_list F.simplex h1] congr; --TODO: here to deal with casts; need to understand them better (see example below) symm; exact Nat.sub_add_cancel F.nonempty; simp_all only [heq_cast_iff_heq, heq_eq_eq] @@ -369,65 +370,65 @@ end Findist structure Finprob : Type where ℙ : List ℚ prob : LSimplex ℙ - -lemma List.unique_head_notin_tail (L : List τ) (ne : L ≠ []) (nodup : L.Nodup) : - L.head ne ∉ L.tail := + +lemma List.unique_head_notin_tail (L : List τ) (ne : L ≠ []) (nodup : L.Nodup) : + L.head ne ∉ L.tail := by induction L - · simp at ne + · simp at ne · simp [List.head, List.tail] simp_all only [ne_eq, reduceCtorEq, not_false_eq_true, List.nodup_cons] -namespace Finprob +namespace Finprob variable (P : Finprob) @[simp] -def length := P.ℙ.length - +def length := P.ℙ.length -def singleton : Finprob := + +def singleton : Finprob := ⟨ [1], LSimplex.singleton ⟩ def grow {p : ℚ} (prob : Prob p) : Finprob := ⟨P.ℙ.grow p, P.prob.grow prob⟩ - + /-- all probability in the head -/ abbrev degenerate : Bool := P.prob.degenerate abbrev supported : Bool := P.prob.supported -theorem not_degen_supp (supp : ¬P.degenerate) : P.supported := - by simp_all [Finprob.degenerate, Finprob.supported] +theorem not_degen_supp (supp : ¬P.degenerate) : P.supported := + by simp_all [Finprob.degenerate, Finprob.supported] -theorem degen_of_not_supp (notsupp : ¬P.supported) : P.degenerate := - by simp_all [Finprob.degenerate, Finprob.supported] +theorem degen_of_not_supp (notsupp : ¬P.supported) : P.degenerate := + by simp_all [Finprob.degenerate, Finprob.supported] -def shrink (supp : P.supported) : Finprob := +def shrink (supp : P.supported) : Finprob := {ℙ := P.ℙ.shrink, prob := P.prob.shrink supp} - + -- Define an induction principle for probability spaces -- similar to the induction on lists, but also must argue about probability distributions -theorem nonempty : ¬P.ℙ.isEmpty := - by intro a; +theorem nonempty : ¬P.ℙ.isEmpty := + by intro a; simp_all only [LSimplex.nonempty P.prob, List.isEmpty_iff] -theorem length_gt_zero : P.length ≥ 1 := +theorem length_gt_zero : P.length ≥ 1 := by simp [Finprob.length] exact List.nonempty_length_gt_one (P.nonempty) -theorem shrink_length (supp : P.supported) : (P.shrink supp).length = P.length - 1 := +theorem shrink_length (supp : P.supported) : (P.shrink supp).length = P.length - 1 := by have h := Finprob.nonempty P simp [List.isEmpty] at h simp! [Finprob.shrink, Finprob.length, List.shrink, LSimplex.shrink] - -theorem shrink_length_lt (supp : P.supported) : (P.shrink supp).length < P.length := + +theorem shrink_length_lt (supp : P.supported) : (P.shrink supp).length < P.length := by rw [Finprob.shrink_length P supp] exact Nat.sub_one_lt_of_lt (Finprob.length_gt_zero P) theorem nonempty_P : P.ℙ ≠ [] := P.prob.nonempty - + @[simp] def phead := P.ℙ.head P.nonempty_P @@ -435,11 +436,11 @@ def phead := P.ℙ.head P.nonempty_P def ωhead := P.length - 1 theorem phead_inpr : P.phead ∈ P.ℙ := List.head_mem P.nonempty_P - -theorem phead_prob : Prob P.phead := + +theorem phead_prob : Prob P.phead := P.prob.mem_prob P.phead P.phead_inpr -theorem phead_supp_ne_one (supp : P.supported) : P.phead ≠ 1 := +theorem phead_supp_ne_one (supp : P.supported) : P.phead ≠ 1 := by simp [Finprob.supported, LSimplex.supported, LSimplex.degenerate, LSimplex.phead] at supp simp [Finprob.phead] exact supp @@ -451,27 +452,27 @@ theorem len_ge_one : P.length ≥ 1 := exact Nat.one_le_iff_ne_zero.mpr this -theorem shrink_shorter (supp : P.supported) : +theorem shrink_shorter (supp : P.supported) : (P.shrink supp).length = P.length - 1 := by simp_all only [length, shrink, List.shrink_length, List.length_tail] -/-- Shows that growing an shrink probability will create the same probability space -/ -theorem grow_of_shrink (supp : P.supported) : P = (P.shrink supp).grow P.phead_prob := +/-- Shows that growing an shrink probability will create the same probability space -/ +theorem grow_of_shrink (supp : P.supported) : P = (P.shrink supp).grow P.phead_prob := by rw [Finprob.mk.injEq] -- same fields equivalent to same structures simp [Finprob.shrink, Finprob.grow] - apply LSimplex.grow_of_shrink_list + apply LSimplex.grow_of_shrink_list simp_all only [decide_not, Bool.decide_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true, Bool.false_eq_true, decide_false, Bool.not_false] exact P.prob - + /-- induction principle for finite probabilities. Works as "induction P" -/ @[induction_eliminator] -def induction {motive : Finprob → Prop} +def induction {motive : Finprob → Prop} (degenerate : {fp : Finprob} → (d : fp.degenerate) → motive fp) - (composite : (tail : Finprob) → {p : ℚ} → (inP : Prob p) → - (motive tail) → motive (tail.grow inP)) - (P : Finprob) : motive P := + (composite : (tail : Finprob) → {p : ℚ} → (inP : Prob p) → + (motive tail) → motive (tail.grow inP)) + (P : Finprob) : motive P := if b1 : P.ℙ = [] then by have := LSimplex.nonempty P.prob; simp_all else @@ -479,14 +480,14 @@ def induction {motive : Finprob → Prop} degenerate b2 else let indhyp := Finprob.induction degenerate composite (P.shrink (P.not_degen_supp b2)) - (Finprob.grow_of_shrink P (P.not_degen_supp b2)) ▸ + (Finprob.grow_of_shrink P (P.not_degen_supp b2)) ▸ composite (P.shrink (P.not_degen_supp b2)) P.phead_prob indhyp termination_by P.length - decreasing_by + decreasing_by simp only [length, shrink, gt_iff_lt] exact Finprob.shrink_length_lt P (P.not_degen_supp b2) -end Finprob +end Finprob ------------------------------ Section Finrv ----------------------------------- section RandomVariable @@ -496,7 +497,7 @@ section RandomVariable def FinRV (ρ : Type) := ℕ → ρ -namespace FinRV +namespace FinRV @[simp] def and (B : FinRV Bool) (C : FinRV Bool) : FinRV Bool := fun ω ↦ B ω && C ω @@ -516,20 +517,20 @@ def not (B : FinRV Bool) : FinRV Bool := prefix:40 "¬ᵣ" => FinRV.not -@[simp] -def eq {η : Type} [DecidableEq η] (Y : FinRV η) (y : η) : FinRV Bool := +@[simp] +def eq {η : Type} [DecidableEq η] (Y : FinRV η) (y : η) : FinRV Bool := (fun ω ↦ decide (Y ω = y) ) infix:50 "=ᵣ" => FinRV.eq @[simp] -def leq {η : Type} [LE η] [DecidableLE η] (Y : FinRV η) (y : η) : FinRV Bool := +def leq {η : Type} [LE η] [DecidableLE η] (Y : FinRV η) (y : η) : FinRV Bool := (fun ω ↦ Y ω ≤ y) infix:50 "≤ᵣ" => FinRV.leq /-- Shows equivalence when extending the random variable to another element. -/ -theorem le_of_le_eq (D : FinRV ℕ) (n : ℕ) : ((D ≤ᵣ n) ∨ᵣ (D =ᵣ n.succ)) = (D ≤ᵣ n.succ) := by +theorem le_of_le_eq (D : FinRV ℕ) (n : ℕ) : ((D ≤ᵣ n) ∨ᵣ (D =ᵣ n.succ)) = (D ≤ᵣ n.succ) := by funext x --extensionality principle for functions unfold FinRV.leq FinRV.eq FinRV.or grind only [cases Or] @@ -548,14 +549,14 @@ def List.iprodb (ℙ : List ℚ) (B : FinRV Bool) : ℚ := match ℙ with | [] => 0 | head :: tail => (B tail.length).rec 0 head + tail.iprodb B - + variable (P : Finprob) (B : FinRV Bool) (C : FinRV Bool) variable (L : List ℚ) -theorem List.scale_innerprod (x : ℚ) : (L.scale x).iprodb B = x * (L.iprodb B) := +theorem List.scale_innerprod (x : ℚ) : (L.scale x).iprodb B = x * (L.iprodb B) := by induction L with | nil => simp_all [List.scale, List.iprodb] | cons head tail => @@ -564,22 +565,22 @@ theorem List.scale_innerprod (x : ℚ) : (L.scale x).iprodb B = x * (L.iprodb B · simp_all · simp_all ring - -theorem List.decompose_supp (h : L ≠ []) (ne1 : L.head h ≠ 1): + +theorem List.decompose_supp (h : L ≠ []) (ne1 : L.head h ≠ 1): L.iprodb B = (B (L.length - 1)).rec 0 (L.head h) + (1-L.head h) * (L.shrink.iprodb B) := by conv => lhs; unfold iprodb cases L with | nil => simp at h - | cons head tail => + | cons head tail => simp [List.shrink] have := tail.scale_innerprod B (1-head)⁻¹ simp_all - have hnz : 1 - head ≠ 0 := - by by_contra; have : head = 1 := by linarith; + have hnz : 1 - head ≠ 0 := + by by_contra; have : head = 1 := by linarith; contradiction - calc + calc tail.iprodb B = 1 * tail.iprodb B := by ring - _ = (1 - head) * (1 - head)⁻¹ * tail.iprodb B := + _ = (1 - head) * (1 - head)⁻¹ * tail.iprodb B := by rw [Rat.mul_inv_cancel (1-head) hnz] _ = (1 - head) * ((1 - head)⁻¹ * tail.iprodb B ) := by ring @@ -590,13 +591,13 @@ theorem List.iprod_eq_zero_of_zeros (hz : ∀ p ∈ L, p = 0) : L.iprodb B = 0 : theorem List.iprod_first_of_tail_zero (hn : L ≠ []) (hz : ∀ p ∈ L.tail, p = 0) : - L.iprodb B = (B L.tail.length).rec 0 (L.head hn) := + L.iprodb B = (B L.tail.length).rec 0 (L.head hn) := by unfold iprodb cases L · contradiction · simp; simp at hz; (expose_names; exact iprod_eq_zero_of_zeros B tail hz) -lemma List.iprodb_true_sum : L.iprodb (fun _ ↦ true) = L.sum := +lemma List.iprodb_true_sum : L.iprodb (fun _ ↦ true) = L.sum := by induction L · simp only [iprodb, sum_nil] · simp_all only [iprodb, sum_cons] @@ -605,56 +606,56 @@ lemma List.iprodb_true_sum : L.iprodb (fun _ ↦ true) = L.sum := /-- Probability of B -/ def probability : ℚ := P.ℙ.iprodb B -notation "ℙ[" B "//" P "]" => probability P B +notation "ℙ[" B "//" P "]" => probability P B /-- Conditional probability of B -/ def probability_cnd : ℚ := ℙ[ B ∧ᵣ C // P ] / ℙ[ C // P ] --- main decomposition properties -/-- If supported then can be decomposed to the immediate probability and the +/-- If supported then can be decomposed to the immediate probability and the remaining probability -/ -theorem Finprob.decompose_supp (supp : P.supported) : - ℙ[ B // P ] = (B P.ωhead).rec 0 P.phead + (1-P.phead) * ℙ[ B // P.shrink supp ] := +theorem Finprob.decompose_supp (supp : P.supported) : + ℙ[ B // P ] = (B P.ωhead).rec 0 P.phead + (1-P.phead) * ℙ[ B // P.shrink supp ] := by simp [Finprob.phead, Finprob.shrink] exact P.ℙ.decompose_supp B P.nonempty_P (P.phead_supp_ne_one supp) - + theorem Finprob.decompose_degen (degen : P.degenerate) : ℙ[ B // P ] = (B P.ωhead).rec 0 P.phead := by have tz := P.prob.degenerate_tail_zero degen simp [probability, Finprob.ωhead] - have almost := P.ℙ.iprod_first_of_tail_zero B P.nonempty_P tz + have almost := P.ℙ.iprod_first_of_tail_zero B P.nonempty_P tz rw [List.length_tail] at almost - exact almost - + exact almost + --- basic properties -theorem Finprob.in_prob (P : Finprob) : Prob ℙ[ B // P ] := +theorem Finprob.in_prob (P : Finprob) : Prob ℙ[ B // P ] := by have hip := P.phead_prob by_cases h : P.supported · rw [P.decompose_supp B h] have ih := Finprob.in_prob (P.shrink h) simp only [Prob] at ⊢ ih hip cases B P.ωhead - · simp only; - constructor; + · simp only; + constructor; . have prd_zero : 0 ≤ (1 - P.phead) * ℙ[B//P.shrink h] := Rat.mul_nonneg P.phead_prob.of_complement.1 ih.1 simp_all only [phead, probability, zero_add] · have prd_one : (1 - P.phead) * ℙ[B//P.shrink h] ≤ 1 := mul_le_one₀ P.phead_prob.of_complement.2 ih.1 ih.2 simp_all only [phead, probability, zero_add] - · simp only; - constructor; + · simp only; + constructor; · calc 0 ≤ ℙ[B//P.shrink h] := ih.1 - _ ≤ P.phead * 1 + (1 - P.phead) * ℙ[B//P.shrink h] := P.phead_prob.lower_bound_snd ih.2 + _ ≤ P.phead * 1 + (1 - P.phead) * ℙ[B//P.shrink h] := P.phead_prob.lower_bound_snd ih.2 _ = P.phead + (1 - P.phead) * ℙ[B//P.shrink h] := by ring - · calc - P.phead + (1 - P.phead) * ℙ[B//P.shrink h] = + · calc + P.phead + (1 - P.phead) * ℙ[B//P.shrink h] = P.phead * 1 + (1 - P.phead) * ℙ[B//P.shrink h] := by ring _ ≤ 1 := P.phead_prob.upper_bound_fst ih.2 · rw [P.decompose_degen B (P.degen_of_not_supp h) ] - cases B P.ωhead + cases B P.ωhead + · simp_all · simp_all - · simp_all termination_by P.length decreasing_by exact shrink_length_lt P h @@ -662,7 +663,7 @@ theorem Prob.ge_zero : ℙ[ B // P ] ≥ 0 := (P.in_prob B).left theorem Prob.le_one : ℙ[ B // P ] ≤ 1 := (P.in_prob B).right -theorem Prob.true_one : ℙ[ fun _ ↦ true // P] = 1 := +theorem Prob.true_one : ℙ[ fun _ ↦ true // P] = 1 := by simp only [probability]; rw [List.iprodb_true_sum]; exact P.prob.normalized --- sums @@ -677,19 +678,19 @@ theorem List.list_compl_sums_to_one (L : List ℚ) : L.iprodb B + L.iprodb (B.no · simp; linarith -theorem List.law_of_total_probs (L : List ℚ) : L.iprodb B = L.iprodb (B ∧ᵣ C) + L.iprodb (B ∧ᵣ (¬ᵣC) ) := - by induction L with +theorem List.law_of_total_probs (L : List ℚ) : L.iprodb B = L.iprodb (B ∧ᵣ C) + L.iprodb (B ∧ᵣ (¬ᵣC) ) := + by induction L with | nil => simp [List.iprodb] - | cons head tail => + | cons head tail => simp [List.iprodb] cases bB: B tail.length · cases bC : C tail.length; simp_all; simp_all · cases bC : C tail.length · simp_all; ring; - · simp_all; ring; + · simp_all; ring; theorem Prob.prob_compl_sums_to_one : ℙ[B // P] + ℙ[¬ᵣB // P] = 1 := - calc + calc ℙ[ B // P ] + ℙ[ ¬ᵣB // P] = P.ℙ.sum := P.ℙ.list_compl_sums_to_one B _ = 1 := P.prob.normalized @@ -697,23 +698,23 @@ theorem Prob.prob_compl_one_minus : ℙ[¬ᵣB // P] = 1 - ℙ[B // P] := by have := Prob.prob_compl_sums_to_one P B linarith - + theorem Prob.law_of_total_probs : ℙ[B // P] = ℙ[ B ∧ᵣ C // P] + ℙ[ B ∧ᵣ ¬ᵣC //P] := P.ℙ.law_of_total_probs B C ----- conditional probability +---- conditional probability notation "ℙ[" B "|" C "//" P "]" => probability_cnd P B C theorem Prob.conditional_total (h : 0 < ℙ[C // P]) : ℙ[B ∧ᵣ C // P] = ℙ[ B | C // P] * ℙ[ C // P] := - by simp [probability_cnd] at ⊢ h + by simp [probability_cnd] at ⊢ h have : P.ℙ.iprodb C * (P.ℙ.iprodb C)⁻¹ = 1 := Rat.mul_inv_cancel (P.ℙ.iprodb C) (Ne.symm (ne_of_lt h)) - calc + calc P.ℙ.iprodb (B ∧ᵣC) = P.ℙ.iprodb (B ∧ᵣC) * 1 := by ring _ = P.ℙ.iprodb (B ∧ᵣC) * (P.ℙ.iprodb C * (P.ℙ.iprodb C)⁻¹) := by rw [←this] _ = P.ℙ.iprodb (B ∧ᵣ C) / P.ℙ.iprodb C * P.ℙ.iprodb C := by ring - -theorem Prob.law_of_total_probs_cnd + +theorem Prob.law_of_total_probs_cnd (h1 : 0 < ℙ[C // P]) (h2 : ℙ[C // P] < 1) : ℙ[B // P] = ℙ[B | C // P] * ℙ[ C // P] + ℙ[B | ¬ᵣC //P] * ℙ[¬ᵣC // P] := by have h2' : 0 < ℙ[¬ᵣC // P] := by rw [prob_compl_one_minus]; linarith rw [←Prob.conditional_total P B C h1] @@ -734,7 +735,7 @@ variable (P : Finprob) (X Y Z: FinRV ℚ) (B : FinRV Bool) def expect : ℚ := P.ℙ.iprod X -notation "𝔼[" X "//" P "]" => expect P X +notation "𝔼[" X "//" P "]" => expect P X -- expectation for a joint probability space and random variable notation "𝔼[" PX "]" => expect PX.1 PX.2 @@ -769,20 +770,20 @@ may induce equivalent sample spaces. Also there is no guarantee that there will not be a generator with zero probability. -/ def Finprob.SampleMap (P : Finprob) (m : ℕ) : Type := Fin P.length → Fin m -variable {ρ : Type} {P : Finprob} {m : ℕ} +variable {ρ : Type} {P : Finprob} {m : ℕ} -instance : CoeOut (Finprob.SampleMap P m) (FinRV (Fin m)) where coe a := +instance : CoeOut (Finprob.SampleMap P m) (FinRV (Fin m)) where coe a := (fun ω ↦ if h : ω < P.length then a ⟨ω, h⟩ else a ⟨0,P.len_ge_one⟩) - -/-- Defines that the random variable X is measurable with respect to a map -and a reduced random variable Y + +/-- Defines that the random variable X is measurable with respect to a map +and a reduced random variable Y --/ def FinRV.MeasurableRV (X Y : FinRV ρ) (ℱ : P.SampleMap m) : Prop := ∀ ω : Fin P.length, X ω = Y (ℱ ω) /-- Defines the aggregated probability in the compacted space --/ -def FinProb.MeasurableProb {L : List ℚ} (ℱ : P.SampleMap L.length) : Prop := - ∀ m : Fin L.length, ℙ[ℱ =ᵣ m // P] = L.get m - +def FinProb.MeasurableProb {L : List ℚ} (ℱ : P.SampleMap L.length) : Prop := + ∀ m : Fin L.length, ℙ[ℱ =ᵣ m // P] = L.get m + --example {m : ℕ} {ℱ : P.SampleMap m} (h: X.Measurable Y ℱ) : 1 = 𝔼[ X // P ] := by sorry end Measurability From b50090caa732382b0d8db3b48c0a3569a43f7b90 Mon Sep 17 00:00:00 2001 From: Keith Badger Date: Tue, 21 Oct 2025 11:59:31 -0400 Subject: [PATCH 2/6] added comment --- blueprint/src/print.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index 19066fd..930fb30 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -9,6 +9,7 @@ % (no ugly rectangles around links). % It is otherwise a very minimal preamble (you should probably at least % add cleveref and tikz-cd). +% broke everything \documentclass[letterpaper]{article} From 7b3cb25fc667849eaa47ace48630a48a3fe0a8fb Mon Sep 17 00:00:00 2001 From: Keith Badger Date: Wed, 22 Oct 2025 22:55:44 -0400 Subject: [PATCH 3/6] Made the omega implied in indicator function --- Probability/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Probability/Basic.lean b/Probability/Basic.lean index 8888dae..9001407 100644 --- a/Probability/Basic.lean +++ b/Probability/Basic.lean @@ -27,7 +27,7 @@ def indicator (cond : Bool) : ℚ := cond.rec 0 1 abbrev 𝕀 : Bool → ℚ := indicator /-- Indicator is 0 or 1 -/ -theorem ind_zero_one (cond : τ → Bool) (ω : τ) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by +theorem ind_zero_one (cond : τ → Bool) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by by_cases h : cond ω · left; simp only [Function.comp_apply, h, indicator] · right; simp only [Function.comp_apply, h, indicator] From 961663f76f631fca6d47e157695c555b73e77bec Mon Sep 17 00:00:00 2001 From: Keith Badger Date: Thu, 23 Oct 2025 11:34:07 -0400 Subject: [PATCH 4/6] idk --- Probability/Basic.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Probability/Basic.lean b/Probability/Basic.lean index 8888dae..f92f1c7 100644 --- a/Probability/Basic.lean +++ b/Probability/Basic.lean @@ -1,4 +1,5 @@ --Please add to main pretty pretty please +--Broke everything import Mathlib.Data.Nat.Basic import Mathlib.Data.Real.Basic import Mathlib.Data.Rat.Defs From c5fe44edd45799cb8fb2a445f3c8ccd7d2853f5d Mon Sep 17 00:00:00 2001 From: Keith Badger Date: Thu, 23 Oct 2025 11:35:26 -0400 Subject: [PATCH 5/6] Fixed pull request --- Probability/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Probability/Basic.lean b/Probability/Basic.lean index fe5d456..6b9d9df 100644 --- a/Probability/Basic.lean +++ b/Probability/Basic.lean @@ -28,7 +28,7 @@ def indicator (cond : Bool) : ℚ := cond.rec 0 1 abbrev 𝕀 : Bool → ℚ := indicator /-- Indicator is 0 or 1 -/ -theorem ind_zero_one (cond : τ → Bool) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by +theorem ind_zero_on {ω} (cond : τ → Bool) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by by_cases h : cond ω · left; simp only [Function.comp_apply, h, indicator] · right; simp only [Function.comp_apply, h, indicator] From 074989a007feea6de1c0866adbc6055c6c0b4ca1 Mon Sep 17 00:00:00 2001 From: Keith Badger Date: Thu, 23 Oct 2025 11:57:50 -0400 Subject: [PATCH 6/6] refixed the fix --- Probability/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Probability/Basic.lean b/Probability/Basic.lean index 6b9d9df..5df8cad 100644 --- a/Probability/Basic.lean +++ b/Probability/Basic.lean @@ -28,7 +28,7 @@ def indicator (cond : Bool) : ℚ := cond.rec 0 1 abbrev 𝕀 : Bool → ℚ := indicator /-- Indicator is 0 or 1 -/ -theorem ind_zero_on {ω} (cond : τ → Bool) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by +theorem ind_zero_on (cond : τ → Bool) : ( (𝕀∘cond) ω = 1)∨((𝕀∘cond) ω = 0) := by by_cases h : cond ω · left; simp only [Function.comp_apply, h, indicator] · right; simp only [Function.comp_apply, h, indicator]