OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/ActualWindowMass.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.OrdinaryChainScales.actual_window_massline 27 - theorem
OAI.OrdinaryChainScales.actual_terminal_energyline 42