OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightCounts.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.template_current_length_leline 9 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.TreeSourceLabels.root_length_leline 19 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.TreeSourceLabels.internal_length_leline 26 - def
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.historyCostCoefficientline 39 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.historyCostCoefficient_posline 42 - theorem
OAI.Ostmann.Arithmetic.HistorySymbolicEncoding.TreeSourceLabels.cost_leline 46