From d3778f74cb9c4b59b6b7b2995b2b40ce9f19a62b Mon Sep 17 00:00:00 2001 From: Eduardo Nava Hernandez Date: Wed, 16 Sep 2026 11:54:00 -0600 Subject: [PATCH 1/6] feat(PhyslibAlpha): Fisher-Rao metric and Cramer-Rao bound for algebraic states --- PhyslibAlpha.lean | 1 + .../InformationGeometry/FisherRao.lean | 216 ++++++++++++++++++ 2 files changed, 217 insertions(+) create mode 100644 PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index 6102e0c8d..15b69d5e4 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -229,4 +229,5 @@ public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanStatistics public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanPositivity public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanCFC public import PhyslibAlpha.AlgebraicFramework.CStarAlgebra.JordanSpecial +public import PhyslibAlpha.AlgebraicFramework.InformationGeometry.FisherRao public import PhyslibAlpha.Relativity.General.Schwarzschild.IncompressibleSphere diff --git a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean new file mode 100644 index 000000000..61fb7366c --- /dev/null +++ b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean @@ -0,0 +1,216 @@ +/- +Copyright (c) 2026 Eduardo Nava Hernandez. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eduardo Nava Hernandez +-/ +import Mathlib.Analysis.InnerProductSpace.Basic +import Mathlib.Algebra.BigOperators.Finprod +import Mathlib.Algebra.Order.Field.Basic +import Mathlib.Algebra.BigOperators.Group.Finset.Basic +import Mathlib.Topology.Algebra.InfiniteSum.Basic +import PhyslibAlpha.Basic + +/-! +# Fisher--Rao metric and Cramer--Rao bound (finite case) + +Defines the Fisher--Rao inner product on the open probability simplex +and the classical Cramer--Rao lower bound on estimator variance, +for finite sample spaces. All definitions reuse Mathlib primitives +(`Finset.sum`, `div`, `sq`). The Cramer--Rao proof is Cauchy--Schwarz +on the weighted inner product -- the same obstruction kernel as +Robertson--Schrödinger in algebraic uncertainty frameworks. + +## Main definitions + +* `PhyslibAlpha.OpenSimplex` — a point on the open probability simplex. +* `PhyslibAlpha.OpenSimplex.fisherRaoInner` — the Fisher--Rao inner product $g_p(u,v)$. +* `PhyslibAlpha.fisherInfo` — classical Fisher information $I(θ)$ for a parametric family. +* `PhyslibAlpha.cramerRao` — the Cramer--Rao lower bound $\mathrm{Var}(T) \ge 1/I(θ)$. + +## References + +* C. R. Rao, *Information and the accuracy attainable in the estimation + of statistical parameters*, Bull. Calcutta Math. Soc. 37, 81--91 (1945). +* H. Cramer, *Mathematical Methods of Statistics*, Princeton (1946). +-/ + +noncomputable section + +open Finset BigOperators + +variable {α : Type*} [Fintype α] + +namespace PhyslibAlpha + +/-! ## I. Open probability simplex -/ + +/-- A point on the open probability simplex: strictly positive weights summing to 1. -/ +structure OpenSimplex (α : Type*) [Fintype α] where + val : α → ℝ + pos : ∀ i, 0 < val i + sum_one : ∑ i : α, val i = 1 + +namespace OpenSimplex + +variable (p : OpenSimplex α) + +/-- Every coordinate is nonzero (convenience lemma). -/ +theorem val_ne_zero (i : α) : p.val i ≠ 0 := ne_of_gt (p.pos i) + +/-- Every coordinate is nonneg (convenience lemma). -/ +theorem val_nonneg (i : α) : 0 ≤ p.val i := le_of_lt (p.pos i) + +/-! ## II. Fisher--Rao inner product -/ + +/-- The Fisher--Rao inner product at $p \in \Delta^\circ(\alpha)$: + `g_p(u, v) = \sum_{i \in \alpha} \frac{u_i v_i}{p_i}` -/ +def fisherRaoInner (u v : α → ℝ) : ℝ := + ∑ i : α, u i * v i / p.val i + +/-- The Fisher--Rao quadratic form (squared norm). -/ +def fisherRaoSq (u : α → ℝ) : ℝ := p.fisherRaoInner u u + +/-- $g_p(u, u) \ge 0$ for all $u$. -/ +theorem fisherRaoSq_nonneg (u : α → ℝ) : 0 ≤ p.fisherRaoSq u := by + apply Finset.sum_nonneg + intro i _ + apply div_nonneg + · exact mul_self_nonneg (u i) + · exact p.val_nonneg i + +/-- $g_p(u, u) = 0 \iff u = 0$ (positive definiteness). -/ +theorem fisherRaoSq_eq_zero_iff (u : α → ℝ) : + p.fisherRaoSq u = 0 ↔ u = 0 := by + constructor + · intro h + have hnn : ∀ i ∈ Finset.univ, 0 ≤ u i * u i / p.val i := by + intro i _ + exact div_nonneg (mul_self_nonneg _) (p.val_nonneg i) + have hall := Finset.sum_eq_zero_iff_of_nonneg hnn |>.mp h + ext i + simp only [Pi.zero_apply] + have hi := hall i (Finset.mem_univ i) + rcases div_eq_zero_iff.mp hi with hmul | habs + · exact mul_self_eq_zero.mp hmul + · exact absurd habs (p.val_ne_zero i) + · intro h + simp [fisherRaoSq, fisherRaoInner, h] + +/-- Symmetry: $g_p(u, v) = g_p(v, u)$. -/ +theorem fisherRaoInner_comm (u v : α → ℝ) : + p.fisherRaoInner u v = p.fisherRaoInner v u := by + simp only [fisherRaoInner] + congr 1; ext i; ring + +/-- Expansion of the Fisher--Rao norm under linear combinations. -/ +theorem fisherRaoInner_sub_smul (u v : α → ℝ) (t : ℝ) : + p.fisherRaoSq (fun i => u i - t * v i) = + p.fisherRaoSq u - 2 * t * p.fisherRaoInner u v + + t ^ 2 * p.fisherRaoSq v := by + simp only [fisherRaoSq, fisherRaoInner] + rw [show (∑ i : α, (u i - t * v i) * (u i - t * v i) / p.val i) = + (∑ i : α, u i * u i / p.val i) - 2 * t * (∑ i : α, u i * v i / p.val i) + + t ^ 2 * (∑ i : α, v i * v i / p.val i) from by + rw [Finset.mul_sum, Finset.mul_sum] + simp only [← Finset.sum_add_distrib, ← Finset.sum_sub_distrib] + apply Finset.sum_congr rfl; intro i _; ring] + +/-- Cauchy--Schwarz for the Fisher--Rao inner product: + $g_p(u, v)^2 \le g_p(u, u) \cdot g_p(v, v)$. -/ +theorem fisherRao_cauchy_schwarz (u v : α → ℝ) : + p.fisherRaoInner u v ^ 2 ≤ p.fisherRaoSq u * p.fisherRaoSq v := by + by_cases hv : p.fisherRaoSq v = 0 + · rw [p.fisherRaoSq_eq_zero_iff] at hv + simp [fisherRaoInner, fisherRaoSq, hv] + · have hvpos : 0 < p.fisherRaoSq v := + lt_of_le_of_ne (p.fisherRaoSq_nonneg v) (Ne.symm hv) + set t := p.fisherRaoInner u v / p.fisherRaoSq v with ht_def + have key := p.fisherRaoSq_nonneg (fun i => u i - t * v i) + rw [p.fisherRaoInner_sub_smul u v t] at key + have ht2 : t * p.fisherRaoInner u v = + p.fisherRaoInner u v ^ 2 / p.fisherRaoSq v := by + rw [ht_def]; field_simp + have ht3 : t ^ 2 * p.fisherRaoSq v = + p.fisherRaoInner u v ^ 2 / p.fisherRaoSq v := by + rw [ht_def]; field_simp + rw [show 2 * t * p.fisherRaoInner u v = + 2 * (p.fisherRaoInner u v ^ 2 / p.fisherRaoSq v) from by + linarith [ht2]] at key + rw [ht3] at key + have h1 : p.fisherRaoInner u v ^ 2 / p.fisherRaoSq v ≤ p.fisherRaoSq u := + by linarith + rwa [div_le_iff₀ hvpos] at h1 + +end OpenSimplex + +/-! ## III. Classical Fisher information -/ + +/-- Classical Fisher information for a 1-parameter discrete family + $\theta \mapsto p(\cdot|\theta)$, given as $I(\theta) = \sum_i \frac{(\partial p_i / \partial \theta)^2}{p_i(\theta)}$. + This equals the Fisher--Rao squared norm of the score tangent vector. -/ +def fisherInfo (p : α → ℝ) (dp : α → ℝ) : ℝ := + ∑ i : α, dp i ^ 2 / p i + +/-- Fisher information is nonneg. -/ +theorem fisherInfo_nonneg (p dp : α → ℝ) (hpos : ∀ i, 0 < p i) : + 0 ≤ fisherInfo p dp := by + apply Finset.sum_nonneg + intro i _ + exact div_nonneg (sq_nonneg _) (le_of_lt (hpos i)) + +/-- Fisher information equals the Fisher--Rao squared norm of the + derivative vector: $I(\theta) = \|dp/d\theta\|^2_{\mathrm{FR}}$. -/ +theorem fisherInfo_eq_fisherRaoSq (q : OpenSimplex α) (dp : α → ℝ) : + fisherInfo q.val dp = q.fisherRaoSq dp := by + simp only [fisherInfo, OpenSimplex.fisherRaoSq, OpenSimplex.fisherRaoInner] + congr 1; ext i; ring + +/-! ## IV. Cramer--Rao lower bound -/ + +/-- Weighted expectation $\mathbb{E}_p[f] = \sum_i f(i) p(i)$. -/ +def expect (p : α → ℝ) (f : α → ℝ) : ℝ := + ∑ i : α, f i * p i + +/-- Weighted variance $\mathrm{Var}_p(f) = \mathbb{E}_p[(f - \mathbb{E}_p[f])^2]$. -/ +def variance (p : α → ℝ) (f : α → ℝ) : ℝ := + expect p (fun i => (f i - expect p f) ^ 2) + +/-- **Cramer--Rao lower bound.** For a parametric family with + all $p_i > 0$ and an estimator $T$ satisfying the unbiasedness + derivative condition $\sum_i T(i) \cdot (\partial p_i / \partial \theta) = 1$, we have + + $\mathrm{Var}_p(T) \ge 1 / I(\theta)$ + + where $I(\theta) = \mathrm{fisherInfo}(p, dp)$. The proof is a single application + of Cauchy--Schwarz on the Fisher--Rao inner product to the pair + $(T - \mathbb{E}[T], dp/p)$. -/ +theorem cramerRao (p dp : α → ℝ) (T : α → ℝ) + (hpos : ∀ i, 0 < p i) + (hsum : ∑ i : α, p i = 1) + (hdsum : ∑ i : α, dp i = 0) + (hunbiased : ∑ i : α, T i * dp i = 1) + (hI : 0 < fisherInfo p dp) : + 1 / fisherInfo p dp ≤ variance p T := by + let q : OpenSimplex α := ⟨p, hpos, hsum⟩ + let a : α → ℝ := fun i => (T i - expect p T) * p i + have cs := q.fisherRao_cauchy_schwarz a dp + have hpne : ∀ i, p i ≠ 0 := fun i => ne_of_gt (hpos i) + have inner_eq : q.fisherRaoInner a dp = 1 := by + simp only [OpenSimplex.fisherRaoInner, a] + conv => lhs; arg 2; ext i; rw [show ((T i - expect p T) * p i) * dp i / p i = + (T i - expect p T) * dp i from by field_simp [hpne i]] + simp_rw [sub_mul] + rw [Finset.sum_sub_distrib, ← Finset.mul_sum, hdsum, mul_zero, sub_zero] + exact hunbiased + have sq_u_eq : q.fisherRaoSq a = variance p T := by + simp only [OpenSimplex.fisherRaoSq, OpenSimplex.fisherRaoInner, variance, expect, a] + apply Finset.sum_congr rfl; intro i _ + simp only [q]; field_simp [hpne i] + have sq_v_eq : q.fisherRaoSq dp = fisherInfo p dp := by + simp only [OpenSimplex.fisherRaoSq, OpenSimplex.fisherRaoInner, fisherInfo] + apply Finset.sum_congr rfl; intro i _; ring + rw [inner_eq, sq_u_eq, sq_v_eq] at cs + rw [one_pow] at cs + rwa [div_le_iff₀ hI] + +end PhyslibAlpha From 5f21d9867f8fbb06364d27d34fd701bcb28cc5bc Mon Sep 17 00:00:00 2001 From: Eduardo Nava Hernandez Date: Wed, 16 Sep 2026 12:05:40 -0600 Subject: [PATCH 2/6] style: wrap docstring line to satisfy 100-char linter rule --- .../AlgebraicFramework/InformationGeometry/FisherRao.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean index 61fb7366c..18995e088 100644 --- a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean +++ b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean @@ -146,7 +146,8 @@ end OpenSimplex /-! ## III. Classical Fisher information -/ /-- Classical Fisher information for a 1-parameter discrete family - $\theta \mapsto p(\cdot|\theta)$, given as $I(\theta) = \sum_i \frac{(\partial p_i / \partial \theta)^2}{p_i(\theta)}$. + $\theta \mapsto p(\cdot|\theta)$, given as + $I(\theta) = \sum_i \frac{(\partial p_i / \partial \theta)^2}{p_i(\theta)}$. This equals the Fisher--Rao squared norm of the score tangent vector. -/ def fisherInfo (p : α → ℝ) (dp : α → ℝ) : ℝ := ∑ i : α, dp i ^ 2 / p i From 7db19c75101e0e2575017d0628aacf751a25e83c Mon Sep 17 00:00:00 2001 From: Eduardo Nava Hernandez Date: Wed, 16 Sep 2026 12:13:33 -0600 Subject: [PATCH 3/6] fix(PhyslibAlpha): add module header to FisherRao.lean for module system compliance --- .../InformationGeometry/FisherRao.lean | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean index 18995e088..396bad8d8 100644 --- a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean +++ b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean @@ -3,12 +3,14 @@ Copyright (c) 2026 Eduardo Nava Hernandez. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Eduardo Nava Hernandez -/ -import Mathlib.Analysis.InnerProductSpace.Basic -import Mathlib.Algebra.BigOperators.Finprod -import Mathlib.Algebra.Order.Field.Basic -import Mathlib.Algebra.BigOperators.Group.Finset.Basic -import Mathlib.Topology.Algebra.InfiniteSum.Basic -import PhyslibAlpha.Basic +module + +public import Mathlib.Analysis.InnerProductSpace.Basic +public import Mathlib.Algebra.BigOperators.Finprod +public import Mathlib.Algebra.Order.Field.Basic +public import Mathlib.Algebra.BigOperators.Group.Finset.Basic +public import Mathlib.Topology.Algebra.InfiniteSum.Basic +public import PhyslibAlpha.Basic /-! # Fisher--Rao metric and Cramer--Rao bound (finite case) From e5cbf00dcaab0f1bfafec81021d282fc0a2a2654 Mon Sep 17 00:00:00 2001 From: Eduardo Nava Hernandez Date: Fri, 18 Sep 2026 18:15:22 -0600 Subject: [PATCH 4/6] fix(PhyslibAlpha): expose FisherRao declarations with a public section FisherRao.lean is a `module` without `@[expose] public section`, so `OpenSimplex`, `fisherRaoInner`, `fisherInfo` and `cramerRao` were private to the file and importing modules saw them as unknown identifiers. Add the public section, as in the other PhyslibAlpha files. Co-Authored-By: Claude Sonnet 5 --- .../AlgebraicFramework/InformationGeometry/FisherRao.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean index 396bad8d8..7b9ab8ab3 100644 --- a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean +++ b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean @@ -36,6 +36,8 @@ Robertson--Schrödinger in algebraic uncertainty frameworks. * H. Cramer, *Mathematical Methods of Statistics*, Princeton (1946). -/ +@[expose] public section + noncomputable section open Finset BigOperators From 08dca00755a5bc91d9bfefe52e07e8137b918946 Mon Sep 17 00:00:00 2001 From: Eduardo Nava Hernandez Date: Fri, 18 Sep 2026 18:23:36 -0600 Subject: [PATCH 5/6] fix(PhyslibAlpha): document the fields of OpenSimplex Exposing the module's public section makes the `docBlame` linter check `OpenSimplex.val`, `pos` and `sum_one`. Add their docstrings. Co-Authored-By: Claude Sonnet 5 --- .../AlgebraicFramework/InformationGeometry/FisherRao.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean index 7b9ab8ab3..07aab15bb 100644 --- a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean +++ b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean @@ -50,8 +50,11 @@ namespace PhyslibAlpha /-- A point on the open probability simplex: strictly positive weights summing to 1. -/ structure OpenSimplex (α : Type*) [Fintype α] where + /-- The probability weight at each outcome. -/ val : α → ℝ + /-- Every weight is strictly positive. -/ pos : ∀ i, 0 < val i + /-- The weights sum to one. -/ sum_one : ∑ i : α, val i = 1 namespace OpenSimplex From 913db45045435f2f5052eff174f587f06212c4b5 Mon Sep 17 00:00:00 2001 From: Eduardo Nava Hernandez Date: Fri, 18 Sep 2026 20:40:06 -0600 Subject: [PATCH 6/6] refactor(PhyslibAlpha): move expect and variance under OpenSimplex MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `PhyslibAlpha.expect` and `PhyslibAlpha.variance` were generic names in the root namespace, next to `LinearMap.variance` and `UnitalPositiveLinearMap.variance`. Define them as `OpenSimplex.expect` and `OpenSimplex.variance` on a point of the simplex, and state `cramerRao` for `q : OpenSimplex α` instead of a raw weight vector with `hpos`/`hsum`. Co-Authored-By: Claude Sonnet 5 --- .../InformationGeometry/FisherRao.lean | 54 ++++++++++--------- 1 file changed, 30 insertions(+), 24 deletions(-) diff --git a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean index 07aab15bb..7d1842808 100644 --- a/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean +++ b/PhyslibAlpha/AlgebraicFramework/InformationGeometry/FisherRao.lean @@ -26,6 +26,8 @@ Robertson--Schrödinger in algebraic uncertainty frameworks. * `PhyslibAlpha.OpenSimplex` — a point on the open probability simplex. * `PhyslibAlpha.OpenSimplex.fisherRaoInner` — the Fisher--Rao inner product $g_p(u,v)$. +* `PhyslibAlpha.OpenSimplex.expect`, `PhyslibAlpha.OpenSimplex.variance` — expectation and + variance of a function under a point of the simplex. * `PhyslibAlpha.fisherInfo` — classical Fisher information $I(θ)$ for a parametric family. * `PhyslibAlpha.cramerRao` — the Cramer--Rao lower bound $\mathrm{Var}(T) \ge 1/I(θ)$. @@ -175,46 +177,50 @@ theorem fisherInfo_eq_fisherRaoSq (q : OpenSimplex α) (dp : α → ℝ) : /-! ## IV. Cramer--Rao lower bound -/ +namespace OpenSimplex + +variable (p : OpenSimplex α) + /-- Weighted expectation $\mathbb{E}_p[f] = \sum_i f(i) p(i)$. -/ -def expect (p : α → ℝ) (f : α → ℝ) : ℝ := - ∑ i : α, f i * p i +def expect (f : α → ℝ) : ℝ := + ∑ i : α, f i * p.val i /-- Weighted variance $\mathrm{Var}_p(f) = \mathbb{E}_p[(f - \mathbb{E}_p[f])^2]$. -/ -def variance (p : α → ℝ) (f : α → ℝ) : ℝ := - expect p (fun i => (f i - expect p f) ^ 2) +def variance (f : α → ℝ) : ℝ := + p.expect fun i => (f i - p.expect f) ^ 2 + +end OpenSimplex -/-- **Cramer--Rao lower bound.** For a parametric family with - all $p_i > 0$ and an estimator $T$ satisfying the unbiasedness - derivative condition $\sum_i T(i) \cdot (\partial p_i / \partial \theta) = 1$, we have +/-- **Cramer--Rao lower bound.** For a parametric family through a point `q` of the open + simplex with derivative vector `dp` (so $\sum_i dp_i = 0$), and an estimator $T$ satisfying + the unbiasedness derivative condition $\sum_i T(i) \cdot dp_i = 1$, we have - $\mathrm{Var}_p(T) \ge 1 / I(\theta)$ + $\mathrm{Var}_q(T) \ge 1 / I(\theta)$ - where $I(\theta) = \mathrm{fisherInfo}(p, dp)$. The proof is a single application + where $I(\theta) = \mathrm{fisherInfo}(q, dp)$. The proof is a single application of Cauchy--Schwarz on the Fisher--Rao inner product to the pair - $(T - \mathbb{E}[T], dp/p)$. -/ -theorem cramerRao (p dp : α → ℝ) (T : α → ℝ) - (hpos : ∀ i, 0 < p i) - (hsum : ∑ i : α, p i = 1) + $(T - \mathbb{E}[T], dp/q)$. -/ +theorem cramerRao (q : OpenSimplex α) (dp T : α → ℝ) (hdsum : ∑ i : α, dp i = 0) (hunbiased : ∑ i : α, T i * dp i = 1) - (hI : 0 < fisherInfo p dp) : - 1 / fisherInfo p dp ≤ variance p T := by - let q : OpenSimplex α := ⟨p, hpos, hsum⟩ - let a : α → ℝ := fun i => (T i - expect p T) * p i + (hI : 0 < fisherInfo q.val dp) : + 1 / fisherInfo q.val dp ≤ q.variance T := by + let a : α → ℝ := fun i => (T i - q.expect T) * q.val i have cs := q.fisherRao_cauchy_schwarz a dp - have hpne : ∀ i, p i ≠ 0 := fun i => ne_of_gt (hpos i) + have hpne : ∀ i, q.val i ≠ 0 := q.val_ne_zero have inner_eq : q.fisherRaoInner a dp = 1 := by simp only [OpenSimplex.fisherRaoInner, a] - conv => lhs; arg 2; ext i; rw [show ((T i - expect p T) * p i) * dp i / p i = - (T i - expect p T) * dp i from by field_simp [hpne i]] + conv => lhs; arg 2; ext i; rw [show ((T i - q.expect T) * q.val i) * dp i / q.val i = + (T i - q.expect T) * dp i from by field_simp [hpne i]] simp_rw [sub_mul] rw [Finset.sum_sub_distrib, ← Finset.mul_sum, hdsum, mul_zero, sub_zero] exact hunbiased - have sq_u_eq : q.fisherRaoSq a = variance p T := by - simp only [OpenSimplex.fisherRaoSq, OpenSimplex.fisherRaoInner, variance, expect, a] + have sq_u_eq : q.fisherRaoSq a = q.variance T := by + simp only [OpenSimplex.fisherRaoSq, OpenSimplex.fisherRaoInner, OpenSimplex.variance, + OpenSimplex.expect, a] apply Finset.sum_congr rfl; intro i _ - simp only [q]; field_simp [hpne i] - have sq_v_eq : q.fisherRaoSq dp = fisherInfo p dp := by + field_simp [hpne i] + have sq_v_eq : q.fisherRaoSq dp = fisherInfo q.val dp := by simp only [OpenSimplex.fisherRaoSq, OpenSimplex.fisherRaoInner, fisherInfo] apply Finset.sum_congr rfl; intro i _; ring rw [inner_eq, sq_u_eq, sq_v_eq] at cs