OAI/Combinatorics/SharpRamsey/Reciprocal/LevelLosses.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpLogRamsey.Incidence.card_incident_points line 13
  2. theorem OAI.SharpLogRamsey.Incidence.incident_iff_dualAnnihilator line 26
  3. theorem OAI.SharpLogRamsey.Incidence.card_incident_dual line 34
  4. theorem OAI.SharpLogRamsey.Incidence.card_common_incident_dual line 45
  5. def OAI.SharpLogRamsey.Incidence.weightedIncidences line 69
  6. theorem OAI.SharpLogRamsey.Incidence.design_quadratic line 72
  7. theorem OAI.SharpLogRamsey.Incidence.design_variance line 119
  8. theorem OAI.SharpLogRamsey.Incidence.geom_design_identity line 143
  9. theorem OAI.SharpLogRamsey.Incidence.projective_variance line 162
  10. theorem OAI.SharpLogRamsey.Incidence.projective_variance_le line 208
  11. def OAI.SharpLogRamsey.Incidence.incidenceCount line 219
  12. theorem OAI.SharpLogRamsey.Incidence.projective_mixing_sq line 223
  13. theorem OAI.SharpLogRamsey.Incidence.projective_mixing line 259
  14. theorem OAI.SharpLogRamsey.Incidence.sparse_product_bound line 272
  15. theorem OAI.SharpLogRamsey.Incidence.mixing_cell_scale line 330
  16. theorem OAI.SharpLogRamsey.Incidence.mixing_loss_log line 386
  17. lemma OAI.SharpLogRamsey.Incidence.incidenceCount_eq_card line 435
  18. def OAI.SharpLogRamsey.Selection.positiveSupport line 447
  19. lemma OAI.SharpLogRamsey.Selection.positiveSupport_zero line 449
  20. lemma OAI.SharpLogRamsey.Selection.positiveSupport_cell_mass line 453
  21. lemma OAI.SharpLogRamsey.Selection.positive_cell_nonempty line 463
  22. def OAI.SharpLogRamsey.Incidence.endpointLabels line 479
  23. lemma OAI.SharpLogRamsey.Incidence.endpoint_cell_subset line 485
  24. theorem OAI.SharpLogRamsey.Incidence.reciprocal_level_losses line 500