From 85ec9d638559d2d9c2facab457bccdac7e6481e1 Mon Sep 17 00:00:00 2001 From: Marek Petrik Date: Fri, 25 Sep 2026 15:23:47 -0400 Subject: [PATCH 1/3] cleanup --- README.md | 42 +++++++++++++----------------------------- 1 file changed, 13 insertions(+), 29 deletions(-) diff --git a/README.md b/README.md index a2f57fc..afdde39 100644 --- a/README.md +++ b/README.md @@ -26,15 +26,12 @@ instantiate at `ℝ` for the standard theory, where the definitions remain well- `VaR[X // P, α]` cannot be `#eval`'d over `ℝ`). -### Relationship to Mathlib's measure theory-based probability +### Relationship to Mathlib's probability -Mathlib's measure-theoretic probability (`Measure`, `PMF`, `∫`, `∫⁻`) is **not** used, and -cannot be: it is uniformly `noncomputable` and valued in `ℝ≥0∞` or an `ℝ`-normed space, so it -neither evaluates at `ℚ` nor says anything about a general scalar `R`. Mathlib also has no -quantiles, VaR or CVaR at all. What *is* reused is the scalar-generic algebraic API — -`Finset.centerMass`, which is weighted expectation over exactly this library's class stack, and -the order/convexity results built on it. See the audit note at the top of -[`MDPLib/Probability/Defs.lean`](MDPLib/Probability/Defs.lean) for the details and citations. +Mathlib's measure-theoretic probability (`Measure`, `PMF`, `∫`) is not used: it is +`noncomputable` and valued in `ℝ≥0∞` or `ℝ`, so it can neither be evaluated at `ℚ` nor stated +over a general `R`, and it has no quantiles or VaR. Mathlib's scalar-generic convexity API +(`Finset.centerMass`, `StdSimplex`) is reused instead. Legend: ✅ proof complete  ·  🚧 statement final, proof still depends on a `sorry` @@ -64,7 +61,7 @@ Legend: ✅ proof complete  ·  🚧 statement final, proof still depe | | Result | Lean name | |---|---|---| | ✅ | `𝔼[X // P]` is Mathlib's `Finset.centerMass` at weights summing to one | [`Findist.expect_eq_centerMass`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_eq_centerMass) | -| ✅ | `min X ≤ 𝔼[X] ≤ max X` | [`Findist.expect_ge_min`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_ge_min), [`Findist.expect_le_max`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_le_max) | +| ✅ | `minQuark X ≤ 𝔼[X] ≤ maxQuark X` | [`Findist.expect_ge_minQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_ge_minQuark), [`Findist.expect_le_maxQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_le_maxQuark) | | ✅ | Jensen's inequality for an arbitrary convex / concave function | [`Findist.expect_convexOn_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_convexOn_le), [`Findist.expect_concaveOn_ge`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_concaveOn_ge) | ### Bridge to Mathlib's standard simplex @@ -96,17 +93,7 @@ Legend: ✅ proof complete  ·  🚧 statement final, proof still depe | ✅ | Expectation equals the sum over the (finite) image of `X` | [`Findist.expect_eq_sum_probability_mul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_eq_sum_probability_mul), [`FinRV.sum_image_univ_eq_sum_fin`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.sum_image_univ_eq_sum_fin) | | ✅ | Duplicate-free list of the values of a random variable, with index/value inverses | [`FinRV.imageList`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageList), [`FinRV.imageIdxOf`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageIdxOf), [`FinRV.getElem_imageIdxOf`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.getElem_imageIdxOf), [`FinRV.imageList_nodup`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageList_nodup) | | ✅ | Invariance of probability and expectation under a permutation of the sample space | [`Findist.comp`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.comp), [`Findist.probability_comp_perm`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_comp_perm), [`Findist.expect_comp_perm`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_comp_perm) | -| 🚧 | A `≤` event can be replaced by a strict `<` event at a larger threshold | [`Findist.exists_probability_leq_eq_probability_lt_of_lt_max`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.exists_probability_leq_eq_probability_lt_of_lt_max) | - -### Probability: matrices and Markov reward processes - -[`MDPLib/Probability/Matrix.lean`](MDPLib/Probability/Matrix.lean) - -| | Result | Lean name | -|---|---|---| -| ✅ | Row-stochastic transition matrix | [`Matrix.ProbabilityMatrix`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Matrix.html#Matrix.ProbabilityMatrix) | -| ✅ | A distribution pushed through a transition matrix is again a distribution | [`Matrix.nonneg_vecMul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Matrix.html#Matrix.nonneg_vecMul), [`Matrix.vecMul_dotProduct_one`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Matrix.html#Matrix.vecMul_dotProduct_one) | -| ✅ | Discounted Markov reward process and its Bellman backup `𝔹[v // Proc] = r + γ · P v` | [`Matrix.DiscountedMRP`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Matrix.html#Matrix.DiscountedMRP), [`Matrix.bellmanBackup`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Matrix.html#Matrix.bellmanBackup) | +| ✅ | A `≤` event can be replaced by a strict `<` event at a larger threshold | [`Findist.exists_probability_leq_eq_probability_lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.exists_probability_leq_eq_probability_lt), [`Findist.exists_probability_leq_eq_probability_lt_of_lt_maxQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.exists_probability_leq_eq_probability_lt_of_lt_maxQuark) | ### Quantiles @@ -134,17 +121,14 @@ Legend: ✅ proof complete  ·  🚧 statement final, proof still depe | ✅ | Characterization `IsVaR v ↔ ℙ[X < v] ≤ α < ℙ[X ≤ v]` | [`Risk.isVaR_iff`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaR_iff) | | ✅ | Computable VaR `VaR[X // P, α]` as a max over the finite candidate set, which is nonempty | [`Risk.finVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR), [`Risk.finVaRSet`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaRSet), [`Risk.finVaRSet_nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaRSet_nonempty) | | ✅ | VaR is monotone: `X ≤ Y` implies `VaR[X] ≤ VaR[Y]` | [`Risk.IsVaR.le_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.le_of_le) | -| 🚧 | **Correctness of the computable VaR:** `IsVaR P X α (VaR[X // P, α])` | [`Risk.isVaR_finVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaR_finVaR) | -| 🚧 | The two definitions (greatest quantile / greatest lower quantile) agree | [`Risk.isVaRQuantile_iff_isVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaRQuantile_iff_isVaR) | -| 🚧 | The quantile set is nonempty | [`Risk.quantile_nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.quantile_nonempty) | +| ✅ | **Correctness of the computable VaR:** `IsVaR P X α (VaR[X // P, α])` | [`Risk.isVaR_finVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaR_finVaR) | +| ✅ | The two definitions (greatest quantile / greatest lower quantile) agree | [`Risk.isVaRQuantile_iff_isVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaRQuantile_iff_isVaR) | +| ✅ | The quantile set is nonempty | [`Risk.quantile_nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.quantile_nonempty) | | ✅ | Translation (cash) invariance for the `Risk.IsVaR` predicate | [`Risk.IsVaR.add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.add_const) | -| 🚧 | … and for the computable VaR: `VaR[X + c] = VaR[X] + c` | [`Risk.finVaR_add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_add_const) | +| ✅ | … and for the computable VaR: `VaR[X + c] = VaR[X] + c` | [`Risk.finVaR_add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_add_const) | | ✅ | Strictly monotone transformations for the `Risk.IsVaR` predicate | [`Risk.IsVaR.comp_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.comp_of_strictMono) | -| 🚧 | … and for the computable VaR: `VaR[f∘X] = f(VaR[X])` | [`Risk.finVaR_comp_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_comp_of_strictMono) | -| 🚧 | Positive homogeneity: `VaR[c·X] = c·VaR[X]` for `c > 0` | [`Risk.finVaR_const_mul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_const_mul) | - -The 🚧 entries above are all complete modulo the single missing lemma -`Findist.exists_probability_leq_eq_probability_lt_of_lt_max`. +| ✅ | … and for the computable VaR: `VaR[f∘X] = f(VaR[X])` | [`Risk.finVaR_comp_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_comp_of_strictMono) | +| ✅ | Positive homogeneity: `VaR[c·X] = c·VaR[X]` for `c > 0` | [`Risk.finVaR_const_mul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_const_mul) | [`Main.lean`](Main.lean) contains an executable that reads distributions from a JSON file, computes VaR with `computeVaR`, and checks it against reference values From cbecefc024eb534c53fc60d96142c5a6a45ee9bb Mon Sep 17 00:00:00 2001 From: Marek Petrik Date: Tue, 6 Oct 2026 10:22:50 -0400 Subject: [PATCH 2/3] updated boolean algebra --- MDPLib/Probability/Basic.lean | 76 +++++++++++++------------------- MDPLib/Probability/Defs.lean | 32 +++++--------- MDPLib/Probability/Quantile.lean | 44 ++++++++---------- MDPLib/Risk/VaR.lean | 6 +-- README.md | 2 +- 5 files changed, 66 insertions(+), 94 deletions(-) diff --git a/MDPLib/Probability/Basic.lean b/MDPLib/Probability/Basic.lean index 06afe88..b74369a 100644 --- a/MDPLib/Probability/Basic.lean +++ b/MDPLib/Probability/Basic.lean @@ -54,9 +54,7 @@ theorem probability_nonneg : 0 ≤ ℙ[B // P] := theorem probability_le_one : ℙ[B // P] ≤ 1 := - by rw [probability_eq_expect_indicator] - calc 𝔼[𝕀 ∘ B//P] ≤ 𝔼[1 // P] := expect_mono indicator_le_one - _ = 1 := expect_const + by grw [probability_eq_expect_indicator, expect_mono indicator_le_one, expect_one] theorem isProb_probability (P : Findist R Ω) : IsProb ℙ[B // P] := ⟨probability_nonneg, probability_le_one⟩ @@ -309,12 +307,13 @@ theorem probability_add_probability_not : ℙ[B // P] + ℙ[¬ᵣB // P] = 1 := theorem probability_not : ℙ[¬ᵣB // P] = 1 - ℙ[B // P] := by rw [←probability_add_probability_not (P:=P) (B:=B)]; ring -@[to_dual geq_add_lt] -theorem _root_.FinRV.leq_add_gt : (X ≤ᵣ t) + (X >ᵣ t) = 1 := by +@[to_dual geq_sup_lt] +theorem _root_.FinRV.leq_sup_gt : (X ≤ᵣ t) ⊔ (X >ᵣ t) = 1 := by ext ω; simpa [FinRV.leq, FinRV.gt] using le_or_gt (X ω) t -theorem probability_leq_add_probability_gt : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P] = 1 := by - rw [probability_eq_expect_indicator, probability_eq_expect_indicator, ← expect_add] +@[to_dual probability_ge_lt_one] +theorem probability_le_gt_one : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P] = 1 := by + rw [probability_eq_expect_indicator, probability_eq_expect_indicator, ←expect_add] have h : (𝕀 ∘ (X ≤ᵣ t)) + (𝕀 ∘ (X >ᵣ t)) = (1 : FinRV Ω R) := by ext ω unfold FinRV.leq FinRV.gt @@ -327,37 +326,26 @@ theorem probability_leq_add_probability_gt : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t rw [h] exact expect_one +theorem probability_lt_ge_one : ℙ[X <ᵣ t // P] + ℙ[X ≥ᵣ t // P] = 1 := + (add_comm _ _).trans probability_ge_lt_one + theorem probability_gt_eq_one_sub : ℙ[X >ᵣ t // P] = 1 - ℙ[X ≤ᵣ t // P] := by - rw [←probability_leq_add_probability_gt (P := P) (X := X) (t := t)] + rw [←probability_le_gt_one (P := P) (X := X) (t := t)] ring -theorem probability_leq_eq_one_sub : ℙ[X ≤ᵣ t // P] = 1 - ℙ[X >ᵣ t // P] := by - rw [←probability_leq_add_probability_gt (P := P) (X := X) (t := t)] +theorem probability_le_eq_one_sub : ℙ[X ≤ᵣ t // P] = 1 - ℙ[X >ᵣ t // P] := by + rw [←probability_le_gt_one (P := P) (X := X) (t := t)] ring -theorem probability_lt_add_probability_geq : ℙ[X <ᵣ t // P] + ℙ[X ≥ᵣ t // P] = 1 := by - rw [probability_eq_expect_indicator, probability_eq_expect_indicator, ← expect_add] - have h : (𝕀 ∘ (X <ᵣ t)) + (𝕀 ∘ (X ≥ᵣ t)) = (1 : FinRV Ω R) := by - ext ω - unfold FinRV.lt FinRV.geq - simp [𝕀, indicator] - by_cases h1 : X ω < t - · have h2 : ¬ (X ω ≥ t) := not_le_of_gt h1 - simp [h1, h2] - · have h3 : X ω ≥ t := le_of_not_gt h1 - simp [h1, h3] - rw [h] - exact expect_one - -theorem probability_geq_eq_one_sub : ℙ[X ≥ᵣ t // P] = 1 - ℙ[X <ᵣ t // P] := by - rw [← probability_lt_add_probability_geq (P := P) (X := X) (t := t)]; ring +theorem probability_ge_eq_one_sub : ℙ[X ≥ᵣ t // P] = 1 - ℙ[X <ᵣ t // P] := by + rw [← probability_lt_ge_one (P := P) (X := X) (t := t)]; ring theorem probability_lt_eq_one_sub : ℙ[X <ᵣ t // P] = 1 - ℙ[X ≥ᵣ t // P] := by - rw [← probability_lt_add_probability_geq (P := P) (X := X) (t := t)]; ring + rw [← probability_lt_ge_one (P := P) (X := X) (t := t)]; ring theorem probability_mono : A ≤ B → ℙ[A // P] ≤ ℙ[B // P] := fun h => expect_mono (indicator_mono h) -theorem probability_leq_mono : X ≤ Y → t₁ ≤ t₂ → ℙ[Y ≤ᵣ t₁ // P] ≤ ℙ[X ≤ᵣ t₂ // P] := by +theorem probability_le_mono : X ≤ Y → t₁ ≤ t₂ → ℙ[Y ≤ᵣ t₁ // P] ≤ ℙ[X ≤ᵣ t₂ // P] := by intro hxy ht exact expect_mono (indicator_leq_mono hxy ht) @@ -365,16 +353,16 @@ theorem probability_lt_mono : X ≤ Y → t₁ ≤ t₂ → ℙ[Y <ᵣ t₁ // P intro hxy ht exact expect_mono (indicator_lt_mono hxy ht) -theorem probability_geq_anti : X ≤ Y → t₁ ≤ t₂ → ℙ[Y ≥ᵣ t₁ // P] ≥ ℙ[X ≥ᵣ t₂ // P] := by +theorem probability_ge_anti : X ≤ Y → t₁ ≤ t₂ → ℙ[Y ≥ᵣ t₁ // P] ≥ ℙ[X ≥ᵣ t₂ // P] := by intro hxy ht - rewrite [probability_geq_eq_one_sub,probability_geq_eq_one_sub] + rewrite [probability_ge_eq_one_sub,probability_ge_eq_one_sub] have := probability_lt_mono (P := P) hxy ht linarith theorem probability_gt_anti : X ≤ Y → t₁ ≤ t₂ → ℙ[Y >ᵣ t₁ // P] ≥ ℙ[X >ᵣ t₂ // P] := by intro hxy ht rewrite [probability_gt_eq_one_sub,probability_gt_eq_one_sub] - have := probability_leq_mono (P := P) hxy ht + have := probability_le_mono (P := P) hxy ht linarith theorem probability_leq_le_probability_lt {q : R} (h : q > t) : ℙ[X <ᵣ q // P] ≥ ℙ[X ≤ᵣ t // P] := by @@ -397,7 +385,7 @@ theorem probability_lt_minQuark : ℙ[X <ᵣ X.minQuark // P] = 0 := by theorem lt_maxQuark_of_probability_leq_lt_one {t : R} (h : ℙ[X ≤ᵣ t // P] < 1) : t < X.maxQuark := by by_contra! hcontra - have h1 := probability_leq_mono (P := P) (le_refl X) hcontra + have h1 := probability_le_mono (P := P) (le_refl X) hcontra rw [probability_leq_maxQuark] at h1 exact not_le_of_gt h h1 @@ -432,28 +420,26 @@ open Function variable {f : R → R} {x : R} --- LE - -theorem _root_.Monotone.probability_leq_le (hm : Monotone f) : ℙ[X ≤ᵣ x // P] ≤ ℙ[f ∘ X ≤ᵣ f x // P] := +theorem _root_.Monotone.probability_le (hm : Monotone f) : ℙ[X ≤ᵣ x // P] ≤ ℙ[f ∘ X ≤ᵣ f x // P] := probability_mono (leq_le_comp_leq_of_monotone hm) -theorem _root_.StrictMono.probability_leq_eq (hm : StrictMono f) : ℙ[X ≤ᵣ x // P] = ℙ[f ∘ X ≤ᵣ f x // P] := +theorem _root_.StrictMono.probability_le (hm : StrictMono f) : ℙ[X ≤ᵣ x // P] = ℙ[f ∘ X ≤ᵣ f x // P] := probability_congr (leq_eq_comp_leq_of_strictMono hm) ---- LT - -theorem _root_.StrictMono.probability_lt_eq (hm : StrictMono f) : ℙ[X <ᵣ x // P] = ℙ[f ∘ X <ᵣ f x // P] := + +--- LT: no equivalent of leq for Monotonicity +theorem _root_.StrictMono.probability_lt (hm : StrictMono f) : ℙ[X <ᵣ x // P] = ℙ[f ∘ X <ᵣ f x // P] := probability_congr (lt_eq_comp_lt_of_strictMono hm) --- GE - -theorem _root_.Monotone.probability_geq_le (hm : Monotone f) : ℙ[X ≥ᵣ x // P] ≤ ℙ[f ∘ X ≥ᵣ f x // P] := +theorem _root_.Monotone.probability_geq (hm : Monotone f) : ℙ[X ≥ᵣ x // P] ≤ ℙ[f ∘ X ≥ᵣ f x // P] := probability_mono (geq_le_comp_geq_of_monotone hm) -theorem _root_.StrictMono.probability_geq_eq (hm : StrictMono f) : ℙ[X ≥ᵣ x // P] = ℙ[f ∘ X ≥ᵣ f x // P] := +theorem _root_.StrictMono.probability_ge (hm : StrictMono f) : ℙ[X ≥ᵣ x // P] = ℙ[f ∘ X ≥ᵣ f x // P] := probability_congr (geq_eq_comp_geq_of_strictMono hm) --- GT -theorem _root_.StrictMono.probability_gt_eq (hm : StrictMono f) : ℙ[X >ᵣ x // P] = ℙ[f ∘ X >ᵣ f x // P] := +theorem _root_.StrictMono.probability_gt (hm : StrictMono f) : ℙ[X >ᵣ x // P] = ℙ[f ∘ X >ᵣ f x // P] := probability_congr (gt_eq_comp_gt_of_strictMono hm) end Monotone @@ -503,12 +489,12 @@ variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} {X Y : FinRV /-- shows CDF is non-decreasing -/ theorem cdf_mono : t₁ ≤ t₂ → cdf P X t₁ ≤ cdf P X t₂ := by intro ht; unfold cdf - apply probability_leq_mono (le_refl X) ht + apply probability_le_mono (le_refl X) ht /-- Shows CDF is monotone in random variable -/ theorem cdf_anti_of_le : X ≤ Y → cdf P X t ≥ cdf P Y t := by intro h; unfold cdf - apply probability_leq_mono h (le_refl t) + apply probability_le_mono h (le_refl t) end Findist @@ -636,7 +622,7 @@ variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {k : ℕ} {L : FinRV Ω (Fin k) variable {P : Findist R Ω} {B : FinRV Ω Bool} /-- The law of total probabilities -/ -theorem probability_eq_sum : ℙ[B // P] = ∑ i, ℙ[B * (L =ᵣ i) // P] := by +theorem probability_eq_sum : ℙ[B // P] = ∑ i, ℙ[B ⊓ (L =ᵣ i) // P] := by rewrite [probability_eq_expect_indicator, eq_sum_mul_indicatorEq (𝕀∘B : FinRV Ω R) L, expect_sum] apply Fintype.sum_congr intro i diff --git a/MDPLib/Probability/Defs.lean b/MDPLib/Probability/Defs.lean index 2c598b2..7d9ba39 100644 --- a/MDPLib/Probability/Defs.lean +++ b/MDPLib/Probability/Defs.lean @@ -6,6 +6,7 @@ import Mathlib.Algebra.Notation.Pi.Defs -- operations on functions import Mathlib.Algebra.Module.PointwisePi -- for smul_pi import Mathlib.LinearAlgebra.Matrix.DotProduct -- for monotonicity import Mathlib.Data.Finset.Image -- for Finset.universal.image +import Mathlib.Algebra.Ring.BooleanRing -- `0`, `1` on Bool set_option linter.unusedSectionVars false @@ -87,20 +88,15 @@ variable {Ω : Type} [Nonempty Ω] {ρ : Type} namespace FinRV --- WARNING: these four instances shadow Mathlib's global `Bool` algebra. --- in `Mathlib/Algebra/Ring/BooleanRing.lean. These operations are defined differntly -instance instMulBool : Mul Bool where mul a b := Bool.and a b -instance instAddBool: Add Bool where add a b := Bool.or a b -instance instZeroBool : Zero Bool where zero := false -instance instOneBool : One Bool where one := true - +-- Boolean random variables use Mathlib's lattice operations: `B ⊔ C` is the union (`or`), +-- `B ⊓ C` the intersection (`and`), and `¬ᵣ B` the complement. `0`/`1` are `false`/`true` +-- from Mathlib's `BooleanRing Bool`; do not use its `+`, which is `xor`. variable {A B : Bool} - @[simp] theorem one_eq_true : (1:Bool) = true := rfl @[simp] theorem zero_eq_false : (0:Bool) = false := rfl -@[simp] theorem add_eq_or : A + B = Bool.or A B := rfl -@[simp] theorem mul_eq_and : A * B = Bool.and A B := rfl +@[simp] theorem sup_eq_or : A ⊔ B = (A || B) := rfl +@[simp] theorem inf_eq_and : A ⊓ B = (A && B) := rfl -- NOTE: the following definitions of inequalities and operations @@ -163,14 +159,10 @@ infix:50 ">ᵣ" => FinRV.gt -- coe a := a /-- Equivalence when adding an element to integer comparison. -/ -theorem leq_add_eq_succ (D : FinRV Ω ℕ) (m : ℕ) : ((D ≤ᵣ m) + (D =ᵣ m.succ)) = (D ≤ᵣ m.succ) := by - have exclusion {a b : ℕ} (h : a > b + 1) : (a > b) ∧ ¬(a = b + 1) := - ⟨ Nat.lt_of_succ_lt h, Ne.symm (Nat.ne_of_lt h) ⟩ - funext x - rw [FinRV.leq, instHAdd, Add.add, Pi.instAdd, Pi.add_apply, add_eq_or] - by_cases h : D x ≤ m.succ - · simp [h, Nat.le_or_eq_of_le_succ] - · simp [h, exclusion (Nat.not_le.mp h)] +theorem leq_sup_eq_succ (D : FinRV Ω ℕ) (m : ℕ) : ((D ≤ᵣ m) ⊔ (D =ᵣ m.succ)) = (D ≤ᵣ m.succ) := by + funext x + simp only [Pi.sup_apply, FinRV.leq, FinRV.eq, sup_eq_or] + by_cases h₁ : D x ≤ m <;> by_cases h₂ : D x = m + 1 <;> simp [h₁, h₂] <;> omega /-- Defines a preimage of an RV. This is a set with a decidable membership. -/ def preimage (f : FinRV Ω ρ) : ρ → Set Ω := @@ -224,7 +216,7 @@ theorem eq_sum_mul_indicatorEq (X : FinRV Ω R) (L : FinRV Ω (Fin k)) : X = ∑ omit [Nonempty Ω] in theorem indicator_one : 𝕀 ∘ (1 : Ω → Bool) = (1 : Ω → R) := by ext; simp [𝕀, indicator] -theorem add_not_eq_one : B + (¬ᵣ B) = (1 : FinRV Ω Bool) := by ext ω; unfold FinRV.not; simp +theorem sup_not_eq_one : B ⊔ (¬ᵣ B) = (1 : FinRV Ω Bool) := by ext ω; unfold FinRV.not; simp theorem indicator_add_indicator_not_eq_one : (𝕀∘B) + (𝕀∘(¬ᵣ B)) = (1 : FinRV Ω R) := by ext ω; unfold FinRV.not 𝕀 indicator Bool.not @@ -277,7 +269,7 @@ def probability : R := P.p ⬝ᵥ (𝕀 ∘ B) notation "ℙ[" B "//" P "]" => probability P B /-- Conditional probability of B on C -/ -def probabilityCond : R := ℙ[B * C // P] / ℙ[ C // P ] +def probabilityCond : R := ℙ[B ⊓ C // P] / ℙ[ C // P ] /-- Conditional probability of B on C -/ notation "ℙ[" B "|" C "//" P "]" => probabilityCond P B C diff --git a/MDPLib/Probability/Quantile.lean b/MDPLib/Probability/Quantile.lean index 5a5106b..3418f35 100644 --- a/MDPLib/Probability/Quantile.lean +++ b/MDPLib/Probability/Quantile.lean @@ -8,9 +8,6 @@ variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [CharZero R] [Archimedean R] - - - -- TODO(naming): Mathlib states order lemmas in the `≤` / `<` direction and derives the `≥` -- / `>` forms via `ge_iff_le`. Most statements in this file (`IsQuantile`, `probability_geq_of_mem_quantile`, -- `mem_quantileLower_iff`, ...) are written with `≥`, which keeps them from matching Mathlib's @@ -66,28 +63,25 @@ theorem mem_quantileLower_iff_probability_lt : q ∈ quantileLower P X α ↔ suffices ℙ[X≥ᵣq // P] ≥ 1-α from this linarith -theorem probability_lt_of_mem_quantile : q ∈ quantile P X α → ℙ[ X <ᵣ q // P] ≤ α := - by intro h - have := probability_geq_of_mem_quantile h - rewrite [probability_geq_eq_one_sub] at this +theorem probability_lt_of_mem_quantile (h : q ∈ quantile P X α) : ℙ[ X <ᵣ q // P] ≤ α := + by have h1 := probability_geq_of_mem_quantile h + rewrite [probability_ge_eq_one_sub] at h1 linarith -- TODO(mathlib): this is `mem_quantile_iff.mpr`; consider dropping it. -theorem mem_quantile_of_probability_geq : ℙ[ X ≤ᵣ q // P ] ≥ α ∧ ℙ[ X ≥ᵣ q // P] ≥ 1 - α → q ∈ quantile P X α := - by intro h; simp_all [quantile, IsQuantile] +theorem mem_quantile_of_probability_geq (h1 : ℙ[X ≤ᵣ q // P] ≥ α) (h2 : ℙ[X ≥ᵣ q // P] ≥ 1 - α) : q ∈ quantile P X α := + by simp_all [quantile, IsQuantile] -theorem mem_quantile_of_probability_lt : ℙ[X ≤ᵣ q // P] ≥ α ∧ ℙ[ X <ᵣ q // P] ≤ α → q ∈ quantile P X α := - by intro h1 - have h2 : ℙ[ X ≥ᵣ q // P] ≥ 1 - α := by rw [probability_geq_eq_one_sub]; linarith - exact mem_quantile_of_probability_geq ⟨h1.1, h2⟩ +theorem mem_quantile_of_probability_lt (h1 : ℙ[X ≤ᵣ q // P] ≥ α) (h2 : ℙ[X <ᵣ q // P] ≤ α) : q ∈ quantile P X α := + by have h3 : ℙ[ X ≥ᵣ q // P] ≥ 1 - α := by rw [probability_ge_eq_one_sub]; linarith + exact mem_quantile_of_probability_geq h1 h3 -- TODO(mathlib): this is `mem_quantileLower_iff.mpr`; consider dropping it. -theorem mem_quantileLower_of_probability_geq : ℙ[ X ≥ᵣ q // P] ≥ 1 - α → q ∈ quantileLower P X α := - by intro h; simp_all [quantileLower, IsQuantileLower] +theorem mem_quantileLower_of_probability_geq (h : ℙ[ X ≥ᵣ q // P] ≥ 1 - α) : q ∈ quantileLower P X α := + by simp_all [quantileLower, IsQuantileLower] -theorem mem_quantileLower_of_probability_lt : ℙ[ X <ᵣ q // P] ≤ α → q ∈ quantileLower P X α := - by intro h1 - have h2 : ℙ[X ≥ᵣ q // P] ≥ 1 - α := by rw [probability_geq_eq_one_sub]; linarith +theorem mem_quantileLower_of_probability_lt (h1 : ℙ[ X <ᵣ q // P] ≤ α) : q ∈ quantileLower P X α := + by have h2 : ℙ[X ≥ᵣ q // P] ≥ 1 - α := by rw [probability_ge_eq_one_sub]; linarith exact mem_quantileLower_of_probability_geq h2 theorem IsQuantile.isQuantileLower : IsQuantile P X α v → IsQuantileLower P X α v := @@ -95,10 +89,10 @@ theorem IsQuantile.isQuantileLower : IsQuantile P X α v → IsQuantileLower P X theorem quantile_subset_quantileLower : quantile P X α ⊆ quantileLower P X α := fun _ => IsQuantile.isQuantileLower -theorem isCofinalFor_quantileLower_of_le : X ≤ Y → IsCofinalFor (quantileLower P X α) (IsQuantileLower P Y α) := by - intro hle q₁ hvar₁ +theorem isCofinalFor_quantileLower_of_le (hle : X ≤ Y) : IsCofinalFor (quantileLower P X α) (IsQuantileLower P Y α) := by + intro q₁ hvar₁ have hq₁ := le_refl q₁ - exact ⟨q₁, ⟨le_trans hvar₁ (probability_geq_anti hle hq₁), hq₁⟩⟩ + exact ⟨q₁, hvar₁.trans (probability_ge_anti hle hq₁), hq₁⟩ section Negation @@ -132,16 +126,16 @@ variable {f : R → R} -- the reverse implications of the following results do not hold theorem mem_quantile_comp_of_monotone (hm : Monotone f) : q ∈ quantile P X α → (f q) ∈ quantile P (f ∘ X) α := by - intro h; grw [mem_quantile_iff, hm.probability_leq_le, hm.probability_geq_le] at h; exact h + intro h; grw [mem_quantile_iff, hm.probability_le, hm.probability_geq] at h; exact h theorem mem_quantile_comp_iff_of_strictMono (hm : StrictMono f) : q ∈ quantile P X α ↔ (f q) ∈ quantile P (f ∘ X) α := by - rw [mem_quantile_iff, mem_quantile_iff, hm.probability_leq_eq, hm.probability_geq_eq] + rw [mem_quantile_iff, mem_quantile_iff, hm.probability_le, hm.probability_ge] theorem mem_quantileLower_comp_of_monotone (hm : Monotone f) : q ∈ quantileLower P X α → (f q) ∈ quantileLower P (f ∘ X) α := by - intro h; grw [mem_quantileLower_iff, hm.probability_geq_le] at h; exact h + intro h; grw [mem_quantileLower_iff, hm.probability_geq] at h; exact h theorem mem_quantileLower_comp_iff_of_strictMono (hm : StrictMono f) : q ∈ quantileLower P X α ↔ (f q) ∈ quantileLower P (f ∘ X) α := by - rw [mem_quantileLower_iff, mem_quantileLower_iff, hm.probability_geq_eq] + rw [mem_quantileLower_iff, mem_quantileLower_iff, hm.probability_ge] -- set transformations theorem image_quantile_subset_quantile_comp_of_monotone (hm : Monotone f) : f '' quantile P X α ⊆ quantile P (f∘X) α := by diff --git a/MDPLib/Risk/VaR.lean b/MDPLib/Risk/VaR.lean index bfc7cbe..43bbd07 100644 --- a/MDPLib/Risk/VaR.lean +++ b/MDPLib/Risk/VaR.lean @@ -79,7 +79,7 @@ theorem isVaR_iff : IsVaR P X α v ↔ (ℙ[X <ᵣ v // P] ≤ α.val ∧ α.val · intro h constructor · have h1 : 1 - ℙ[X<ᵣv//P] ≥ 1 - α.val := by - simp_all [IsVaR,IsGreatest,quantileLower,IsQuantileLower,probability_geq_eq_one_sub] + simp_all [IsVaR,IsGreatest,quantileLower,IsQuantileLower,probability_ge_eq_one_sub] linarith · by_contra! hc obtain ⟨q,hq⟩ := exists_probability_leq_eq_probability_lt P X v @@ -134,7 +134,7 @@ theorem isCofinalFor_quantileLower_quantile : IsCofinalFor (quantileLower P X α constructor · exact hq₂ · by_contra! ine - exact ge_trans (probability_leq_mono (le_refl X) (le_of_lt ine)) (le_probability_leq_of_mem_quantile hq₂) |> not_le_of_gt h2l + exact ge_trans (probability_le_mono (le_refl X) (le_of_lt ine)) (le_probability_leq_of_mem_quantile hq₂) |> not_le_of_gt h2l · exfalso; exact not_le_of_gt h2r h theorem isCofinalFor_quantile_quantileLower : IsCofinalFor (quantile P X α.val) (quantileLower P X α.val) := @@ -174,7 +174,7 @@ theorem finVaR_add_const : VaR[X + c•1 // P, α] = VaR[X // P, α] + c := by theorem IsVaR.comp_of_strictMono (hm : StrictMono f) (hv : IsVaR P X α v) : IsVaR P (f ∘ X) α (f v) := by rw [isVaR_iff] rw [isVaR_iff] at hv - rw [← hm.probability_lt_eq, ← hm.probability_leq_eq] + rw [← hm.probability_lt, ← hm.probability_le] exact hv diff --git a/README.md b/README.md index afdde39..4c7c7f1 100644 --- a/README.md +++ b/README.md @@ -46,7 +46,7 @@ Legend: ✅ proof complete  ·  🚧 statement final, proof still depe |---|---|---| | ✅ | Finite distribution on `Ω` (nonneg weights summing to one), Dirac distribution | [`Findist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist), [`Findist.Δ`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.Δ), [`Findist.dirac`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.dirac) | | ✅ | A distribution forces its sample space to be nonempty | [`Findist.nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.nonempty) | -| ✅ | Random variables as bare functions `Ω → ρ`; events as `Ω → Bool` with a Boolean semiring structure | [`FinRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV), [`FinRV.instMulBool`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.instMulBool), [`FinRV.instAddBool`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.instAddBool) | +| ✅ | Random variables as bare functions `Ω → ρ`; events as `Ω → Bool` with Mathlib's Boolean algebra (`⊔`, `⊓`) | [`FinRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV), [`FinRV.sup_eq_or`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.sup_eq_or), [`FinRV.inf_eq_and`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.inf_eq_and) | | ✅ | Comparison events `X ≤ᵣ t`, `X <ᵣ t`, `X ≥ᵣ t`, `X >ᵣ t`, `X =ᵣ y` and the indicator `𝕀` | [`FinRV.leq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.leq), [`FinRV.lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.lt), [`FinRV.geq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.geq), [`FinRV.gt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.gt), [`FinRV.eq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.eq), [`FinRV.indicator`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.indicator) | | ✅ | Probability `ℙ[B // P]`, conditional probability `ℙ[B \| C // P]` | [`Findist.probability`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.probability), [`Findist.probabilityCond`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.probabilityCond) | | ✅ | Expectation `𝔼[X // P]`, conditional expectation `𝔼[X \| B // P]` and the conditional-expectation random variable `𝔼[X \|ᵣ L // P]` | [`Findist.expect`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect), [`Findist.expectCond`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expectCond), [`Findist.expectCondRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expectCondRV) | From 8c9167d4b021338dd37a0c496fca35f952a62738 Mon Sep 17 00:00:00 2001 From: Marek Petrik Date: Mon, 12 Oct 2026 15:42:05 -0400 Subject: [PATCH 3/3] refactored to use two data type: one for random variables, another one for provavilities in order to make to_dual work correctly --- MDPLib/MDP/Histories.lean | 50 ++++---- MDPLib/Probability/Basic.lean | 129 ++++++++++--------- MDPLib/Probability/Defs.lean | 141 ++++++++++---------- MDPLib/Probability/Prelude.lean | 32 ++--- MDPLib/Probability/Quantile.lean | 48 +++++-- MDPLib/Risk/CVaR.lean | 2 +- MDPLib/Risk/VaR.lean | 74 ++++++----- README.md | 212 ++++++++++++++----------------- 8 files changed, 363 insertions(+), 325 deletions(-) diff --git a/MDPLib/MDP/Histories.lean b/MDPLib/MDP/Histories.lean index fd1b2e0..a17c1e6 100644 --- a/MDPLib/MDP/Histories.lean +++ b/MDPLib/MDP/Histories.lean @@ -18,8 +18,8 @@ import MDPLib.Probability.Basic set_option linter.unusedSectionVars false -variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R] - [CharZero R] [Archimedean R] +variable {W : Type} [Field W] [LinearOrder W] [IsStrictOrderedRing W] + [CharZero W] [Archimedean W] @@ -28,7 +28,7 @@ section Definitions open Findist /-- Markov decision process -/ -structure MDP (R : Type) [Field R] [LinearOrder R] [IsStrictOrderedRing R] : Type where +structure MDP (W : Type) [Field W] [LinearOrder W] [IsStrictOrderedRing W] : Type where /-- states -/ S : ℕ S_pos : 0 < S @@ -36,11 +36,11 @@ structure MDP (R : Type) [Field R] [LinearOrder R] [IsStrictOrderedRing R] : Typ A : ℕ A_pos : 0 < A /-- transition probability s, a, s' -/ - P : Fin S → Fin A → Δ R (Fin S) + P : Fin S → Fin A → Δ W (Fin S) /-- reward function s, a, s' -/ - r : Fin S → Fin A → Fin S → R + r : Fin S → Fin A → Fin S → W -variable (M : MDP R) +variable (M : MDP W) def MDP.maxS : Fin M.S := ⟨M.S-1, by simp [M.S_pos]⟩ def MDP.maxA : Fin M.A := ⟨M.A-1, by simp [M.A_pos]⟩ @@ -67,14 +67,14 @@ theorem MDP.numStateActions_pos : 0 < M.numStateActions := Nat.mul_pos M.S_pos M end Definitions -variable {M : MDP R} +variable {M : MDP W} section Histories /-- Represents a history. The state is type ℕ and action is type ℕ. -/ -- NOTE(mathlib): `Hist M` is INFINITE -- histories have unbounded length, and there is no -- `Fintype`/`FinEnum` instance for it (only `MDP.HistOfLength M t`, the length-`t` slice, has one; --- see the `Fintype (M.HistOfLength t)` instance below). Consequently `Δ R (Hist M)` is currently +-- see the `Fintype (M.HistOfLength t)` instance below). Consequently `Δ W (Hist M)` is currently -- inexpressible: `Findist` requires `[FinEnum Ω]`. -- -- That matters for the roadmap. Randomized history-dependent policies `Π_HR` and the @@ -92,7 +92,7 @@ section Histories -- (b) Mathlib's `Finsupp`, accepting noncomputability for history distributions only. -- (c) keep indexing by `MDP.HistOfLength M t`, which is finite for each `t`, and never form a -- distribution over all of `Hist M`. -inductive Hist (M : MDP R) : Type where +inductive Hist (M : MDP W) : Type where | init : Fin M.S → Hist M | foll : Hist M → Fin M.A → Fin M.S → Hist M @@ -105,12 +105,12 @@ def Hist.length : Hist M → ℕ | init _ => 0 | Hist.foll h _ _ => 1 + length h -def MDP.HistOfLength (M : MDP R) (t : ℕ) := {h : Hist M // h.length = t} +def MDP.HistOfLength (M : MDP W) (t : ℕ) := {h : Hist M // h.length = t} -- TODO: We should prove that HistOfLength is a Fintype in order to be able to perform operations on it /-- Nonempty histories -/ -abbrev HistNonempty (M : MDP R) := {m : Hist M // m.length ≥ 1} +abbrev HistNonempty (M : MDP W) := {m : Hist M // m.length ≥ 1} /-- Returns the last state of the history -/ def Hist.last : Hist M → Fin M.S @@ -119,7 +119,7 @@ def Hist.last : Hist M → Fin M.S /-- Number of histories of length t. -/ @[simp] -def MDP.numHist (M : MDP R) (t : ℕ) : ℕ := M.S * M.numStateActions^t +def MDP.numHist (M : MDP W) (t : ℕ) : ℕ := M.S * M.numStateActions^t theorem numHist_zero : M.numHist 0 = M.S := by simp [MDP.numHist] @@ -127,7 +127,7 @@ theorem numHist_zero : M.numHist 0 = M.S := by simp [MDP.numHist] section ExplicitHistIndex /-- Construct i-th history of length t -/ -def MDP.idxToHist (M : MDP R) (t : ℕ) (i : Fin (M.numHist t)) : M.HistOfLength t := +def MDP.idxToHist (M : MDP W) (t : ℕ) (i : Fin (M.numHist t)) : M.HistOfLength t := match t with | Nat.zero => let ii : Fin M.S := ⟨i.1, by have h := i.2; simp_all [MDP.numHist] ⟩ @@ -164,7 +164,7 @@ lemma MDPLib.Nat.sub_one_mul_add_self (n : ℕ) {m : ℕ} (h : 0 < m) : (m-1) * exact Nat.le_mul_of_pos_left n h /-- Compute the index of a history -/ -def MDP.histToIdx (M : MDP R) (h : Hist M) : Fin (M.numHist h.length) := +def MDP.histToIdx (M : MDP W) (h : Hist M) : Fin (M.numHist h.length) := match h with | Hist.init s => ⟨s, by simp only [numHist, Hist.length, pow_zero, mul_one, Fin.is_lt]⟩ | Hist.foll h' a s => @@ -211,23 +211,23 @@ open Function /-- A more convenient definition for constructing inverses -/ -def MDP.histToIdx' (M : MDP R) (t : ℕ) (h : HistOfLength M t) : Fin (M.numHist t) := +def MDP.histToIdx' (M : MDP W) (t : ℕ) (h : HistOfLength M t) : Fin (M.numHist t) := h.property ▸ M.histToIdx h.val /-- A more convenient definition for constructing inverses -/ -def MDP.idxToHist' (M : MDP R) (t : ℕ) (i : Fin (M.numHist t)) : HistOfLength M t := +def MDP.idxToHist' (M : MDP W) (t : ℕ) (i : Fin (M.numHist t)) : HistOfLength M t := M.idxToHist t i -def MDP.histIdxValid (M : MDP R) := {ti : ℕ × ℕ | ti.2 < M.numHist ti.1} +def MDP.histIdxValid (M : MDP W) := {ti : ℕ × ℕ | ti.2 < M.numHist ti.1} -variable (M : MDP R) (t : ℕ) +variable (M : MDP W) (t : ℕ) theorem exists_init_of_length_eq_zero (h : M.HistOfLength 0) : ∃s, h.val = Hist.init s := sorry theorem exists_foll_of_length_eq_succ (h : M.HistOfLength t.succ) : ∃h',∃a,∃s, h.val = Hist.foll h' a s := sorry -theorem leftInverse_idxToHist_histToIdx (M : MDP R) : LeftInverse (M.idxToHist' t) (M.histToIdx' t) := by +theorem leftInverse_idxToHist_histToIdx (M : MDP W) : LeftInverse (M.idxToHist' t) (M.histToIdx' t) := by intro h unfold MDP.idxToHist' MDP.histToIdx' --simp only @@ -321,7 +321,7 @@ def MDP.histToTuple : HistNonempty M → Hist M × (Fin M.A) × (Fin M.S) open Function -variable {M : MDP R} +variable {M : MDP W} -- mapping between tuples and histories are injective lemma leftInverse_histToTuple_tupleToHist : LeftInverse M.histToTuple M.tupleToHist := fun _ ↦ rfl @@ -332,8 +332,8 @@ def tupleToHistNEEmbedding : Hist M × (Fin M.A) × (Fin M.S) ↪ HistNonempty M def tupleToHistEmbedding : Hist M × (Fin M.A) × (Fin M.S) ↪ Hist M := ⟨λ x ↦ M.tupleToHist x, val_comp_tupleToHist_injective⟩ --- state -def MDP.stateToHist (M : MDP R) (s : Fin M.S) : Hist M := Hist.init s -def MDP.histToState (M : MDP R) : Hist M → (Fin M.S) +def MDP.stateToHist (M : MDP W) (s : Fin M.S) : Hist M := Hist.init s +def MDP.histToState (M : MDP W) : Hist M → (Fin M.S) | Hist.init s => s | Hist.foll _ _ s => s @@ -372,7 +372,7 @@ theorem length_foll (h : Hist M) (a : M.Action) (s : M.State) : (h.foll a s).len by rewrite [Hist.length.eq_def]; exact Nat.add_comm 1 h.length /-- All histories of a given length -/ -def MDP.historiesHorizon (M : MDP R) (t : ℕ) : Finset (Hist M) := +def MDP.historiesHorizon (M : MDP W) (t : ℕ) : Finset (Hist M) := match t with | Nat.zero => M.setS.map stateToHistEmbedding | Nat.succ t => ((M.historiesHorizon t) ×ˢ M.setA ×ˢ M.setS).map tupleToHistEmbedding @@ -416,7 +416,7 @@ theorem length_eq_of_mem_historiesHorizon (t : ℕ) (h : Hist M) (hh : h ∈ M.h rw [ih h' hasi.1] exact Nat.add_comm 1 t' -def MDP.historiesHorizonT (M : MDP R) (t : ℕ) : Finset (M.HistOfLength t) := +def MDP.historiesHorizonT (M : MDP W) (t : ℕ) : Finset (M.HistOfLength t) := let H := M.historiesHorizon t let f : {h : Hist M // h ∈ H} → M.HistOfLength t := fun hh => ⟨hh.1, length_eq_of_mem_historiesHorizon t hh.1 hh.2⟩ have finj : Injective f := by unfold Injective f; intro h₁ h₂ steq; grind only @@ -430,7 +430,7 @@ theorem mem_historiesHorizonT (t : ℕ) (h : M.HistOfLength t) : h ∈ M.histori use ⟨h.1, mem_historiesHorizon t h⟩ exact ⟨Finset.mem_attach _ _, rfl⟩ -instance (M : MDP R) (t : ℕ) : Fintype (M.HistOfLength t) where +instance (M : MDP W) (t : ℕ) : Fintype (M.HistOfLength t) where elems := M.historiesHorizonT t complete := fun h => mem_historiesHorizonT t h diff --git a/MDPLib/Probability/Basic.lean b/MDPLib/Probability/Basic.lean index b74369a..3c121eb 100644 --- a/MDPLib/Probability/Basic.lean +++ b/MDPLib/Probability/Basic.lean @@ -8,11 +8,16 @@ import Mathlib.Data.Fin.Tuple.Sort -- for Equiv.Perm and permutation operations set_option linter.unusedSectionVars false -variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R] - [CharZero R] [Archimedean R] +variable {W : Type} [Field W] [LinearOrder W] [IsStrictOrderedRing W] + [CharZero W] [Archimedean W] + + +-- `to_dual` translates a lemma about `ℙ` only if its `relevant_arg` is translated. By default +-- that is the first ordered type, the probability type `W`. The probability lemmas below set +-- `(relevant_arg := V)` instead, so that proofs tagged `@[to_dual (dont_translate := W)]` +-- (which keep the order on probabilities) still translate them. The linter flags each override. +set_option linter.translateRelevantArg false --- Synthesize NoMinOrder to reduce exists_gt in a proof below -attribute [to_dual existing] instNoMaxOrderOfNontrivial /-! @@ -29,7 +34,7 @@ attribute [to_dual existing] instNoMaxOrderOfNontrivial section General open Matrix -variable {Ω : Type} [FinEnum Ω] {p x : Ω → R} +variable {Ω : Type} [FinEnum Ω] {p x : Ω → W} /-- If a dot product with a nonnegative vector is positive, some coordinate of the vector is positive. -/ @@ -45,7 +50,7 @@ end General namespace Findist open FinRV -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} {B : FinRV Ω Bool} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist W Ω} {B : FinRV Ω Bool} theorem probability_nonneg : 0 ≤ ℙ[B // P] := by rw [probability_eq_expect_indicator] @@ -56,7 +61,7 @@ theorem probability_nonneg : 0 ≤ ℙ[B // P] := theorem probability_le_one : ℙ[B // P] ≤ 1 := by grw [probability_eq_expect_indicator, expect_mono indicator_le_one, expect_one] -theorem isProb_probability (P : Findist R Ω) : IsProb ℙ[B // P] := ⟨probability_nonneg, probability_le_one⟩ +theorem isProb_probability (P : Findist W Ω) : IsProb ℙ[B // P] := ⟨probability_nonneg, probability_le_one⟩ end Findist @@ -67,16 +72,16 @@ section RandomVariables namespace FinRV open Findist -variable {Ω : Type} [Nonempty Ω] {X Y : FinRV Ω R} {t t₁ t₂ : R} +variable {Ω : Type} [Nonempty Ω] {V : Type} [LinearOrder V] {X Y : FinRV Ω V} {t t₁ t₂ : V} -theorem indicator_leq_mono (h1 : X ≤ Y) (h2: t₁ ≤ t₂) : (𝕀 ∘ (Y ≤ᵣ t₁) : FinRV Ω R) ≤ 𝕀 ∘ (X ≤ᵣ t₂) := by +theorem indicator_leq_mono (h1 : X ≤ Y) (h2: t₁ ≤ t₂) : (𝕀 ∘ (Y ≤ᵣ t₁) : FinRV Ω W) ≤ 𝕀 ∘ (X ≤ᵣ t₂) := by intro ω by_cases h3 : Y ω ≤ t₁ · simp [FinRV.leq, 𝕀, indicator, h3, (le_trans (le_trans (h1 ω) h3) h2)] · by_cases h5 : X ω ≤ t₂ repeat simp [h3, h5, 𝕀, indicator] -theorem indicator_lt_mono (h1 : X ≤ Y) (h2: t₁ ≤ t₂) : (𝕀 ∘ (Y <ᵣ t₁) : FinRV Ω R) ≤ 𝕀 ∘ (X <ᵣ t₂) := by +theorem indicator_lt_mono (h1 : X ≤ Y) (h2: t₁ ≤ t₂) : (𝕀 ∘ (Y <ᵣ t₁) : FinRV Ω W) ≤ 𝕀 ∘ (X <ᵣ t₂) := by intro ω by_cases h3 : Y ω < t₁ · have h4 : X ω < t₂ := @@ -87,11 +92,11 @@ theorem indicator_lt_mono (h1 : X ≤ Y) (h2: t₁ ≤ t₂) : (𝕀 ∘ (Y <ᵣ · by_cases h5 : X ω < t₂ repeat simp [h3, h5, 𝕀, indicator] -theorem gt_of_geq_of_lt {t₁ t₂ : R} (h : t₁ < t₂) (ω) (hω : (X ≥ᵣ t₂) ω ) : (X >ᵣ t₁) ω := +theorem gt_of_geq_of_lt {t₁ t₂ : V} (h : t₁ < t₂) (ω) (hω : (X ≥ᵣ t₂) ω ) : (X >ᵣ t₁) ω := by simp [FinRV.gt, FinRV.geq] at hω ⊢ order -variable [FinEnum Ω] {P : Findist R Ω} {A B : FinRV Ω Bool} +variable [FinEnum Ω] {P : Findist W Ω} {A B : FinRV Ω Bool} @[to_dual geq_minQuark] theorem leq_maxQuark : (X ≤ᵣ X.maxQuark) = 1 := @@ -100,9 +105,9 @@ theorem leq_maxQuark : (X ≤ᵣ X.maxQuark) = 1 := -- results for discrete probability distributions section Atomic -variable (P : Findist R Ω) (X : FinRV Ω R) (t : R) +variable (P : Findist W Ω) (X : FinRV Ω V) (t : V) -theorem _root_.Findist.exists_eq_of_probability_pos {b : R} (h : ℙ[X =ᵣ b // P] > 0) : ∃ω, X ω = b := by +theorem _root_.Findist.exists_eq_of_probability_pos {b : V} (h : ℙ[X =ᵣ b // P] > 0) : ∃ω, X ω = b := by obtain ⟨ω, hω⟩ : ∃ω, (𝕀 ∘ (X=ᵣb)) ω > 0 := exists_pos_of_dotProduct_pos (P.nonneg) h use ω by_contra! @@ -111,12 +116,12 @@ theorem _root_.Findist.exists_eq_of_probability_pos {b : R} (h : ℙ[X =ᵣ b // section QuarkSubMax -variable {t y : R} (h : t < X.maxQuark) +variable {t y : V} (h : t < X.maxQuark) /-- Computes the smallest successive potential atom greater than `t`. see also: Finset.exists_next_right -/ @[to_dual] -- predQuark -def succQuark (t : R) (h : t < X.maxQuark) : R := +def succQuark (t : V) (h : t < X.maxQuark) : V := let 𝓨 := X.quarks.filter (fun x ↦ x > t) let h_nonempty : 𝓨.Nonempty := Finset.filter_nonempty_iff.mpr ⟨X.maxQuark, ⟨maxQuark_mem_quarks, h⟩⟩ 𝓨.min' h_nonempty @@ -145,7 +150,7 @@ theorem succQuark_nogap_ind' {ω} (hty : X ω < X.succQuark t h) : X ω ≤ t := succQuark_nogap_ind X h (mem_quarks ω) hty @[to_dual] -- predQuark_gtrv_eq_gerv -theorem succQuark_lt_eq_le {t : R} (h : t < X.maxQuark) : (X <ᵣ X.succQuark t h) = (X ≤ᵣ t) := by +theorem succQuark_lt_eq_le {t : V} (h : t < X.maxQuark) : (X <ᵣ X.succQuark t h) = (X ≤ᵣ t) := by ext ω; rw [FinRV.leq, FinRV.lt, decide_eq_decide] exact ⟨succQuark_nogap_ind' X h, (lt_of_le_of_lt · (succQuark_gt X h))⟩ @@ -160,17 +165,13 @@ theorem lt_eq_one_of_maxQuark_lt (h : X.maxQuark < t) : (X <ᵣ t) = 1 := /-- Because the distribution is discrete, there exists a value for which the distribution is the same -/ @[to_dual exists_geq_eq_gt] -theorem exists_leq_eq_lt : ∃q > t, (X ≤ᵣ t) = (X <ᵣ q) := +theorem exists_leq_eq_lt [NoMaxOrder V] : ∃q > t, (X ≤ᵣ t) = (X <ᵣ q) := if h : t < X.maxQuark then ⟨X.succQuark t h, ⟨succQuark_gt X h, (succQuark_lt_eq_le X h).symm⟩⟩ else let ⟨q, hq⟩ := exists_gt t --from NoMaxOrder have hm := le_of_not_gt h ⟨q, hq, by rw [leq_eq_one_of_maxQuark_le X hm, lt_eq_one_of_maxQuark_lt X (hm.trans_lt hq)]⟩ - -variable {t : ℚ} - - end QuarkSubMax end Atomic @@ -185,7 +186,7 @@ section Monotone open Function -variable {f : R → R} {x : R} +variable {f : V → V} {x : V} --- LE @@ -253,7 +254,8 @@ end Monotone section CashInvariance -variable (c : R) {x : R} +-- adds a constant to the values, so they are in `W` +variable (c : W) {X : FinRV Ω W} {x : W} omit [FinEnum Ω] in theorem leq_add_const : (X ≤ᵣ x) = (X + c•1 ≤ᵣ x + c) := by ext ω; simp @@ -271,8 +273,8 @@ end CashInvariance section Negation - -variable {x : R} +-- negates the values, so they are in `W` +variable {X : FinRV Ω W} {x : W} theorem leq_eq_neg_geq_neg : (X ≤ᵣ x) = (-X ≥ᵣ -x) := by ext ω; simp @@ -297,7 +299,8 @@ section Probability namespace Findist open FinRV -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} {A B C : FinRV Ω Bool} {X Y : FinRV Ω R} {t t₁ t₂ : R} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist W Ω} {A B C : FinRV Ω Bool} +variable {V : Type} [LinearOrder V] {X Y : FinRV Ω V} {t t₁ t₂ : V} theorem probability_add_probability_not : ℙ[B // P] + ℙ[¬ᵣB // P] = 1 := @@ -311,10 +314,10 @@ theorem probability_not : ℙ[¬ᵣB // P] = 1 - ℙ[B // P] := theorem _root_.FinRV.leq_sup_gt : (X ≤ᵣ t) ⊔ (X >ᵣ t) = 1 := by ext ω; simpa [FinRV.leq, FinRV.gt] using le_or_gt (X ω) t -@[to_dual probability_ge_lt_one] +@[to_dual (relevant_arg := V) probability_ge_lt_one] theorem probability_le_gt_one : ℙ[X ≤ᵣ t // P] + ℙ[X >ᵣ t // P] = 1 := by rw [probability_eq_expect_indicator, probability_eq_expect_indicator, ←expect_add] - have h : (𝕀 ∘ (X ≤ᵣ t)) + (𝕀 ∘ (X >ᵣ t)) = (1 : FinRV Ω R) := by + have h : (𝕀 ∘ (X ≤ᵣ t)) + (𝕀 ∘ (X >ᵣ t)) = (1 : FinRV Ω W) := by ext ω unfold FinRV.leq FinRV.gt simp [𝕀, indicator] @@ -337,9 +340,11 @@ theorem probability_le_eq_one_sub : ℙ[X ≤ᵣ t // P] = 1 - ℙ[X >ᵣ t // rw [←probability_le_gt_one (P := P) (X := X) (t := t)] ring +@[to_dual existing (relevant_arg := V) probability_le_eq_one_sub] theorem probability_ge_eq_one_sub : ℙ[X ≥ᵣ t // P] = 1 - ℙ[X <ᵣ t // P] := by rw [← probability_lt_ge_one (P := P) (X := X) (t := t)]; ring +@[to_dual existing (relevant_arg := V) probability_gt_eq_one_sub] theorem probability_lt_eq_one_sub : ℙ[X <ᵣ t // P] = 1 - ℙ[X ≥ᵣ t // P] := by rw [← probability_lt_ge_one (P := P) (X := X) (t := t)]; ring @@ -365,11 +370,11 @@ theorem probability_gt_anti : X ≤ Y → t₁ ≤ t₂ → ℙ[Y >ᵣ t₁ // P have := probability_le_mono (P := P) hxy ht linarith -theorem probability_leq_le_probability_lt {q : R} (h : q > t) : ℙ[X <ᵣ q // P] ≥ ℙ[X ≤ᵣ t // P] := by +theorem probability_leq_le_probability_lt {q : V} (h : q > t) : ℙ[X <ᵣ q // P] ≥ ℙ[X ≤ᵣ t // P] := by unfold probability apply Finset.sum_le_sum intro ω hω - have h2 : (𝕀 ∘ (X ≤ᵣ t) : FinRV Ω R) ω ≤ (𝕀 ∘ (X <ᵣ q) : FinRV Ω R) ω := + have h2 : (𝕀 ∘ (X ≤ᵣ t) : FinRV Ω W) ω ≤ (𝕀 ∘ (X <ᵣ q) : FinRV Ω W) ω := by by_cases h3 : X ω ≤ t · have h4 : X ω < q := lt_of_le_of_lt h3 h simp [FinRV.leq, FinRV.lt, 𝕀, indicator, Function.comp, h3, h4] @@ -377,13 +382,14 @@ theorem probability_leq_le_probability_lt {q : R} (h : q > t) : ℙ[X <ᵣ q // by_cases h5 : X ω < q <;> simp [h5] exact mul_le_mul_of_nonneg_left h2 (P.nonneg ω) -@[to_dual probability_geq_minQuark] +@[to_dual (relevant_arg := V) probability_geq_minQuark] theorem probability_leq_maxQuark : ℙ[X ≤ᵣ X.maxQuark // P] = 1 := by rw [leq_maxQuark]; exact probability_one P +@[to_dual (relevant_arg := V) probability_gt_maxQuark] theorem probability_lt_minQuark : ℙ[X <ᵣ X.minQuark // P] = 0 := by rw [probability_lt_eq_one_sub, probability_geq_minQuark]; exact sub_self 1 -theorem lt_maxQuark_of_probability_leq_lt_one {t : R} (h : ℙ[X ≤ᵣ t // P] < 1) : t < X.maxQuark := by +theorem lt_maxQuark_of_probability_leq_lt_one {t : V} (h : ℙ[X ≤ᵣ t // P] < 1) : t < X.maxQuark := by by_contra! hcontra have h1 := probability_le_mono (P := P) (le_refl X) hcontra rw [probability_leq_maxQuark] at h1 @@ -391,7 +397,7 @@ theorem lt_maxQuark_of_probability_leq_lt_one {t : R} (h : ℙ[X ≤ᵣ t // P] section Rounding ---results for discrete probability distributions -variable (P : Findist R Ω) (X : FinRV Ω R) (t : R) +variable (P : Findist W Ω) (X : FinRV Ω V) (t : V) --TODO: not clear if we need this one. Delete? theorem exists_probability_leq_eq_probability_lt_of_lt_maxQuark (h: t < X.maxQuark) : @@ -402,7 +408,7 @@ theorem exists_probability_leq_eq_probability_lt_of_lt_maxQuark (h: t < X.maxQua --TODO: not clear if we need this one. Delete? /-- similar to `exists_probability_leq_eq_probability_lt_of_lt_maxQuark` but no precondition -/ -theorem exists_probability_leq_eq_probability_lt : ∃q > t, ℙ[X ≤ᵣ t // P] = ℙ[X <ᵣ q // P] := +theorem exists_probability_leq_eq_probability_lt [NoMaxOrder V] : ∃q > t, ℙ[X ≤ᵣ t // P] = ℙ[X <ᵣ q // P] := let ⟨q, hq⟩ := exists_leq_eq_lt X (t := t) Exists.intro q ⟨hq.1, probability_congr hq.2⟩ @@ -417,7 +423,7 @@ section Monotone open Function -variable {f : R → R} {x : R} +variable {f : V → V} {x : V} --- LE theorem _root_.Monotone.probability_le (hm : Monotone f) : ℙ[X ≤ᵣ x // P] ≤ ℙ[f ∘ X ≤ᵣ f x // P] := @@ -446,7 +452,8 @@ end Monotone section CashInvariance -variable (c : R) {x : R} +-- adds a constant to the values, so they are in `W` +variable (c : W) {X : FinRV Ω W} {x : W} theorem probability_leq_add_const : ℙ[X ≤ᵣ x // P] = ℙ[X + c•1 ≤ᵣ x + c // P] := probability_congr (leq_add_const c) @@ -460,7 +467,8 @@ end CashInvariance section Negation -variable {x : R} +-- negates the values, so they are in `W` +variable {X : FinRV Ω W} {x : W} theorem probability_leq_eq_neg_geq_neg : ℙ[X ≤ᵣ x // P] = ℙ[-X ≥ᵣ -x // P] := by rw [leq_eq_neg_geq_neg] @@ -484,7 +492,8 @@ section CDF namespace Findist open FinRV -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} {X Y : FinRV Ω R} {t t₁ t₂ : R} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist W Ω} +variable {V : Type} [LinearOrder V] {X Y : FinRV Ω V} {t t₁ t₂ : V} /-- shows CDF is non-decreasing -/ theorem cdf_mono : t₁ ≤ t₂ → cdf P X t₁ ≤ cdf P X t₂ := by @@ -506,9 +515,9 @@ section Expectation namespace Findist open FinRV -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} -variable {k : ℕ} {X : FinRV Ω R} {B : FinRV Ω Bool} {L : FinRV Ω (Fin k)} -variable (g : Fin k → R) +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist W Ω} +variable {k : ℕ} {X : FinRV Ω W} {B : FinRV Ω Bool} {L : FinRV Ω (Fin k)} +variable (g : Fin k → W) /-- expect_comp_eq_sum: The law of the unconscious statistician (or similar) -/ theorem expect_comp_eq_sum : 𝔼[g ∘ L // P ] = ∑ i, ℙ[L =ᵣ i // P] * (g i) := @@ -533,18 +542,18 @@ theorem expect_expectCondRV : 𝔼[𝔼[X |ᵣ L // P] // P] = 𝔼[X // P] := section RV_Unique_Values -variable {τ:Type} [DecidableEq τ] +variable {V : Type} [DecidableEq V] /-- The distinct values of a random variable, as a deduplicated list built from the enumeration of the sample space. -/ -def _root_.FinRV.imageList (X : FinRV Ω τ) : List τ := List.dedup ((FinEnum.toList Ω).map X) +def _root_.FinRV.imageList (X : FinRV Ω V) : List V := List.dedup ((FinEnum.toList Ω).map X) /-- The quarks of `X` equal the `toFinset` of its `imageList`. -/ -theorem _root_.FinRV.quarks_eq_imageList_toFinset (X : FinRV Ω τ) : X.quarks = X.imageList.toFinset := by +theorem _root_.FinRV.quarks_eq_imageList_toFinset (X : FinRV Ω V) : X.quarks = X.imageList.toFinset := by ext y simp [FinRV.imageList] -theorem _root_.FinRV.sum_image_univ_eq_sum_imageList (f : R → R) : +theorem _root_.FinRV.sum_image_univ_eq_sum_imageList (f : W → W) : (∑ y ∈ X.quarks, f y) = ((X.imageList).map f).sum := by rw [quarks_eq_imageList_toFinset] exact List.sum_toFinset f (List.nodup_dedup _) @@ -552,7 +561,7 @@ theorem _root_.FinRV.sum_image_univ_eq_sum_imageList (f : R → R) : section Generic -variable {X : FinRV Ω τ} +variable {X : FinRV Ω V} theorem _root_.FinRV.apply_mem_imageList (ω : Ω) : X ω ∈ X.imageList := by simp only [FinRV.imageList, List.mem_dedup, List.mem_map] @@ -563,14 +572,14 @@ theorem _root_.FinRV.exists_getElem_imageList (ω) : ∃ i : Fin X.imageList.len theorem _root_.FinRV.imageList_nodup : X.imageList.Nodup := List.nodup_dedup _ -def _root_.MDPLib.List.finIdxOf (L : List τ) (a : τ) (h : a ∈ L) : Fin L.length := +def _root_.MDPLib.List.finIdxOf (L : List V) (a : V) (h : a ∈ L) : Fin L.length := ⟨L.idxOf a, List.idxOf_lt_length_of_mem h⟩ @[simp] -theorem _root_.MDPLib.List.getElem_finIdxOf (L : List τ) (a : τ) (h : a ∈ L) : L[MDPLib.List.finIdxOf L a h] = a := +theorem _root_.MDPLib.List.getElem_finIdxOf (L : List V) (a : V) (h : a ∈ L) : L[MDPLib.List.finIdxOf L a h] = a := List.getElem_idxOf (List.idxOf_lt_length_of_mem h) -def _root_.FinRV.imageIdxOf (X : FinRV Ω τ) (ω : Ω) : Fin (X.imageList.length) := +def _root_.FinRV.imageIdxOf (X : FinRV Ω V) (ω : Ω) : Fin (X.imageList.length) := MDPLib.List.finIdxOf X.imageList (X ω) (apply_mem_imageList ω) @[simp] @@ -588,7 +597,7 @@ theorem _root_.FinRV.eq_getElem_iff_imageIdxOf_eq {ω i} : X ω = X.imageList[i] end Generic -theorem _root_.FinRV.sum_image_univ_eq_sum_fin (f : R → R) : +theorem _root_.FinRV.sum_image_univ_eq_sum_fin (f : W → W) : ∑ y ∈ X.quarks, f y = ∑ i : Fin X.imageList.length, f (X.imageList[i]) := by rw [sum_image_univ_eq_sum_imageList, ← List.ofFn_getElem_eq_map, List.sum_ofFn]; rfl @@ -605,9 +614,6 @@ theorem expect_eq_sum_probability_mul : 𝔼[ X // P] = ∑ y ∈ X.quarks, (ℙ rw [show (X =ᵣ X.imageList[i]) = (L =ᵣ i) by ext ω; simpa [L, FinRV.eq] using eq_getElem_iff_imageIdxOf_eq] --- theorem expect_def_correct2 : 𝔼[ X // P] = ∑ y ∈ X.imageList, ℙ[ X =ᵣ y // P] * y := by sorry - - end RV_Unique_Values end Findist @@ -619,11 +625,11 @@ namespace Findist open FinRV variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {k : ℕ} {L : FinRV Ω (Fin k)} -variable {P : Findist R Ω} {B : FinRV Ω Bool} +variable {P : Findist W Ω} {B : FinRV Ω Bool} /-- The law of total probabilities -/ theorem probability_eq_sum : ℙ[B // P] = ∑ i, ℙ[B ⊓ (L =ᵣ i) // P] := by - rewrite [probability_eq_expect_indicator, eq_sum_mul_indicatorEq (𝕀∘B : FinRV Ω R) L, expect_sum] + rewrite [probability_eq_expect_indicator, eq_sum_mul_indicatorEq (𝕀∘B : FinRV Ω W) L, expect_sum] apply Fintype.sum_congr intro i rewrite [probability_eq_expect_indicator] @@ -642,24 +648,25 @@ section Probability_Permutation namespace Findist open FinRV -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} {A B : FinRV Ω Bool} {X Y : FinRV Ω R} {t : R} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist W Ω} {A B : FinRV Ω Bool} +variable {V : Type} [LinearOrder V] {X : FinRV Ω V} {t : V} -def comp (P : Findist R Ω) (σ : Equiv.Perm (Ω)) : Findist R Ω where +def comp (P : Findist W Ω) (σ : Equiv.Perm (Ω)) : Findist W Ω where p := P.p ∘ σ sum_eq_one := by - have h1 : 1 = (1 : Ω → R) ∘ σ := rfl + have h1 : 1 = (1 : Ω → W) ∘ σ := rfl rw [h1, comp_equiv_dotProduct_comp_equiv 1 P.p σ] exact P.sum_eq_one nonneg := fun ω => P.nonneg (σ ω) variable (σ : Equiv.Perm (Ω)) -theorem expect_comp_perm : 𝔼[X ∘ σ // P.comp σ] = 𝔼[X // P] := by +theorem expect_comp_perm {X : FinRV Ω W} : 𝔼[X ∘ σ // P.comp σ] = 𝔼[X // P] := by unfold expect Findist.comp exact (comp_equiv_dotProduct_comp_equiv P.1 X σ) theorem probability_comp_perm : ℙ[A ∘ σ // P.comp σ] = ℙ[A // P] := by - have h1 : (𝕀 ∘ A ∘ σ : FinRV Ω R) = (𝕀 ∘ A) ∘ σ := by rfl + have h1 : (𝕀 ∘ A ∘ σ : FinRV Ω W) = (𝕀 ∘ A) ∘ σ := by rfl rw [probability_eq_expect_indicator, h1, expect_comp_perm, ←probability_eq_expect_indicator] theorem _root_.FinRV.leq_comp_perm : (X ∘ σ ≤ᵣ t) = (X ≤ᵣ t) ∘ σ := by unfold FinRV.leq; grind only diff --git a/MDPLib/Probability/Defs.lean b/MDPLib/Probability/Defs.lean index 7d9ba39..1925e4d 100644 --- a/MDPLib/Probability/Defs.lean +++ b/MDPLib/Probability/Defs.lean @@ -10,16 +10,22 @@ import Mathlib.Algebra.Ring.BooleanRing -- `0`, `1` on Bool set_option linter.unusedSectionVars false --- The scalar type: any linear ordered field (see `MDPLib/Probability/Prelude.lean`). --- the particular targets are: ℚ for computability and ℝ for proofs -variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [CharZero R] [Archimedean R] +-- Two types, by role: +-- * `W` (weights): probabilities, and the values of random variables that are combined with +-- them arithmetically (expectation, CVaR). Any linear ordered field (see +-- `MDPLib/Probability/Prelude.lean`); the targets are ℚ for computability and ℝ for proofs. +-- * `V` (values): the values of random variables whose results only need the order on them +-- (events, `ℙ`, the CDF, quantiles, VaR). Any linear order, e.g. `W` itself, ℕ, or ℤ. +-- Keeping `V` separate from `W` lets `@[to_dual (dont_translate := W)]` reverse the order on +-- values without also reversing it on probabilities. +variable {W : Type} [Field W] [LinearOrder W] [IsStrictOrderedRing W] [CharZero W] [Archimedean W] --------------------------- Findist --------------------------------------------------------------- -structure Findist (R : Type) [Field R] [LinearOrder R] [IsStrictOrderedRing R] (Ω : Type) [FinEnum Ω] : Type where +structure Findist (W : Type) [Field W] [LinearOrder W] [IsStrictOrderedRing W] (Ω : Type) [FinEnum Ω] : Type where /-- Probability measure -/ - p : Ω → R + p : Ω → W sum_eq_one : 1 ⬝ᵥ p = 1 nonneg : 0 ≤ p @@ -27,14 +33,14 @@ namespace Findist /-- Finite probability distribution -/ -abbrev Delta (R : Type) [Field R] [LinearOrder R] [IsStrictOrderedRing R] (Ω : Type) [FinEnum Ω] : Type := Findist R Ω +abbrev Delta (W : Type) [Field W] [LinearOrder W] [IsStrictOrderedRing W] (Ω : Type) [FinEnum Ω] : Type := Findist W Ω /-- Finite probability distribution -/ -abbrev Δ (R : Type) [Field R] [LinearOrder R] [IsStrictOrderedRing R] (Ω : Type) [FinEnum Ω] : Type := Delta R Ω +abbrev Δ (W : Type) [Field W] [LinearOrder W] [IsStrictOrderedRing W] (Ω : Type) [FinEnum Ω] : Type := Delta W Ω /-- Dirac (point mass) distribution concentrated at `ω₀`. -/ -- NOTE(mathlib): `p` here is `Pi.single ω₀ 1`; cf. `StdSimplex.single` / `single_mem_stdSimplex`. -def dirac {Ω : Type} [FinEnum Ω] (ω₀ : Ω) : Findist R Ω where +def dirac {Ω : Type} [FinEnum Ω] (ω₀ : Ω) : Findist W Ω where p := fun ω => if ω = ω₀ then 1 else 0 sum_eq_one := by simp [dotProduct] nonneg := by intro ω; by_cases h : ω = ω₀ <;> simp [h] @@ -43,14 +49,14 @@ variable {Ω : Type} [FinEnum Ω] /-- The sample space of a probability distribution is nonempty. -/ -theorem nonempty (P : Findist R Ω) : Nonempty Ω := by +theorem nonempty (P : Findist W Ω) : Nonempty Ω := by by_contra h rw [not_nonempty_iff] at h have := P.sum_eq_one simp_all only [Matrix.dotProduct_of_isEmpty, zero_ne_one] /-- A distribution over an empty sample space is impossible. -/ -theorem isEmpty_elim [IsEmpty Ω] (P : Findist R Ω) : False := +theorem isEmpty_elim [IsEmpty Ω] (P : Findist W Ω) : False := (not_nonempty_iff.mpr ‹_›) P.nonempty @@ -69,7 +75,7 @@ using the standard notation: - L =ᵣ i is a boolean indicator random variable -- L =ᵢ i is an `R`-valued indicator random variable +- L =ᵢ i is a `W`-valued indicator random variable - L ≤ᵣ i is a bool indicator random variable Main results @@ -80,11 +86,11 @@ Main results section RandomVariable -/-- A finite random variable: a bare function from the sample space `Ω` to `ρ`. +/-- A finite random variable: a bare function from the sample space `Ω` to `V`. The `FinEnum` instance lives on `Ω` and is shared with the distribution function. -/ -abbrev FinRV (Ω : Type) [Nonempty Ω] (ρ : Type) := Ω → ρ +abbrev FinRV (Ω : Type) [Nonempty Ω] (V : Type) := Ω → V -variable {Ω : Type} [Nonempty Ω] {ρ : Type} +variable {Ω : Type} [Nonempty Ω] {V : Type} namespace FinRV @@ -111,22 +117,22 @@ variable {A B : Bool} prefix:40 "¬ᵣ" => FinRV.not /-- Boolean random variable representing an quality condition -/ -@[simp] def eq [DecidableEq ρ] (Y : FinRV Ω ρ) (y : ρ) : FinRV Ω Bool := +@[simp] def eq [DecidableEq V] (Y : FinRV Ω V) (y : V) : FinRV Ω Bool := (fun ω ↦ decide (Y ω = y)) /-- Boolean random variable representing an quality condition -/ infix:50 "=ᵣ" => FinRV.eq /-- 0/1 random variable representing an quality condition -/ -@[simp] def indicatorEq {R : Type} [Zero R] [One R] [DecidableEq ρ] (Y : FinRV Ω ρ) (y : ρ) : - FinRV Ω R := +@[simp] def indicatorEq {W : Type} [Zero W] [One W] [DecidableEq V] (Y : FinRV Ω V) (y : V) : + FinRV Ω W := (fun ω ↦ if Y ω = y then 1 else 0) /-- 0/1 random variable representing an quality condition -/ infix:50 "=ᵢ" => FinRV.indicatorEq /-- Boolean random variable represening Y ≤ y inequality -/ -@[simp] def leq [LE ρ] [DecidableLE ρ] (Y : FinRV Ω ρ) (y : ρ) : FinRV Ω Bool := +@[simp] def leq [LE V] [DecidableLE V] (Y : FinRV Ω V) (y : V) : FinRV Ω Bool := (fun ω ↦ Y ω ≤ y) /-- Boolean random variable represening Y ≤ y inequality -/ @@ -134,7 +140,7 @@ infix:50 "≤ᵣ" => FinRV.leq /-- Boolean random variable represening Y ≤ y inequality -/ @[simp] -def lt [LT ρ] [DecidableLT ρ] (Y : FinRV Ω ρ) (y : ρ) : FinRV Ω Bool := +def lt [LT V] [DecidableLT V] (Y : FinRV Ω V) (y : V) : FinRV Ω Bool := (fun ω ↦ Y ω < y) /-- Boolean random variable represening Y ≤ y inequality -/ @@ -142,20 +148,20 @@ infix:50 "<ᵣ" => FinRV.lt /-- Boolean random variable represening Y ≤ y inequality -/ @[simp, to_dual existing leq] -def geq [LE ρ] [DecidableLE ρ] (Y : FinRV Ω ρ) (y : ρ) : FinRV Ω Bool := +def geq [LE V] [DecidableLE V] (Y : FinRV Ω V) (y : V) : FinRV Ω Bool := (fun ω ↦ Y ω ≥ y) /-- Boolean random variable represening Y ≤ y inequality -/ infix:50 "≥ᵣ" => FinRV.geq /-- Boolean random variable represening Y > y inequality -/ -@[simp, to_dual existing lt] def gt [LT ρ] [DecidableLT ρ] (Y : FinRV Ω ρ) (y : ρ) : FinRV Ω Bool := +@[simp, to_dual existing lt] def gt [LT V] [DecidableLT V] (Y : FinRV Ω V) (y : V) : FinRV Ω Bool := fun ω ↦ Y ω > y /-- Boolean random variable represening Y > y inequality -/ infix:50 ">ᵣ" => FinRV.gt ---instance instCoeFinRV_Fun : Coe (FinRV Ω ρ) (Ω → ρ) where +--instance instCoeFinRV_Fun : Coe (FinRV Ω V) (Ω → V) where -- coe a := a /-- Equivalence when adding an element to integer comparison. -/ @@ -165,83 +171,81 @@ theorem leq_sup_eq_succ (D : FinRV Ω ℕ) (m : ℕ) : ((D ≤ᵣ m) ⊔ (D =ᵣ by_cases h₁ : D x ≤ m <;> by_cases h₂ : D x = m + 1 <;> simp [h₁, h₂] <;> omega /-- Defines a preimage of an RV. This is a set with a decidable membership. -/ -def preimage (f : FinRV Ω ρ) : ρ → Set Ω := +def preimage (f : FinRV Ω V) : V → Set Ω := fun t => { m : Ω | f m = t} -variable {β : Type} [DecidableEq β] [FinEnum Ω] +variable [DecidableEq V] [FinEnum Ω] /-! Finite set of potential atoms of X (probability may be zero) -/ -abbrev quarks (X : FinRV Ω β) := Finset.univ.image X +abbrev quarks (X : FinRV Ω V) := Finset.univ.image X -theorem mem_quarks {X : FinRV Ω β} (ω) : X ω ∈ X.quarks := Finset.mem_image_of_mem X (Finset.mem_univ ω) +theorem mem_quarks {X : FinRV Ω V} (ω) : X ω ∈ X.quarks := Finset.mem_image_of_mem X (Finset.mem_univ ω) -theorem quarks_nonempty {X : FinRV Ω β} : X.quarks.Nonempty := Finset.univ_nonempty.image X +theorem quarks_nonempty {X : FinRV Ω V} : X.quarks.Nonempty := Finset.univ_nonempty.image X end FinRV namespace FinRV /-- Boolean indicator function -/ -def indicator {R : Type} [Zero R] [One R] (cond : Bool) : R := cond.rec 0 1 +def indicator {W : Type} [Zero W] [One W] (cond : Bool) : W := cond.rec 0 1 /-- Boolean indicator function -/ -abbrev 𝕀 {R : Type} [Zero R] [One R] : Bool → R := indicator +abbrev 𝕀 {W : Type} [Zero W] [One W] : Bool → W := indicator variable {k : ℕ} {L : FinRV Ω (Fin k)} -theorem indicator_comp_eq_indicatorEq : ∀i : Fin k, (𝕀 ∘ (L =ᵣ i) : FinRV Ω R) = (L =ᵢ i) := by +theorem indicator_comp_eq_indicatorEq : ∀i : Fin k, (𝕀 ∘ (L =ᵣ i) : FinRV Ω W) = (L =ᵢ i) := by intro i; unfold FinRV.eq FinRV.indicatorEq 𝕀 indicator; ext ω; by_cases h: L ω = i; repeat simp [h] variable {B : FinRV Ω Bool} -theorem indicator_eq_one_or_eq_zero {ω : Ω} : (𝕀∘B : FinRV Ω R) ω = 1 ∨ (𝕀∘B : FinRV Ω R) ω = 0 := by +theorem indicator_eq_one_or_eq_zero {ω : Ω} : (𝕀∘B : FinRV Ω W) ω = 1 ∨ (𝕀∘B : FinRV Ω W) ω = 0 := by by_cases h : B ω · left; simp only [Function.comp_apply, h, indicator] · right; simp only [Function.comp_apply, h, indicator] /-- Indicator is 0 or 1 -/ -theorem indicator_nonneg : (0 : FinRV Ω R) ≤ 𝕀∘B := by +theorem indicator_nonneg : (0 : FinRV Ω W) ≤ 𝕀∘B := by intro ω; unfold 𝕀 indicator; by_cases h : B ω; repeat simp [h] -theorem indicator_le_one : (𝕀∘B : FinRV Ω R) ≤ 1 := +theorem indicator_le_one : (𝕀∘B : FinRV Ω W) ≤ 1 := by unfold 𝕀 indicator; intro ω; by_cases h : B ω; repeat simp [h] -variable {c : R} {X : FinRV Ω R} +variable {c : W} {X : FinRV Ω W} omit [Nonempty Ω] in -theorem const_eq_smul_one : (fun _ ↦ c : FinRV Ω R) = c • 1 := by ext; simp; +theorem const_eq_smul_one : (fun _ ↦ c : FinRV Ω W) = c • 1 := by ext; simp; -theorem eq_sum_mul_indicatorEq (X : FinRV Ω R) (L : FinRV Ω (Fin k)) : X = ∑ i, X * (L =ᵢ i) := by ext ω; simp +theorem eq_sum_mul_indicatorEq (X : FinRV Ω W) (L : FinRV Ω (Fin k)) : X = ∑ i, X * (L =ᵢ i) := by ext ω; simp omit [Nonempty Ω] in -theorem indicator_one : 𝕀 ∘ (1 : Ω → Bool) = (1 : Ω → R) := by ext; simp [𝕀, indicator] +theorem indicator_one : 𝕀 ∘ (1 : Ω → Bool) = (1 : Ω → W) := by ext; simp [𝕀, indicator] theorem sup_not_eq_one : B ⊔ (¬ᵣ B) = (1 : FinRV Ω Bool) := by ext ω; unfold FinRV.not; simp -theorem indicator_add_indicator_not_eq_one : (𝕀∘B) + (𝕀∘(¬ᵣ B)) = (1 : FinRV Ω R) := +theorem indicator_add_indicator_not_eq_one : (𝕀∘B) + (𝕀∘(¬ᵣ B)) = (1 : FinRV Ω W) := by ext ω; unfold FinRV.not 𝕀 indicator Bool.not by_cases h : B ω <;> simp [h] -variable {X Y: FinRV Ω R} {Xs : Fin k → FinRV Ω R} +variable {X Y: FinRV Ω W} {Xs : Fin k → FinRV Ω W} theorem rv_le_abs : X ≤ abs ∘ X := le_abs_self X theorem rv_prod_sum_additive : ∑ i, Y * (Xs i) = Y * (∑ i, Xs i) := Eq.symm (Finset.mul_sum Finset.univ Xs Y) -variable {g : Fin k → R} +variable {g : Fin k → W} theorem comp_mul_indicatorEq (i) : (g ∘ L) * (L =ᵢ i) = (g i) • (L =ᵢ i) := by ext ω; by_cases h : L ω = i <;> simp [h] -variable {β : Type} -- general type, but different from the scalar type; could be an integer or categorical - -- assume enumerability of Ω from here because we need a probability space -variable [FinEnum Ω] [LinearOrder β] +variable [FinEnum Ω] [LinearOrder V] @[to_dual] -- minQuark -def maxQuark (X : FinRV Ω β) : β := X.quarks.max' quarks_nonempty +def maxQuark (X : FinRV Ω V) : V := X.quarks.max' quarks_nonempty -variable {X : FinRV Ω β} +variable {X : FinRV Ω V} @[to_dual] theorem maxQuark_mem_quarks : X.maxQuark ∈ X.quarks := Finset.max'_mem _ quarks_nonempty @@ -260,33 +264,33 @@ open FinRV section Probability -variable {Ω : Type} [Nonempty Ω] [FinEnum Ω] (P : Findist R Ω) (B C : FinRV Ω Bool) +variable {Ω : Type} [Nonempty Ω] [FinEnum Ω] (P : Findist W Ω) (B C : FinRV Ω Bool) /-- Probability of B -/ -def probability : R := P.p ⬝ᵥ (𝕀 ∘ B) +def probability : W := P.p ⬝ᵥ (𝕀 ∘ B) /-- Probability of B -/ notation "ℙ[" B "//" P "]" => probability P B /-- Conditional probability of B on C -/ -def probabilityCond : R := ℙ[B ⊓ C // P] / ℙ[ C // P ] +def probabilityCond : W := ℙ[B ⊓ C // P] / ℙ[ C // P ] /-- Conditional probability of B on C -/ notation "ℙ[" B "|" C "//" P "]" => probabilityCond P B C /-- Elements of Ω with positive probability -/ -def support (P : Findist R Ω) : Finset Ω := Finset.univ.filter (fun ω => P.p ω > 0) +def support (P : Findist W Ω) : Finset Ω := Finset.univ.filter (fun ω => P.p ω > 0) /-- Values of X with positive probability -/ -def atoms (P : Findist R Ω) (X : FinRV Ω R) : Finset R := P.support.image X +def atoms {V : Type} [DecidableEq V] (P : Findist W Ω) (X : FinRV Ω V) : Finset V := P.support.image X theorem probability_one : ℙ[1 // P] = 1 := by rewrite [probability, indicator_one, dotProduct_comm] exact P.sum_eq_one -example {a b : R} (h : 0 ≤ a) (h2 : 0 ≤ b) : 0 ≤ a * b := mul_nonneg h h2 +example {a b : W} (h : 0 ≤ a) (h2 : 0 ≤ b) : 0 ≤ a * b := mul_nonneg h h2 -variable {P : Findist R Ω} {B : FinRV Ω Bool} +variable {P : Findist W Ω} {B : FinRV Ω Bool} theorem probability_congr {A : FinRV Ω Bool} (h : A = B) : ℙ[A // P] = ℙ[B // P] := congrArg (probability P) h @@ -296,11 +300,11 @@ theorem mul_eq_zero_of_probability_eq_zero (h : ℙ[B // P] = 0) : (P.p * (𝕀 ------------------------------ IsPMF --------------------------- /-- Proof that p is a the IsPMF of X on probability space P -/ -def IsPMF {K : ℕ} (pmf : Fin K → R) (P : Findist R Ω) (L : FinRV Ω (Fin K)) := +def IsPMF {K : ℕ} (pmf : Fin K → W) (P : Findist W Ω) (L : FinRV Ω (Fin K)) := ∀ k : Fin K, pmf k = ℙ[ L =ᵣ k // P] variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {k : ℕ} {L : FinRV Ω (Fin k)} -variable {pmf : Fin k → R} {P : Findist R Ω} +variable {pmf : Fin k → W} {P : Findist W Ω} theorem IsPMF.pos (h : IsPMF pmf P L) : 0 < k := match k with @@ -313,12 +317,9 @@ end Probability section CDF -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] - -def cdf (P : Findist R Ω) (X : FinRV Ω R) (t : R) : R := ℙ[X ≤ᵣ t // P] - -variable {P : Findist R Ω} {X Y : FinRV Ω R} {t t₁ t₂ : R} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {V : Type} [LinearOrder V] +def cdf (P : Findist W Ω) (X : FinRV Ω V) (t : V) : W := ℙ[X ≤ᵣ t // P] end CDF @@ -338,19 +339,19 @@ Main results section Expectation_properties -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] (P : Findist R Ω) (X Y Z: FinRV Ω R) (B : FinRV Ω Bool) +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] (P : Findist W Ω) (X Y Z: FinRV Ω W) (B : FinRV Ω Bool) /-- Standard expectation operator -/ -def expect : R := P.p ⬝ᵥ X +def expect : W := P.p ⬝ᵥ X /-- Default expectation operator -/ notation "𝔼[" X "//" P "]" => expect P X -theorem probability_eq_expect_indicator : ℙ[B // P] = 𝔼[(𝕀 ∘ B : FinRV Ω R) // P] := by simp only [expect, probability] +theorem probability_eq_expect_indicator : ℙ[B // P] = 𝔼[(𝕀 ∘ B : FinRV Ω W) // P] := by simp only [expect, probability] /-- Conditional expectation operator -/ -def expectCond : R := 𝔼[ X * (𝕀 ∘ B) // P] / ℙ[ B // P] +def expectCond : W := 𝔼[ X * (𝕀 ∘ B) // P] / ℙ[ B // P] /-- Conditional expectation operator -/ notation "𝔼[" X "|" B "//" P "]" => expectCond P X B @@ -358,20 +359,20 @@ notation "𝔼[" X "|" B "//" P "]" => expectCond P X B variable {k : ℕ} (L : FinRV Ω (Fin k)) /-- Expectation conditioned on a random variable. It creates a random variable -/ -def expectCondRV : Ω → R := fun i ↦ 𝔼[ X | L =ᵣ (L i) // P ] +def expectCondRV : Ω → W := fun i ↦ 𝔼[ X | L =ᵣ (L i) // P ] /-- Expectation conditioned on a random variable. It creates a random variable -/ notation "𝔼[" X "|ᵣ" L "//" P "]" => expectCondRV P X L --- some basic properties -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} {X Y Z: FinRV Ω R} {B : FinRV Ω Bool} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist W Ω} {X Y Z: FinRV Ω W} {B : FinRV Ω Bool} theorem expect_congr (h : X = Y) : 𝔼[X // P] = 𝔼[Y // P] := congrArg (expect P) h theorem expect_mul_comm : 𝔼[X * Y // P] = 𝔼[Y * X // P] := expect_congr (mul_comm X Y) -variable {c : R} {p : Ω → R} +variable {c : W} {p : Ω → W} theorem expect_const : 𝔼[(fun _ ↦ c) // P] = c := by rw [const_eq_smul_one,expect, dotProduct_smul,smul_eq_mul,dotProduct_comm,P.sum_eq_one,mul_one] @@ -383,12 +384,12 @@ theorem expect_smul : 𝔼[c • X // P] = c * 𝔼[X // P] := by rw [expect, ex theorem expect_const_mul : 𝔼[(fun _ ↦ c) * X // P] = c * 𝔼[X // P] := by rw [const_mul_eq_smul, expect_smul] -variable {k : ℕ} {g : Fin k → R} {L : FinRV Ω (Fin k)} +variable {k : ℕ} {g : Fin k → W} {L : FinRV Ω (Fin k)} -theorem expect_indicatorEq (i) : 𝔼[(L =ᵢ i : FinRV Ω R) // P] = 𝔼[(𝕀 ∘ (L =ᵣ i) : FinRV Ω R) // P] := by rw [indicator_comp_eq_indicatorEq] +theorem expect_indicatorEq (i) : 𝔼[(L =ᵢ i : FinRV Ω W) // P] = 𝔼[(𝕀 ∘ (L =ᵣ i) : FinRV Ω W) // P] := by rw [indicator_comp_eq_indicatorEq] /-- Additivity of expectation --/ -theorem expect_sum {m : ℕ} (Xs : Fin m → FinRV Ω R) : +theorem expect_sum {m : ℕ} (Xs : Fin m → FinRV Ω W) : 𝔼[∑ i : Fin m, Xs i // P] = ∑ i : Fin m, 𝔼[Xs i // P] := dotProduct_sum P.p Finset.univ Xs theorem expect_add : 𝔼[X + Y // P] = 𝔼[X // P] + 𝔼[Y // P] := dotProduct_add P.p X Y @@ -426,7 +427,7 @@ section Probability_properties namespace FinRV theorem indicator_mono {Ω : Type} [Nonempty Ω] {A B : FinRV Ω Bool} - (h : ∀ ω, A ω → B ω) : (𝕀∘A : FinRV Ω R) ≤ (𝕀∘B) := by + (h : ∀ ω, A ω → B ω) : (𝕀∘A : FinRV Ω W) ≤ (𝕀∘B) := by intro ω specialize h ω by_cases h1 : A ω diff --git a/MDPLib/Probability/Prelude.lean b/MDPLib/Probability/Prelude.lean index 3cfc38f..476db21 100644 --- a/MDPLib/Probability/Prelude.lean +++ b/MDPLib/Probability/Prelude.lean @@ -7,23 +7,23 @@ import Mathlib.Logic.Function.Defs -- The scalar type used throughout the library: any linear ordered field. -- Instantiate at `ℚ` for computable results and at `ℝ` for the standard theory. -- The whole class stack is carried uniformly; Lean auto-includes every instance binder --- whenever `R` appears, so the `unusedSectionVars` linter is off in the numeric files. +-- whenever `W` appears, so the `unusedSectionVars` linter is off in the numeric files. set_option linter.unusedSectionVars false -variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R] - [CharZero R] [Archimedean R] +variable {W : Type} [Field W] [LinearOrder W] [IsStrictOrderedRing W] + [CharZero W] [Archimedean W] /-- states that p is a valid probability value -/ @[simp] -abbrev IsProb (p : R) : Prop := 0 ≤ p ∧ p ≤ 1 +abbrev IsProb (p : W) : Prop := 0 ≤ p ∧ p ≤ 1 ----------------- Section: Basic Probability ----------------------------------------------- namespace IsProb -variable {p x y : R} +variable {p x y : W} @[simp] theorem one_sub ( hp : IsProb p) : IsProb (1-p) := by @@ -64,7 +64,7 @@ section dotProduct namespace Matrix variable {Ω : Type*} [Fintype Ω] -variable {x y z : Ω → R} {c : R} +variable {x y z : Ω → W} {c : W} theorem dotProduct_mul_rotate : x ⬝ᵥ (y * z) = z ⬝ᵥ (x * y) := by @@ -78,7 +78,7 @@ theorem dotProduct_mul_comm : x ⬝ᵥ (y * z) = x ⬝ᵥ (z * y) := congrArg (x #check smul_eq_mul #check List.map_inj.mp rfl -theorem _root_.const_mul_eq_smul {X : Ω → R} : (fun _ ↦ c) * X = c • X := rfl +theorem _root_.const_mul_eq_smul {X : Ω → W} : (fun _ ↦ c) * X = c • X := rfl -- TODO(mathlib): a literal alias of Mathlib's `dotProduct_smul`; consider dropping it -- and using the Mathlib name at call sites. @@ -93,10 +93,10 @@ theorem mul_eq_zero_of_dotProduct_eq_zero (hx : 0 ≤ x) (hy : 0 ≤ y) : x ⬝ simp_all [dotProduct] exact (Fintype.sum_eq_zero_iff_of_nonneg this).mp h -theorem _root_.abs_mul_of_nonneg {a b : R} (h : 0 ≤ a) : |a * b| = a * |b| := by +theorem _root_.abs_mul_of_nonneg {a b : W} (h : 0 ≤ a) : |a * b| = a * |b| := by rw [abs_mul, abs_of_nonneg h] -theorem abs_dotProduct_le_dotProduct_abs (p x : Ω → R) (hp : ∀ i, 0 ≤ p i) : |p ⬝ᵥ x| ≤ p ⬝ᵥ fun i => |x i| := by +theorem abs_dotProduct_le_dotProduct_abs (p x : Ω → W) (hp : ∀ i, 0 ≤ p i) : |p ⬝ᵥ x| ≤ p ⬝ᵥ fun i => |x i| := by calc |∑ i : Ω, p i * x i| ≤ ∑ i, |p i * x i| := Finset.abs_sum_le_sum_abs (fun i ↦ p i * x i) Finset.univ _ = ∑ i, p i * |x i| := Finset.sum_congr rfl (fun i _ => abs_mul_of_nonneg (hp i)) @@ -105,17 +105,17 @@ theorem abs_dotProduct_le_dotProduct_abs (p x : Ω → R) (hp : ∀ i, 0 ≤ p i -- NOTE(mathlib): general Jensen is now available as `Findist.exp_convexOn_le` -- (`MDPLib/Probability/Convexity.lean`), for any convex `f` and any distribution. This lemma -- does NOT follow from it directly: Mathlib has no `convexOn_abs` (zero occurrences repo-wide), --- so folding it in would first require proving `ConvexOn R Set.univ abs`. Keep it as is. -theorem abs_dotProduct_le_dotProduct_abs_uniform (x : Fin n → R) (hn : 0 < n) : - |(fun _ : Fin n => (1 : R) / n) ⬝ᵥ x| ≤ (fun _ : Fin n => (1 : R) / n) ⬝ᵥ fun i => |x i| := by - have hpos : 0 < (n : R) := by exact_mod_cast hn - have hnonneg : 0 ≤ (1 : R) / n := by +-- so folding it in would first require proving `ConvexOn W Set.univ abs`. Keep it as is. +theorem abs_dotProduct_le_dotProduct_abs_uniform (x : Fin n → W) (hn : 0 < n) : + |(fun _ : Fin n => (1 : W) / n) ⬝ᵥ x| ≤ (fun _ : Fin n => (1 : W) / n) ⬝ᵥ fun i => |x i| := by + have hpos : 0 < (n : W) := by exact_mod_cast hn + have hnonneg : 0 ≤ (1 : W) / n := by have := inv_pos.mpr hpos simp - have hp : ∀ i : Fin n, 0 ≤ (1 : R) / n := fun _ => hnonneg + have hp : ∀ i : Fin n, 0 ≤ (1 : W) / n := fun _ => hnonneg simpa using abs_dotProduct_le_dotProduct_abs - (p := fun _ : Fin n => (1 : R) / n) + (p := fun _ : Fin n => (1 : W) / n) (x := x) (hp := hp) diff --git a/MDPLib/Probability/Quantile.lean b/MDPLib/Probability/Quantile.lean index 3418f35..83511ad 100644 --- a/MDPLib/Probability/Quantile.lean +++ b/MDPLib/Probability/Quantile.lean @@ -4,8 +4,8 @@ import Mathlib.Data.Fin.VecNotation set_option linter.unusedSectionVars false -variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R] - [CharZero R] [Archimedean R] +variable {W : Type} [Field W] [LinearOrder W] [IsStrictOrderedRing W] + [CharZero W] [Archimedean W] -- TODO(naming): Mathlib states order lemmas in the `≤` / `<` direction and derives the `≥` @@ -21,7 +21,8 @@ section Definition --def UnitI := {α : ℚ // 0 ≤ α ∧ α ≤ 1} -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] (P : Findist R Ω) (X Y : FinRV Ω R) (α : R) (q v : R) +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {V : Type} [LinearOrder V] +variable (P : Findist W Ω) (X Y : FinRV Ω V) (α : W) (q v : V) /-- Proof the `q` is an `α`-quantile of `X` --/ def IsQuantile : Prop := ℙ[X ≤ᵣ q // P ] ≥ α ∧ ℙ[X ≥ᵣ q // P] ≥ 1 - α @@ -30,10 +31,10 @@ def IsQuantile : Prop := ℙ[X ≤ᵣ q // P ] ≥ α ∧ ℙ[X ≥ᵣ q // P] def IsQuantileLower : Prop := ℙ[X ≥ᵣ q // P] ≥ 1 - α /-- Set of quantiles at a level `α` --/ -def quantile : Set R := {q | IsQuantile P X α q} +def quantile : Set V := {q | IsQuantile P X α q} /-- Set of lower bounds on a quantile at `α` -/ -def quantileLower : Set R := {q | IsQuantileLower P X α q} +def quantileLower : Set V := {q | IsQuantileLower P X α q} /-- Value `q` is maximum quantile at `α` of `X` and probability `P` -/ def IsGreatestQuantile : Prop := IsGreatest (quantile P X α) q @@ -41,9 +42,35 @@ def IsGreatestQuantile : Prop := IsGreatest (quantile P X α) q /-- Value `q` is minimum quantile at `α` of `X` and probability `P` -/ def IsLeastQuantile : Prop := IsLeast (quantile P X α) q + +@[to_dual (dont_translate := W)] +def aboveQuantileSet (P : Findist W Ω) (X : FinRV Ω V) (α : Set.Ico (0:W) 1) : Finset V := + let 𝓧 := X.quarks + 𝓧.filter (fun t ↦ ℙ[X <ᵣ t // P] ≤ α.val) + +@[to_dual (dont_translate := W)] +theorem aboveQuantileSet_nonempty (P : Findist W Ω) (X : FinRV Ω V) (α : Set.Ico (0:W) 1) : + (aboveQuantileSet (Ω := Ω) P X α).Nonempty := by + apply Finset.filter_nonempty_iff.mpr + use X.minQuark + constructor + · exact minQuark_mem_quarks + · have h : ℙ[X <ᵣ X.minQuark // P] = 0 := probability_lt_minQuark + rewrite [h] + exact α.2.1 + +/-- Computes the maximum quantile value -/ +def maxQuantile (P : Findist W Ω) (X : FinRV Ω V) (α : Set.Ico (0:W) 1) : V := + let 𝓧 := X.quarks + let 𝓢 := 𝓧.filter (fun t ↦ ℙ[X <ᵣ t // P] ≤ α.val) + have h : 𝓢.Nonempty := aboveQuantileSet_nonempty P X α + 𝓢.max' h + + end Definition -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} {X Y : FinRV Ω R} {α : R} {q v : R} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {V : Type} [LinearOrder V] +variable {P : Findist W Ω} {X Y : FinRV Ω V} {α : W} {q v : V} theorem le_probability_leq_of_mem_quantile : q ∈ quantile P X α → ℙ[X ≤ᵣ q // P ] ≥ α := by simp_all [quantile, IsQuantile] @@ -96,6 +123,9 @@ theorem isCofinalFor_quantileLower_of_le (hle : X ≤ Y) : IsCofinalFor (quantil section Negation +-- negates the values, so they are in `W` +variable {X : FinRV Ω W} {q : W} + theorem isQuantile_neg_iff : (IsQuantile P X α q) ↔ (IsQuantile P (-X) (1-α) (-q)) := by rw [IsQuantile, IsQuantile, probability_geq_eq_neg_leq_neg,probability_leq_eq_neg_geq_neg] have hα : 1-(1-α) = α := by ring @@ -122,7 +152,7 @@ end UpperLowerBounds section Transformations -variable {f : R → R} +variable {f : V → V} -- the reverse implications of the following results do not hold theorem mem_quantile_comp_of_monotone (hm : Monotone f) : q ∈ quantile P X α → (f q) ∈ quantile P (f ∘ X) α := by @@ -165,7 +195,9 @@ theorem isCoinitialFor_quantile_comp_image_of_monotone (hm : Monotone f) : IsCoi end Transformations -variable {c : R} +-- adds a constant to the values, so they are in `W` +variable {c : W} {X : FinRV Ω W} {q : W} + theorem mem_quantileLower_add_const_iff : q ∈ quantileLower P X α ↔ (q+c) ∈ quantileLower P (X+c•1) α := by constructor diff --git a/MDPLib/Risk/CVaR.lean b/MDPLib/Risk/CVaR.lean index 4cedf97..28aa191 100644 --- a/MDPLib/Risk/CVaR.lean +++ b/MDPLib/Risk/CVaR.lean @@ -9,7 +9,7 @@ the top of `MDPLib/Probability/Defs.lean` for why measure theory is not usable h * There is **no discrete Markov inequality in Mathlib**. `mul_meas_ge_le_lintegral` (`MeasureTheory/Integral/Lebesgue/Markov.lean:52`) is `ℝ≥0∞`/measure-valued and noncomputable. - A `Finset` version over `R` must be hand-rolled; the ingredients are + A `Finset` version over `W` must be hand-rolled; the ingredients are `Finset.sum_le_sum_of_subset_of_nonneg` and `Finset.card_nsmul_le_sum` (`Mathlib/Algebra/Order/BigOperators/Group/Finset.lean:169,291`) applied over a `Finset.filter`. diff --git a/MDPLib/Risk/VaR.lean b/MDPLib/Risk/VaR.lean index 43bbd07..6c22f72 100644 --- a/MDPLib/Risk/VaR.lean +++ b/MDPLib/Risk/VaR.lean @@ -4,29 +4,31 @@ import Mathlib.Data.Set.Operations set_option linter.unusedSectionVars false -variable {R : Type} [Field R] [LinearOrder R] [IsStrictOrderedRing R] - [CharZero R] [Archimedean R] +variable {W : Type} [Field W] [LinearOrder W] [IsStrictOrderedRing W] + [CharZero W] [Archimedean W] namespace Risk open Findist FinRV Statistic -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] -variable {P : Findist R Ω} {X Y : FinRV Ω R} {t t₁ t₂ : R} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {V : Type} [LinearOrder V] +variable {P : Findist W Ω} {X Y : FinRV Ω V} {t t₁ t₂ : V} -def IsRiskLevel (α : R) : Prop := 0 ≤ α ∧ α < 1 +def IsRiskLevel (α : W) : Prop := 0 ≤ α ∧ α < 1 -def RiskLevel (R : Type) [Field R] [LinearOrder R] [IsStrictOrderedRing R] := { α : R // IsRiskLevel α} +def RiskLevel (W : Type) [Field W] [LinearOrder W] [IsStrictOrderedRing W] := { α : W // IsRiskLevel α} --instance instCoeRiskUnit : Coe RiskLevel UnitI where -- coe := fun ⟨v,c⟩ => ⟨v, ⟨c.1, le_of_lt c.2⟩ ⟩ -def finVaRSet (P : Findist R Ω) (X : FinRV Ω R) (α : RiskLevel R) : Finset R := +-- possibly duplicated in a quantile definition +def finVaRSet (P : Findist W Ω) (X : FinRV Ω V) (α : RiskLevel W) : Finset V := let 𝓧 := X.quarks 𝓧.filter (fun t ↦ ℙ[X <ᵣ t // P] ≤ α.val) -theorem finVaRSet_nonempty (P : Findist R Ω) (X : FinRV Ω R) (α : RiskLevel R) : (finVaRSet (Ω := Ω) P X α).Nonempty := by +-- possibly duplicated in a quantile definition +theorem finVaRSet_nonempty (P : Findist W Ω) (X : FinRV Ω V) (α : RiskLevel W) : (finVaRSet (Ω := Ω) P X α).Nonempty := by apply Finset.filter_nonempty_iff.mpr use X.minQuark constructor @@ -37,13 +39,13 @@ theorem finVaRSet_nonempty (P : Findist R Ω) (X : FinRV Ω R) (α : RiskLevel R /-- Value-at-Risk of X at level α: VaR_α(X) = min { t ∈ X(Ω) | P[X ≤ t] ≥ α }. If we assume 0 ≤ α < 1, then the "else 0" branch is never used. -/ -def finVaR (P : Findist R Ω) (X : FinRV Ω R) (α : RiskLevel R) : R := +def finVaR (P : Findist W Ω) (X : FinRV Ω V) (α : RiskLevel W) : V := let 𝓧 := X.quarks let 𝓢 := 𝓧.filter (fun t ↦ ℙ[X <ᵣ t // P] ≤ α.val) have h : 𝓢.Nonempty := finVaRSet_nonempty P X α 𝓢.max' h -variable {α : RiskLevel R} +variable {α : RiskLevel W} theorem finVaR_spec : ℙ[X <ᵣ (finVaR P X α) // P] ≤ α.val ∧ α.val < ℙ[X ≤ᵣ (finVaR P X α) // P] := by @@ -64,7 +66,8 @@ theorem finVaR_spec : ℙ[X <ᵣ (finVaR P X α) // P] ≤ α.val ∧ α.val < notation "VaR[" X "//" P ", " α "]" => finVaR P X α -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] (P : Findist R Ω) (X Y : FinRV Ω R) (α : RiskLevel R) (q v : R) +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {V : Type} [LinearOrder V] +variable (P : Findist W Ω) (X Y : FinRV Ω V) (α : RiskLevel W) (q v : V) /-- Value `v` is the Value at Risk at `α` of `X` and probability `P` -/ def IsVaRQuantile : Prop := IsGreatest (quantile P X α.val) v @@ -72,7 +75,8 @@ def IsVaRQuantile : Prop := IsGreatest (quantile P X α.val) v /-- A simpler, equivalent definition of Value at Risk -/ def IsVaR : Prop := IsGreatest (quantileLower P X α.val) v -variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {P : Findist R Ω} {X Y : FinRV Ω R} {α : RiskLevel R} {q v q₁ q₂ : R} +variable {Ω : Type} [FinEnum Ω] [Nonempty Ω] {V : Type} [LinearOrder V] +variable {P : Findist W Ω} {X Y : FinRV Ω V} {α : RiskLevel W} {q v q₁ q₂ : V} theorem isVaR_iff : IsVaR P X α v ↔ (ℙ[X <ᵣ v // P] ≤ α.val ∧ α.val < ℙ[X ≤ᵣ v // P]) := by constructor @@ -82,12 +86,13 @@ theorem isVaR_iff : IsVaR P X α v ↔ (ℙ[X <ᵣ v // P] ≤ α.val ∧ α.val simp_all [IsVaR,IsGreatest,quantileLower,IsQuantileLower,probability_ge_eq_one_sub] linarith · by_contra! hc - obtain ⟨q,hq⟩ := exists_probability_leq_eq_probability_lt P X v + have hlt : v < X.maxQuark := lt_maxQuark_of_probability_leq_lt_one (lt_of_le_of_lt hc (Set.Ico.coe_lt_one α)) + obtain ⟨q, hqv, hqp, -⟩ := exists_probability_leq_eq_probability_lt_of_lt_maxQuark P X v hlt have h3 : q ∈ quantileLower P X α.val := by - rw [hq.2,probability_lt_eq_one_sub] at hc + rw [hqp,probability_lt_eq_one_sub] at hc suffices ℙ[X≥ᵣq//P] ≥ 1 - α.val from this linarith - exact not_lt_of_ge (h.2 h3) hq.1 + exact not_lt_of_ge (h.2 h3) hqv · intro h constructor · exact mem_quantileLower_of_probability_lt h.1 @@ -151,25 +156,12 @@ theorem isVaRQuantile_iff : IsVaRQuantile P X α v ↔ (ℙ[X <ᵣ v // P] ≤ section VaR_properties -variable {P : Findist R Ω} {X Y : FinRV Ω R} {q q₁ v₁ v₂ c : R} {α : RiskLevel R} {f : R → R} +variable {P : Findist W Ω} {X Y : FinRV Ω V} {q q₁ v₁ v₂ : V} {α : RiskLevel W} {f : V → V} + theorem IsVaR.le_of_le : X ≤ Y → IsVaR P X α v₁ → IsVaR P Y α v₂ → v₁ ≤ v₂ := fun hle hv1 hv2 => upperBounds_mono_of_isCofinalFor (isCofinalFor_quantileLower_of_le hle) hv2.2 hv1.1 --- TODO(mathlib): literal alias of `add_left_strictMono` -- use the Mathlib name at call sites. -theorem const_monotone_univ : StrictMono (fun x ↦ x + c) := add_left_strictMono - -theorem IsVaR.add_const : IsVaR P X α v → IsVaR P (X+c•1) α (v+c) := by - intro h - rw [IsVaR,quantileLower_add_const_eq_image] - exact MonotoneOn.map_isGreatest (Monotone.monotoneOn add_left_mono - (quantileLower P X α.val)) h - -theorem finVaR_add_const : VaR[X + c•1 // P, α] = VaR[X // P, α] + c := by - have h1 : IsVaR P (X + c•1) α (VaR[X + c•1 // P, α]) := isVaR_finVaR - have h2 : IsVaR P (X + c•1) α (VaR[X // P, α] + c) := IsVaR.add_const isVaR_finVaR - exact le_antisymm (h2.2 h1.1) (h1.2 h2.1) - /-- If `f` is strictly monotone then `f(VaR[X])` is the VaR of `f∘X`. -/ theorem IsVaR.comp_of_strictMono (hm : StrictMono f) (hv : IsVaR P X α v) : IsVaR P (f ∘ X) α (f v) := by rw [isVaR_iff] @@ -184,14 +176,36 @@ theorem finVaR_comp_of_strictMono (hm : StrictMono f) : VaR[f ∘ X // P, α] = have h2 : IsVaR P (f ∘ X) α (f (VaR[X // P, α])) := IsVaR.comp_of_strictMono hm isVaR_finVaR exact le_antisymm (h2.2 h1.1) (h1.2 h2.1) +section CashInvariance + +-- adds or multiplies constants to the values, so they are in `W` +variable {X : FinRV Ω W} {v c : W} + +-- TODO(mathlib): literal alias of `add_left_strictMono` -- use the Mathlib name at call sites. +theorem const_monotone_univ : StrictMono (fun x ↦ x + c) := add_left_strictMono + +theorem IsVaR.add_const : IsVaR P X α v → IsVaR P (X+c•1) α (v+c) := by + intro h + rw [IsVaR,quantileLower_add_const_eq_image] + exact MonotoneOn.map_isGreatest (Monotone.monotoneOn add_left_mono + (quantileLower P X α.val)) h + +theorem finVaR_add_const : VaR[X + c•1 // P, α] = VaR[X // P, α] + c := by + have h1 : IsVaR P (X + c•1) α (VaR[X + c•1 // P, α]) := isVaR_finVaR + have h2 : IsVaR P (X + c•1) α (VaR[X // P, α] + c) := IsVaR.add_const isVaR_finVaR + exact le_antisymm (h2.2 h1.1) (h1.2 h2.1) + -- TODO(naming): the statement writes `finVaR P (fun ω => c * X ω)` where the surrounding -- lemmas use the `c • X` / notation form; `finVaR_const_mul` should be stated the same way -- as its siblings so the names line up with the statements. theorem finVaR_const_mul (hc : c > 0) : finVaR P (fun ω => c * X ω) α = c * finVaR P X α := finVaR_comp_of_strictMono (fun _ _ hab => mul_lt_mul_of_pos_left hab hc) +end CashInvariance + end VaR_properties + end Risk diff --git a/README.md b/README.md index 4c7c7f1..6c818f5 100644 --- a/README.md +++ b/README.md @@ -3,157 +3,146 @@ [![CI](https://github.com/formalproofs/MDPLib/actions/workflows/ci.yml/badge.svg)](https://github.com/formalproofs/MDPLib/actions/workflows/ci.yml) [![Documentation](https://img.shields.io/badge/docs-online-blue)](https://formalproofs.github.io/MDPLib/docs/) -**Documentation:** the [API documentation](https://formalproofs.github.io/MDPLib/docs/) -and the [companion paper](https://formalproofs.github.io/MDPLib/main.pdf) are built by CI and -published to [GitHub Pages](https://formalproofs.github.io/MDPLib/) on every push to `main`. +Verified Lean algorithms for tabular MDPs, with two goals: -Verified Lean algorithms for solving tabular MDPs and proving their properties. The focus of this project is on two main goals: - -1. Basic algorithms that can solve robust and risk-averse MDPs of moderate size. - -2. Proofs of correctness of algorithms and fundamental MDP properties which can be used independently to prove structural results, such as the optimality of certain policy class. +1. Algorithms that solve robust and risk-averse MDPs of moderate size. +2. Proofs of correctness and of fundamental MDP properties, usable on their own for structural + results such as the optimality of a policy class. +The [API documentation](https://formalproofs.github.io/MDPLib/docs/) and the +[companion paper](https://formalproofs.github.io/MDPLib/main.pdf) are published by CI on every +push to `main`. ## Library Contents -The main results formalized so far. Everything is developed for *finite* sample spaces -(`[FinEnum Ω]`) over an arbitrary linear ordered field `R` -(`[Field R] [LinearOrder R] [IsStrictOrderedRing R] [CharZero R] [Archimedean R]`), so the -statements are free of measurability side conditions. Instantiate at `ℚ` — as -[`MDPLibTest.lean`](MDPLibTest.lean) does — and every definition is computable and executable; -instantiate at `ℝ` for the standard theory, where the definitions remain well-formed but -`noncomputable` (`Real.instField` and the classical `DecidableLE ℝ` are noncomputable, so -`VaR[X // P, α]` cannot be `#eval`'d over `ℝ`). - - -### Relationship to Mathlib's probability +Sample spaces are finite (`[FinEnum Ω]`), so there are no measurability side conditions. Two +types appear: -Mathlib's measure-theoretic probability (`Measure`, `PMF`, `∫`) is not used: it is -`noncomputable` and valued in `ℝ≥0∞` or `ℝ`, so it can neither be evaluated at `ℚ` nor stated -over a general `R`, and it has no quantiles or VaR. Mathlib's scalar-generic convexity API -(`Finset.centerMass`, `StdSimplex`) is reused instead. +- `W`: probabilities, and values that are averaged with them (expectation, CVaR). Any linear + ordered field — `ℚ` makes every definition computable (see [`MDPLibTest.lean`](MDPLibTest.lean)), + `ℝ` gives the standard theory. +- `V`: values that are only compared (events, `ℙ`, CDF, quantiles, VaR). Any linear order, e.g. + `W`, `ℕ`, `ℤ`. +They are separate so that order-only results apply to any ordered values, and so that +`@[to_dual (dont_translate := W)]` can derive mirror-image results by reversing the order on +values without reversing it on probabilities. -Legend: ✅ proof complete  ·  🚧 statement final, proof still depends on a `sorry` -(check with `#print axioms`). +Mathlib's measure-theoretic probability is not used: it is `noncomputable`, fixed to `ℝ`/`ℝ≥0∞`, +and has no quantiles or VaR. Its scalar-generic convexity API (`Finset.centerMass`, +`StdSimplex`) is reused instead. ### Probability foundations [`MDPLib/Probability/Defs.lean`](MDPLib/Probability/Defs.lean), [`MDPLib/Probability/Prelude.lean`](MDPLib/Probability/Prelude.lean) -| | Result | Lean name | -|---|---|---| -| ✅ | Finite distribution on `Ω` (nonneg weights summing to one), Dirac distribution | [`Findist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist), [`Findist.Δ`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.Δ), [`Findist.dirac`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.dirac) | -| ✅ | A distribution forces its sample space to be nonempty | [`Findist.nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.nonempty) | -| ✅ | Random variables as bare functions `Ω → ρ`; events as `Ω → Bool` with Mathlib's Boolean algebra (`⊔`, `⊓`) | [`FinRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV), [`FinRV.sup_eq_or`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.sup_eq_or), [`FinRV.inf_eq_and`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.inf_eq_and) | -| ✅ | Comparison events `X ≤ᵣ t`, `X <ᵣ t`, `X ≥ᵣ t`, `X >ᵣ t`, `X =ᵣ y` and the indicator `𝕀` | [`FinRV.leq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.leq), [`FinRV.lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.lt), [`FinRV.geq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.geq), [`FinRV.gt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.gt), [`FinRV.eq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.eq), [`FinRV.indicator`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.indicator) | -| ✅ | Probability `ℙ[B // P]`, conditional probability `ℙ[B \| C // P]` | [`Findist.probability`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.probability), [`Findist.probabilityCond`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.probabilityCond) | -| ✅ | Expectation `𝔼[X // P]`, conditional expectation `𝔼[X \| B // P]` and the conditional-expectation random variable `𝔼[X \|ᵣ L // P]` | [`Findist.expect`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect), [`Findist.expectCond`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expectCond), [`Findist.expectCondRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expectCondRV) | -| ✅ | Probability as the expectation of an indicator | [`Findist.probability_eq_expect_indicator`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.probability_eq_expect_indicator) | -| ✅ | Decomposition of a random variable along a discrete label `X = ∑ᵢ X · 𝕀[L = i]` | [`FinRV.eq_sum_mul_indicatorEq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.eq_sum_mul_indicatorEq), [`Findist.expect_eq_sum_mul_indicatorEq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect_eq_sum_mul_indicatorEq) | -| ✅ | Convexity bounds for two-point mixtures; Jensen's inequality for `\|·\|` on the uniform distribution | [`IsProb.self_le_combo_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Prelude.html#IsProb.self_le_combo_of_le), [`IsProb.combo_le_self_of_ge`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Prelude.html#IsProb.combo_le_self_of_ge), [`Matrix.abs_dotProduct_le_dotProduct_abs_uniform`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Prelude.html#Matrix.abs_dotProduct_le_dotProduct_abs_uniform) | +| Result | Lean name | +|---|---| +| Finite distribution on `Ω` (nonneg weights summing to one), Dirac distribution | [`Findist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist), [`Findist.Δ`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.Δ), [`Findist.dirac`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.dirac) | +| A distribution forces its sample space to be nonempty | [`Findist.nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.nonempty) | +| Random variables as bare functions `Ω → V`; events as `Ω → Bool` with Mathlib's Boolean algebra (`⊔`, `⊓`) | [`FinRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV), [`FinRV.sup_eq_or`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.sup_eq_or), [`FinRV.inf_eq_and`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.inf_eq_and) | +| Comparison events `X ≤ᵣ t`, `X <ᵣ t`, `X ≥ᵣ t`, `X >ᵣ t`, `X =ᵣ y` and the indicator `𝕀` | [`FinRV.leq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.leq), [`FinRV.lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.lt), [`FinRV.geq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.geq), [`FinRV.gt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.gt), [`FinRV.eq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.eq), [`FinRV.indicator`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.indicator) | +| Probability `ℙ[B // P]`, conditional probability `ℙ[B \| C // P]` | [`Findist.probability`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.probability), [`Findist.probabilityCond`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.probabilityCond) | +| Expectation `𝔼[X // P]`, conditional expectation `𝔼[X \| B // P]` and the conditional-expectation random variable `𝔼[X \|ᵣ L // P]` | [`Findist.expect`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect), [`Findist.expectCond`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expectCond), [`Findist.expectCondRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expectCondRV) | +| Probability as the expectation of an indicator | [`Findist.probability_eq_expect_indicator`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.probability_eq_expect_indicator) | +| Decomposition of a random variable along a discrete label `X = ∑ᵢ X · 𝕀[L = i]` | [`FinRV.eq_sum_mul_indicatorEq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#FinRV.eq_sum_mul_indicatorEq), [`Findist.expect_eq_sum_mul_indicatorEq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect_eq_sum_mul_indicatorEq) | +| Convexity bounds for two-point mixtures; Jensen's inequality for `\|·\|` on the uniform distribution | [`IsProb.self_le_combo_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Prelude.html#IsProb.self_le_combo_of_le), [`IsProb.combo_le_self_of_ge`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Prelude.html#IsProb.combo_le_self_of_ge), [`Matrix.abs_dotProduct_le_dotProduct_abs_uniform`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Prelude.html#Matrix.abs_dotProduct_le_dotProduct_abs_uniform) | ### Expectation as a convex combination [`MDPLib/Probability/Convexity.lean`](MDPLib/Probability/Convexity.lean) -| | Result | Lean name | -|---|---|---| -| ✅ | `𝔼[X // P]` is Mathlib's `Finset.centerMass` at weights summing to one | [`Findist.expect_eq_centerMass`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_eq_centerMass) | -| ✅ | `minQuark X ≤ 𝔼[X] ≤ maxQuark X` | [`Findist.expect_ge_minQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_ge_minQuark), [`Findist.expect_le_maxQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_le_maxQuark) | -| ✅ | Jensen's inequality for an arbitrary convex / concave function | [`Findist.expect_convexOn_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_convexOn_le), [`Findist.expect_concaveOn_ge`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_concaveOn_ge) | +| Result | Lean name | +|---|---| +| `𝔼[X // P]` is Mathlib's `Finset.centerMass` at weights summing to one | [`Findist.expect_eq_centerMass`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_eq_centerMass) | +| `minQuark X ≤ 𝔼[X] ≤ maxQuark X` | [`Findist.expect_ge_minQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_ge_minQuark), [`Findist.expect_le_maxQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_le_maxQuark) | +| Jensen's inequality for an arbitrary convex / concave function | [`Findist.expect_convexOn_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_convexOn_le), [`Findist.expect_concaveOn_ge`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Convexity.html#Findist.expect_concaveOn_ge) | ### Bridge to Mathlib's standard simplex [`MDPLib/Probability/StdSimplex.lean`](MDPLib/Probability/StdSimplex.lean) -| | Result | Lean name | -|---|---|---| -| ✅ | A `Findist` as a point of `Convexity.StdSimplex` (`noncomputable`; proof-layer only) | [`Findist.toStdSimplex`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/StdSimplex.html#Findist.toStdSimplex) | -| ✅ | Mathlib's indexed convex combination is this library's expectation | [`Findist.toStdSimplex_iConvexComb`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/StdSimplex.html#Findist.toStdSimplex_iConvexComb) | -| ✅ | `Findist.dirac` is `StdSimplex.single`; the bridge is injective | [`Findist.toStdSimplex_dirac`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/StdSimplex.html#Findist.toStdSimplex_dirac), [`Findist.toStdSimplex_injective`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/StdSimplex.html#Findist.toStdSimplex_injective) | +| Result | Lean name | +|---|---| +| A `Findist` as a point of `Convexity.StdSimplex` (`noncomputable`; proof-layer only) | [`Findist.toStdSimplex`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/StdSimplex.html#Findist.toStdSimplex) | +| Mathlib's indexed convex combination is this library's expectation | [`Findist.toStdSimplex_iConvexComb`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/StdSimplex.html#Findist.toStdSimplex_iConvexComb) | +| `Findist.dirac` is `StdSimplex.single`; the bridge is injective | [`Findist.toStdSimplex_dirac`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/StdSimplex.html#Findist.toStdSimplex_dirac), [`Findist.toStdSimplex_injective`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/StdSimplex.html#Findist.toStdSimplex_injective) | ### Probability: basic properties [`MDPLib/Probability/Basic.lean`](MDPLib/Probability/Basic.lean) -| | Result | Lean name | -|---|---|---| -| ✅ | `ℙ` takes values in `[0,1]` | [`Findist.probability_nonneg`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_nonneg), [`Findist.probability_le_one`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_le_one), [`Findist.isProb_probability`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.isProb_probability) | -| ✅ | Linearity, homogeneity and monotonicity of expectation | [`Findist.expect_sum`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect_sum), [`Findist.expect_smul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect_smul), [`Findist.expect_mono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect_mono) | -| ✅ | Complement rules `ℙ[B] + ℙ[¬B] = 1`, and the `≤`/`>` and `<`/`≥` pairs | [`Findist.probability_add_probability_not`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_add_probability_not), [`Findist.probability_leq_add_probability_gt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_leq_add_probability_gt), [`Findist.probability_lt_add_probability_geq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_lt_add_probability_geq) | -| ✅ | Monotonicity of `ℙ[X ≤ t]` in both `X` and `t` (and the antitone versions) | [`Findist.probability_leq_mono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_leq_mono), [`Findist.probability_lt_mono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_lt_mono), [`Findist.probability_geq_anti`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_geq_anti), [`Findist.probability_gt_anti`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_gt_anti) | -| ✅ | Behaviour of events and probabilities under monotone / strictly monotone / antitone transformations of `X` | [`FinRV.leq_eq_comp_leq_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.leq_eq_comp_leq_of_strictMono), [`StrictMono.probability_leq_eq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#StrictMono.probability_leq_eq), [`StrictMono.probability_geq_eq`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#StrictMono.probability_geq_eq), … | -| ✅ | Cash (translation) invariance and negation duality of the comparison events | [`Findist.probability_leq_add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_leq_add_const), [`Findist.probability_leq_eq_neg_geq_neg`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_leq_eq_neg_geq_neg) | -| ✅ | CDF `cdf P X t = ℙ[X ≤ t]`; it is nondecreasing in `t` and antitone in `X` | [`Findist.cdf`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.cdf), [`Findist.cdf_mono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.cdf_mono), [`Findist.cdf_anti_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.cdf_anti_of_le) | -| ✅ | Law of the unconscious statistician | [`Findist.expect_comp_eq_sum`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_comp_eq_sum) | -| ✅ | Tower property (law of total expectation) | [`Findist.expect_expectCondRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_expectCondRV) | -| ✅ | Law of total probability | [`Findist.probability_eq_sum`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_eq_sum) | -| ✅ | Expectation equals the sum over the (finite) image of `X` | [`Findist.expect_eq_sum_probability_mul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_eq_sum_probability_mul), [`FinRV.sum_image_univ_eq_sum_fin`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.sum_image_univ_eq_sum_fin) | -| ✅ | Duplicate-free list of the values of a random variable, with index/value inverses | [`FinRV.imageList`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageList), [`FinRV.imageIdxOf`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageIdxOf), [`FinRV.getElem_imageIdxOf`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.getElem_imageIdxOf), [`FinRV.imageList_nodup`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageList_nodup) | -| ✅ | Invariance of probability and expectation under a permutation of the sample space | [`Findist.comp`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.comp), [`Findist.probability_comp_perm`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_comp_perm), [`Findist.expect_comp_perm`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_comp_perm) | -| ✅ | A `≤` event can be replaced by a strict `<` event at a larger threshold | [`Findist.exists_probability_leq_eq_probability_lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.exists_probability_leq_eq_probability_lt), [`Findist.exists_probability_leq_eq_probability_lt_of_lt_maxQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.exists_probability_leq_eq_probability_lt_of_lt_maxQuark) | +| Result | Lean name | +|---|---| +| `ℙ` takes values in `[0,1]` | [`Findist.probability_nonneg`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_nonneg), [`Findist.probability_le_one`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_le_one), [`Findist.isProb_probability`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.isProb_probability) | +| Linearity, homogeneity and monotonicity of expectation | [`Findist.expect_sum`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect_sum), [`Findist.expect_smul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect_smul), [`Findist.expect_mono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.expect_mono) | +| Complement rules `ℙ[B] + ℙ[¬B] = 1`, and the `≤`/`>` and `<`/`≥` pairs | [`Findist.probability_add_probability_not`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_add_probability_not), [`Findist.probability_le_gt_one`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_le_gt_one), [`Findist.probability_lt_ge_one`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_lt_ge_one) | +| Monotonicity of `ℙ[X ≤ t]` in both `X` and `t` (and the antitone versions) | [`Findist.probability_le_mono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_le_mono), [`Findist.probability_lt_mono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_lt_mono), [`Findist.probability_ge_anti`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_ge_anti), [`Findist.probability_gt_anti`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_gt_anti) | +| Behaviour of events and probabilities under monotone / strictly monotone / antitone transformations of `X` | [`FinRV.leq_eq_comp_leq_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.leq_eq_comp_leq_of_strictMono), [`StrictMono.probability_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#StrictMono.probability_le), [`StrictMono.probability_ge`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#StrictMono.probability_ge), … | +| Cash (translation) invariance and negation duality of the comparison events | [`Findist.probability_leq_add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_leq_add_const), [`Findist.probability_leq_eq_neg_geq_neg`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_leq_eq_neg_geq_neg) | +| CDF `cdf P X t = ℙ[X ≤ t]`; it is nondecreasing in `t` and antitone in `X` | [`Findist.cdf`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Defs.html#Findist.cdf), [`Findist.cdf_mono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.cdf_mono), [`Findist.cdf_anti_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.cdf_anti_of_le) | +| Law of the unconscious statistician | [`Findist.expect_comp_eq_sum`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_comp_eq_sum) | +| Tower property (law of total expectation) | [`Findist.expect_expectCondRV`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_expectCondRV) | +| Law of total probability | [`Findist.probability_eq_sum`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_eq_sum) | +| Expectation equals the sum over the (finite) image of `X` | [`Findist.expect_eq_sum_probability_mul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_eq_sum_probability_mul), [`FinRV.sum_image_univ_eq_sum_fin`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.sum_image_univ_eq_sum_fin) | +| Duplicate-free list of the values of a random variable, with index/value inverses | [`FinRV.imageList`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageList), [`FinRV.imageIdxOf`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageIdxOf), [`FinRV.getElem_imageIdxOf`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.getElem_imageIdxOf), [`FinRV.imageList_nodup`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#FinRV.imageList_nodup) | +| Invariance of probability and expectation under a permutation of the sample space | [`Findist.comp`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.comp), [`Findist.probability_comp_perm`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.probability_comp_perm), [`Findist.expect_comp_perm`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.expect_comp_perm) | +| A `≤` event can be replaced by a strict `<` event at a larger threshold | [`Findist.exists_probability_leq_eq_probability_lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.exists_probability_leq_eq_probability_lt), [`Findist.exists_probability_leq_eq_probability_lt_of_lt_maxQuark`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Basic.html#Findist.exists_probability_leq_eq_probability_lt_of_lt_maxQuark) | ### Quantiles [`MDPLib/Probability/Quantile.lean`](MDPLib/Probability/Quantile.lean) -| | Result | Lean name | -|---|---|---| -| ✅ | Quantile set `{q \| ℙ[X ≤ q] ≥ α ∧ ℙ[X ≥ q] ≥ 1-α}` and its one-sided (lower) relaxation | [`Statistic.quantile`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.quantile), [`Statistic.quantileLower`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.quantileLower), [`Statistic.IsQuantile`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.IsQuantile), [`Statistic.IsQuantileLower`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.IsQuantileLower) | -| ✅ | Equivalent characterizations of membership, including the strict form `ℙ[X < q] ≤ α` | [`Statistic.mem_quantile_iff`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_iff), [`Statistic.mem_quantileLower_iff_probability_lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantileLower_iff_probability_lt), [`Statistic.mem_quantile_of_probability_lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_of_probability_lt) | -| ✅ | Every quantile is a lower quantile | [`Statistic.quantile_subset_quantileLower`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.quantile_subset_quantileLower) | -| ✅ | Reflection: `q` is an `α`-quantile of `X` iff `-q` is a `(1-α)`-quantile of `-X` | [`Statistic.mem_quantile_neg_iff`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_neg_iff) | -| ✅ | Quantiles under monotone maps; equivalence for strictly monotone maps | [`Statistic.mem_quantile_comp_of_monotone`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_comp_of_monotone), [`Statistic.mem_quantile_comp_iff_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_comp_iff_of_strictMono), [`Statistic.mem_quantileLower_comp_iff_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantileLower_comp_iff_of_strictMono) | -| ✅ | Lower quantiles of `X ≤ Y` are cofinal — the basis for monotonicity of VaR | [`Statistic.isCofinalFor_quantileLower_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.isCofinalFor_quantileLower_of_le) | -| ✅ | Cash invariance of the lower-quantile set: `QuantileLower(X + c) = QuantileLower(X) + c` | [`Statistic.quantileLower_add_const_eq_image`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.quantileLower_add_const_eq_image) | -| 🚧 | The image `f '' quantile(X)` is cofinal/coinitial in `quantile(f∘X)` for monotone `f` | [`Statistic.isCofinalFor_quantile_comp_image_of_monotone`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.isCofinalFor_quantile_comp_image_of_monotone), [`Statistic.isCoinitialFor_quantile_comp_image_of_monotone`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.isCoinitialFor_quantile_comp_image_of_monotone) | +| Result | Lean name | +|---|---| +| Quantile set `{q \| ℙ[X ≤ q] ≥ α ∧ ℙ[X ≥ q] ≥ 1-α}` and its one-sided (lower) relaxation | [`Statistic.quantile`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.quantile), [`Statistic.quantileLower`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.quantileLower), [`Statistic.IsQuantile`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.IsQuantile), [`Statistic.IsQuantileLower`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.IsQuantileLower) | +| Equivalent characterizations of membership, including the strict form `ℙ[X < q] ≤ α` | [`Statistic.mem_quantile_iff`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_iff), [`Statistic.mem_quantileLower_iff_probability_lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantileLower_iff_probability_lt), [`Statistic.mem_quantile_of_probability_lt`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_of_probability_lt) | +| Every quantile is a lower quantile | [`Statistic.quantile_subset_quantileLower`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.quantile_subset_quantileLower) | +| Reflection: `q` is an `α`-quantile of `X` iff `-q` is a `(1-α)`-quantile of `-X` | [`Statistic.mem_quantile_neg_iff`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_neg_iff) | +| Quantiles under monotone maps; equivalence for strictly monotone maps | [`Statistic.mem_quantile_comp_of_monotone`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_comp_of_monotone), [`Statistic.mem_quantile_comp_iff_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantile_comp_iff_of_strictMono), [`Statistic.mem_quantileLower_comp_iff_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.mem_quantileLower_comp_iff_of_strictMono) | +| Lower quantiles of `X ≤ Y` are cofinal — the basis for monotonicity of VaR | [`Statistic.isCofinalFor_quantileLower_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.isCofinalFor_quantileLower_of_le) | +| Cash invariance of the lower-quantile set: `QuantileLower(X + c) = QuantileLower(X) + c` | [`Statistic.quantileLower_add_const_eq_image`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.quantileLower_add_const_eq_image) | +| The image `f '' quantile(X)` is cofinal/coinitial in `quantile(f∘X)` for monotone `f` (proof incomplete) | [`Statistic.isCofinalFor_quantile_comp_image_of_monotone`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.isCofinalFor_quantile_comp_image_of_monotone), [`Statistic.isCoinitialFor_quantile_comp_image_of_monotone`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Probability/Quantile.html#Statistic.isCoinitialFor_quantile_comp_image_of_monotone) | ### Value at Risk [`MDPLib/Risk/VaR.lean`](MDPLib/Risk/VaR.lean) -| | Result | Lean name | -|---|---|---| -| ✅ | Risk level `0 ≤ α < 1` | [`Risk.IsRiskLevel`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsRiskLevel), [`Risk.RiskLevel`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.RiskLevel) | -| ✅ | Non-constructive VaR: the greatest lower quantile (equivalently, the greatest quantile) | [`Risk.IsVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR), [`Risk.IsVaRQuantile`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaRQuantile) | -| ✅ | Characterization `IsVaR v ↔ ℙ[X < v] ≤ α < ℙ[X ≤ v]` | [`Risk.isVaR_iff`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaR_iff) | -| ✅ | Computable VaR `VaR[X // P, α]` as a max over the finite candidate set, which is nonempty | [`Risk.finVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR), [`Risk.finVaRSet`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaRSet), [`Risk.finVaRSet_nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaRSet_nonempty) | -| ✅ | VaR is monotone: `X ≤ Y` implies `VaR[X] ≤ VaR[Y]` | [`Risk.IsVaR.le_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.le_of_le) | -| ✅ | **Correctness of the computable VaR:** `IsVaR P X α (VaR[X // P, α])` | [`Risk.isVaR_finVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaR_finVaR) | -| ✅ | The two definitions (greatest quantile / greatest lower quantile) agree | [`Risk.isVaRQuantile_iff_isVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaRQuantile_iff_isVaR) | -| ✅ | The quantile set is nonempty | [`Risk.quantile_nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.quantile_nonempty) | -| ✅ | Translation (cash) invariance for the `Risk.IsVaR` predicate | [`Risk.IsVaR.add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.add_const) | -| ✅ | … and for the computable VaR: `VaR[X + c] = VaR[X] + c` | [`Risk.finVaR_add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_add_const) | -| ✅ | Strictly monotone transformations for the `Risk.IsVaR` predicate | [`Risk.IsVaR.comp_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.comp_of_strictMono) | -| ✅ | … and for the computable VaR: `VaR[f∘X] = f(VaR[X])` | [`Risk.finVaR_comp_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_comp_of_strictMono) | -| ✅ | Positive homogeneity: `VaR[c·X] = c·VaR[X]` for `c > 0` | [`Risk.finVaR_const_mul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_const_mul) | - -[`Main.lean`](Main.lean) contains an executable that reads distributions from a JSON -file, computes VaR with `computeVaR`, and checks it against reference values -(see [`test_var.json`](test_var.json)). `computeVaR` is standalone IO glue over -`Array ℚ` rather than the verified `Risk.finVaR`; it is -[`MDPLibTest.lean`](MDPLibTest.lean) that instantiates the library itself at `ℚ`. +| Result | Lean name | +|---|---| +| Risk level `0 ≤ α < 1` | [`Risk.IsRiskLevel`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsRiskLevel), [`Risk.RiskLevel`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.RiskLevel) | +| Non-constructive VaR: the greatest lower quantile (equivalently, the greatest quantile) | [`Risk.IsVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR), [`Risk.IsVaRQuantile`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaRQuantile) | +| Characterization `IsVaR v ↔ ℙ[X < v] ≤ α < ℙ[X ≤ v]` | [`Risk.isVaR_iff`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaR_iff) | +| Computable VaR `VaR[X // P, α]` as a max over the finite candidate set, which is nonempty | [`Risk.finVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR), [`Risk.finVaRSet`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaRSet), [`Risk.finVaRSet_nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaRSet_nonempty) | +| VaR is monotone: `X ≤ Y` implies `VaR[X] ≤ VaR[Y]` | [`Risk.IsVaR.le_of_le`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.le_of_le) | +| **Correctness of the computable VaR:** `IsVaR P X α (VaR[X // P, α])` | [`Risk.isVaR_finVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaR_finVaR) | +| The two definitions (greatest quantile / greatest lower quantile) agree | [`Risk.isVaRQuantile_iff_isVaR`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.isVaRQuantile_iff_isVaR) | +| The quantile set is nonempty | [`Risk.quantile_nonempty`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.quantile_nonempty) | +| Translation (cash) invariance for the `Risk.IsVaR` predicate | [`Risk.IsVaR.add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.add_const) | +| … and for the computable VaR: `VaR[X + c] = VaR[X] + c` | [`Risk.finVaR_add_const`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_add_const) | +| Strictly monotone transformations for the `Risk.IsVaR` predicate | [`Risk.IsVaR.comp_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.IsVaR.comp_of_strictMono) | +| … and for the computable VaR: `VaR[f∘X] = f(VaR[X])` | [`Risk.finVaR_comp_of_strictMono`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_comp_of_strictMono) | +| Positive homogeneity: `VaR[c·X] = c·VaR[X]` for `c > 0` | [`Risk.finVaR_const_mul`](https://formalproofs.github.io/MDPLib/docs/MDPLib/Risk/VaR.html#Risk.finVaR_const_mul) | + +[`Main.lean`](Main.lean) checks VaR on the distributions in [`test_var.json`](test_var.json) +using standalone code (`computeVaR`), not the verified `Risk.finVaR`. ### MDPs and histories [`MDPLib/MDP/Histories.lean`](MDPLib/MDP/Histories.lean) -| | Result | Lean name | -|----|---------------------------------------------------------------------------------------------|--------------------------------------------------------------------| -| ✅ | Tabular MDP with finite states, actions, transitions and rewards | [`MDP`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP) | -| ✅ | Histories `s₀ a₀ s₁ …`, their length, last state, prefixes, and the length-indexed subtype | [`Hist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#Hist), [`Hist.length`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#Hist.length), [`Hist.last`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#Hist.last), [`Hist.prefix`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#Hist.prefix), [`MDP.HistOfLength`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.HistOfLength) | -| ✅ | The count `S · (S·A)^t` and the explicit index maps `Fin (numHist t) ↔ HistOfLength t` | [`MDP.numHist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.numHist), [`MDP.idxToHist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.idxToHist), [`MDP.histToIdx`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.histToIdx) | -| 🚧 | … that those maps are mutually inverse, i.e. that the count is the cardinality | [`leftInverse_idxToHist_histToIdx`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#leftInverse_idxToHist_histToIdx), [`rightInverse_idxToHist_histToIdx`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#rightInverse_idxToHist_histToIdx), [`exists_init_of_length_eq_zero`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#exists_init_of_length_eq_zero), [`exists_foll_of_length_eq_succ`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#exists_foll_of_length_eq_succ) | -| ✅ | Embeddings `Hist × A × S ↪ Hist` and `S ↪ Hist` | [`tupleToHistEmbedding`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#tupleToHistEmbedding), [`stateToHistEmbedding`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#stateToHistEmbedding) | -| ✅ | The horizon-`t` history sets are exactly the histories of length `t`; `Fintype (M.HistOfLength t)` | [`mem_historiesHorizon`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#mem_historiesHorizon), [`length_eq_of_mem_historiesHorizon`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#length_eq_of_mem_historiesHorizon), [`MDP.historiesHorizonT`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.historiesHorizonT) | +| Result | Lean name | +|---------------------------------------------------------------------------------------------|--------------------------------------------------------------------| +| Tabular MDP with finite states, actions, transitions and rewards | [`MDP`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP) | +| Histories `s₀ a₀ s₁ …`, their length, last state, prefixes, and the length-indexed subtype | [`Hist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#Hist), [`Hist.length`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#Hist.length), [`Hist.last`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#Hist.last), [`Hist.prefix`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#Hist.prefix), [`MDP.HistOfLength`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.HistOfLength) | +| The count `S · (S·A)^t` and the explicit index maps `Fin (numHist t) ↔ HistOfLength t` | [`MDP.numHist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.numHist), [`MDP.idxToHist`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.idxToHist), [`MDP.histToIdx`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.histToIdx) | +| … that those maps are mutually inverse, i.e. that the count is the cardinality (proof incomplete) | [`leftInverse_idxToHist_histToIdx`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#leftInverse_idxToHist_histToIdx), [`rightInverse_idxToHist_histToIdx`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#rightInverse_idxToHist_histToIdx), [`exists_init_of_length_eq_zero`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#exists_init_of_length_eq_zero), [`exists_foll_of_length_eq_succ`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#exists_foll_of_length_eq_succ) | +| Embeddings `Hist × A × S ↪ Hist` and `S ↪ Hist` | [`tupleToHistEmbedding`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#tupleToHistEmbedding), [`stateToHistEmbedding`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#stateToHistEmbedding) | +| The horizon-`t` history sets are exactly the histories of length `t`; `Fintype (M.HistOfLength t)` | [`mem_historiesHorizon`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#mem_historiesHorizon), [`length_eq_of_mem_historiesHorizon`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#length_eq_of_mem_historiesHorizon), [`MDP.historiesHorizonT`](https://formalproofs.github.io/MDPLib/docs/MDPLib/MDP/Histories.html#MDP.historiesHorizonT) | -The `ℋ h t` family (histories extending `h` by `t` steps) is defined but its length -lemma `length_of_mem_histories` is still 🚧. - -[`MDPLib/Risk/CVaR.lean`](MDPLib/Risk/CVaR.lean) is an empty stub; it carries notes on which -Mathlib pieces are and are not available for Conditional Value at Risk. +The `ℋ h t` family is defined; its length lemma `length_of_mem_histories` is still unproven. +[`MDPLib/Risk/CVaR.lean`](MDPLib/Risk/CVaR.lean) is a stub with notes for CVaR. ## Building and testing @@ -162,17 +151,12 @@ Mathlib pieces are and are not available for Conditional Value at Risk. lake build MDPLib # the library lake -R build MDPLib:docs # the API documentation lake build mdplib # the binary file -lake build MDPLibTest # tests the elaborationa dn +lake build MDPLibTest # computability tests +./test.sh # computability + regression tests, interpreted and compiled (Linux) ``` +CI runs the library build, `test.sh`, the docs and the paper on every pull request. -On linux, you can use build and test the binary file as follows: -```bash -./test.sh # computability + regression tests, interpreted and compiled -``` - -CI (`.github/workflows/ci.yml`) runs the library build, that script, the docs and the paper on -every pull request, and deploys to GitHub Pages on `main`. ## Lean Resources