OAI/NumberTheory/DirichletL/RowCompletion/InitialDensity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CanonicalRowCompletion.hasInitialCanonicalDensityAtRadius_of_theta line 91
2. theorem OAI.InitialMeanSquare.initial_sector_transfer_radius line 215
3. theorem OAI.InitialMeanSquare.initial_subbin_transfer_radius line 299
4. theorem OAI.InitialMeanSquare.initial_source_target_coprime line 364
5. theorem OAI.InitialMeanSquare.HasInitialCanonicalDensityAtRadius.retained_density line 385
6. theorem OAI.InitialMeanSquare.HasInitialCanonicalDensityAtRadius.retained_source line 501