OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkActualPrincipalSourceReindexMeanBackgroundFunctions.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryBulkActualBSquareReplacement.rawBackgroundPoint line 44
2. def OAI.Ostmann.Arithmetic.HistoryBulkActualBSquareReplacement.densityBackgroundPoint line 51
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkActualBSquareReplacement.rawBackgroundPoint_eq_density line 64