OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightBins.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.sourceBulkHalf line 11
2. def OAI.Ostmann.Arithmetic.sourceSpectatorHalf line 14
3. instance OAI.Ostmann.Arithmetic.sourceBulkHalfDecidable line 17
4. instance OAI.Ostmann.Arithmetic.sourceSpectatorHalfDecidable line 21
5. def OAI.Ostmann.Arithmetic.realStateBins line 25
6. def OAI.Ostmann.Arithmetic.sourceStateBins line 32
7. theorem OAI.Ostmann.Arithmetic.realStateBins_bounds line 35
8. theorem OAI.Ostmann.Arithmetic.realStateBins_support line 48
9. theorem OAI.Ostmann.Arithmetic.realStateBins_contDiffAt line 62