theorem
proved
photonStatCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.PhotonStatisticsFromRS on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26 | superPoissonian | poissonian | subPoissonian | fano | mandelQ
27 deriving DecidableEq, Repr, BEq, Fintype
28
29theorem photonStatCount : Fintype.card PhotonStatisticsRegime = 5 := by decide
30
31/-- Coherent light (Poissonian): J = 0. -/
32theorem coherent_poissonian : Jcost 1 = 0 := Jcost_unit0
33
34structure PhotonStatCert where
35 five_regimes : Fintype.card PhotonStatisticsRegime = 5
36 coherent_zero : Jcost 1 = 0
37
38def photonStatCert : PhotonStatCert where
39 five_regimes := photonStatCount
40 coherent_zero := coherent_poissonian
41
42end IndisputableMonolith.Physics.PhotonStatisticsFromRS