OAI/Combinatorics/BalancedRyser/Profiles/ProfileDetectionLimit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileDetection.product_positiveDetection_mass_ae line 11
  2. theorem OAI.Balanced.ProfileDetectionLimit.measurableSet_deletionVisible line 50
  3. theorem OAI.Balanced.ProfileDetectionLimit.measurableSet_coverVisible line 54
  4. def OAI.Balanced.ProfileDetectionLimit.dDiscrepancy line 58
  5. def OAI.Balanced.ProfileDetectionLimit.cDiscrepancy line 61
  6. theorem OAI.Balanced.ProfileDetectionLimit.measurable_dDiscrepancy line 64
  7. theorem OAI.Balanced.ProfileDetectionLimit.measurable_cDiscrepancy line 67
  8. theorem OAI.Balanced.ProfileDetectionLimit.tendsto_dCutoff_visible_mass line 70
  9. theorem OAI.Balanced.ProfileDetectionLimit.tendsto_cCutoff_visible_mass line 95
  10. theorem OAI.Balanced.ProfileDetectionLimit.tendsto_dCutoff_visible_mass_real line 121
  11. theorem OAI.Balanced.ProfileDetectionLimit.tendsto_cCutoff_visible_mass_real line 130
  12. theorem OAI.Balanced.ProfileDetectionLimit.tendsto_cutoff_sum_visible_mass line 139