feat(PhyslibAlpha): Fisher-Rao metric and Cramer-Rao bound for algebraic framework - #1657
naype888-cloud wants to merge 6 commits into
Conversation
|
Thank you for this pull-request (PR). If this is your first PR, welcome to the community! Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.
Tip: The easiest way to get have a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your chages. If you have any problems or questions, please reach out to the community on the Zulip. |
|
I tried importing this file for the Fubini-Study bridge and none of the declarations come through. OpenSimplex, fisherRaoInner and cramerRao all show as unknown identifiers from the importing file. The file is a module with no public section so everything in it stays private to the file. CI won't catch this until something tries to import it. Adding @[expose] public section after the module docstring will fix it. I've tested this locally and the three names then resolve and it's what the other files in PhyslibAlpha do. The maths checks out for me btw and the convention with no factor of 1/4 is the one I want on my side. I'll continue working on my side. |
naype888-cloud
changed the title
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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
`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 <noreply@anthropic.com>
|
zyan tks for the missing @expose public, i all ready fix it with claude, you can see if worksflow now its full operating, all stable now for use allthe chain. i hope this works for you now. |
3 participants
Add classical Fisher-Rao metric and Cramér-Rao bound on open simplex
Following @tobby's recommendation, this PR integrates the classical Fisher-Rao Riemannian metric and the Cramér-Rao lower bound into PhyslibAlpha.AlgebraicFramework.InformationGeometry.
Definitions & Main Results
OpenSimplex (α : Type*) [Fintype α]
The open probability simplex: p i > 0 for all i and ∑ i, p i = 1.
fisherRaoInner
The Fisher-Rao inner product on the tangent space at p:
g_p(u, v) = \sum_i \frac{u_i v_i}{p_i}
with full positive-definiteness proved as fisherRaoSq_eq_zero_iff.
fisherRao_cauchy_schwarz
Cauchy-Schwarz inequality for the Fisher-Rao quadratic form. This is the exact classical obstruction kernel underlying the Robertson-Schrödinger uncertainty relation.
fisherInfo_eq_fisherRaoSq
Verification that Fisher information equals the squared Fisher-Rao norm of the score vector:
I(\theta) = | s_\theta |_{g_p}^2
cramerRao
The classical Cramér-Rao lower bound derived via Cauchy-Schwarz:
\mathrm{Var}_p(T) \geq \frac{1}{I(\theta)}
Integration & Purpose
Directly extends the algebraic state uncertainty bounds merged in #1649 and #1650.
Provides the target simplex infrastructure required by @zblore to connect the Fubini-Study projective quotient metric with the Fisher-Rao metric in the Integrating QuantumInfo initiative.
Status
0 sorries
Only Mathlib imports
Fully sorry-free and builds clean
Note: The mathematical reasoning my own, code architecture and proofs in this PR are LLM suported.