OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairedFrequencyAverageHistoryBudget.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.schedule_budget_eq_historyWeightline 9 - theorem
OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.scheduleMatches_ambientDataline 28 - theorem
OAI.Ostmann.Arithmetic.HistoryPairedFrequencyAverage.ambient_schedule_budget_eq_historyWeightline 40