OAI/NumberTheory/Ostmann/Construction/SourcePriorGridDeletionMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Construction.SourcePriorGridDeletion.pointCap_nonneg line 9
2. theorem OAI.Ostmann.Construction.SourcePriorGridDeletion.deletionCap_nonneg line 12
3. theorem OAI.Ostmann.Construction.SourcePriorGridDeletion.fullMassRatio_nonneg line 15
4. theorem OAI.Ostmann.Construction.SourcePriorGridDeletion.fullMassRatio_le_one_add line 18
5. theorem OAI.Ostmann.Construction.SourcePriorGridDeletion.deletedMean_sub line 31
6. theorem OAI.Ostmann.Construction.SourcePriorGridDeletion.deletedMean_norm_le line 35