OAI/NumberTheory/Ostmann/Construction/LogCellLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Construction.tendsto_center_ratio line 10
2. theorem OAI.Ostmann.Construction.logCellMass_limit_of_logMass_limit line 28
3. theorem OAI.Ostmann.Construction.logCell_two_point_error_tendsto line 44
4. theorem OAI.Ostmann.Construction.logCellMass_limit_uniform_delete_two line 53
5. theorem OAI.Ostmann.Construction.logCellLogMass_limit_uniform_delete_two line 71
6. theorem OAI.Ostmann.Construction.logCellMass_eventually_normalizable line 99