OAI/Combinatorics/BalancedRyser/Selection/SelectionCensorMassBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Selection.Process.noise_domain_overflow_mass_le line 15
  2. theorem OAI.Balanced.Selection.Process.noise_degree_censor_mass_le line 25
  3. theorem OAI.Balanced.Selection.Process.noise_degree_censor_mass_le_source line 57
  4. theorem OAI.Balanced.Selection.Process.domainOverflowMass_le_postcheckTail line 77
  5. theorem OAI.Balanced.Selection.Process.degreeCensorMass_le_source line 83
  6. theorem OAI.Balanced.Selection.Process.censoredDomain_mean_error_le_source line 94
  7. theorem OAI.Balanced.Selection.Process.censoredDegree_mean_le_source line 106
  8. theorem OAI.Balanced.Selection.Process.tendsto_polynomial_mul_postcheckTail line 122