inductive definition def or abbrev

`Statistics`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 161inductive Statistics where
 162  | fermiDirac
 163  | boseEinstein
 164deriving DecidableEq, Repr
 165
 166/-- Determine statistics from spin. -/

From the project-wide theorem graph. These declarations reference this one in their body.

boson_rotation_phase_pos_one in IndisputableMonolith.Foundation.SpinStatistics decl_use
exchange_sign_boson in IndisputableMonolith.Foundation.SpinStatistics decl_use
piInPhysics in IndisputableMonolith.Mathematics.Pi decl_use
quasi_charge_decreasing in IndisputableMonolith.Physics.QuantumHallEffect decl_use
summary in IndisputableMonolith.QFT decl_use
boson_symmetric in IndisputableMonolith.QFT.SpinStatistics decl_use
eight_ticks_full_cycle in IndisputableMonolith.QFT.SpinStatistics decl_use
exchangePhase in IndisputableMonolith.QFT.SpinStatistics decl_use
spin_statistics_boson in IndisputableMonolith.QFT.SpinStatistics decl_use
spin_statistics_fermion in IndisputableMonolith.QFT.SpinStatistics decl_use
statisticsFromSpin in IndisputableMonolith.QFT.SpinStatistics decl_use
certificateWithinTolerance in IndisputableMonolith.RSBridge.ResidueData decl_use
bayesianFilteringCert_holds in IndisputableMonolith.Statistics.BayesianFilteringFromVFE decl_use
cert_inhabited in IndisputableMonolith.Statistics.BayesianUpdateFromJCost decl_use
vfeCert_holds in IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL decl_use
stateProbability in IndisputableMonolith.Thermodynamics.JCostThermoBridge decl_use
classical_limit in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use

Lean names referenced from this declaration's body.

from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
boseEinstein in IndisputableMonolith.Thermodynamics.BoseEinstein decl_use
boseEinstein in IndisputableMonolith.Thermodynamics.FermiDirac decl_use
fermiDirac in IndisputableMonolith.Thermodynamics.FermiDirac decl_use
boseEinstein in IndisputableMonolith.Thermodynamics.JCostThermoBridge decl_use
fermiDirac in IndisputableMonolith.Thermodynamics.JCostThermoBridge decl_use