OAI/Combinatorics/BalancedRyser/Profiles/DetectionThresholds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.ProfileDetection.cutoffDetection line 18
2. def OAI.Balanced.ProfileDetection.positiveDetection line 21
3. theorem OAI.Balanced.ProfileDetection.cutoffDetection_mono line 24
4. theorem OAI.Balanced.ProfileDetection.iUnion_cutoffDetection line 33
5. theorem OAI.Balanced.ProfileDetection.tendsto_measure_cutoffDetection line 55
6. theorem OAI.Balanced.ProfileDetection.tendsto_measureReal_cutoffDetection line 62
7. theorem OAI.Balanced.ProfileDetection.product_positiveDetection_mass line 69
8. theorem OAI.Balanced.ProfileDetection.tendsto_cutoffDetection_visible_mass line 102