OAI/Analysis/IrrationalRotation/Model/UniformIntervalPhase.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Invariant233.UniformIntervalPhase.intervalLawline 11 - def
OAI.Invariant233.UniformIntervalPhase.phaseLawline 14 - def
OAI.Invariant233.UniformIntervalPhase.phaseDensityline 17 - def
OAI.Invariant233.UniformIntervalPhase.representativeline 20 - def
OAI.Invariant233.UniformIntervalPhase.lambdaLawline 23 - def
OAI.Invariant233.UniformIntervalPhase.fractionLawline 26 - def
OAI.Invariant233.UniformIntervalPhase.fractionDensityline 29