OAI/Combinatorics/SharpRamsey/Learning/PreparedVariance.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLogRamsey.RegularPencils.sum_center_shift line 15
  2. lemma OAI.SharpLogRamsey.RegularPencils.indicator_sum line 25
  3. lemma OAI.SharpLogRamsey.RegularPencils.indicator_square_sum line 30
  4. theorem OAI.SharpLogRamsey.RegularPencils.cell_total_variance line 40
  5. def OAI.SharpLogRamsey.RegularPencils.exceptional line 111
  6. lemma OAI.SharpLogRamsey.RegularPencils.exceptional_indicator line 114
  7. theorem OAI.SharpLogRamsey.RegularPencils.exceptional_card line 128
  8. theorem OAI.SharpLogRamsey.RegularPencils.exceptional_mass line 140
  9. lemma OAI.SharpLogRamsey.RegularPencils.clip_nonneg line 157
  10. lemma OAI.SharpLogRamsey.RegularPencils.clip_le_one line 158
  11. lemma OAI.SharpLogRamsey.RegularPencils.clip_sum line 159
  12. lemma OAI.SharpLogRamsey.PreparedVariance.mass_weighted line 177
  13. lemma OAI.SharpLogRamsey.PreparedVariance.actual_cell_variance line 194
  14. theorem OAI.SharpLogRamsey.PreparedVariance.actual_exceptions line 202
  15. def OAI.SharpLogRamsey.PreparedVariance.weights line 244
  16. lemma OAI.SharpLogRamsey.PreparedVariance.weights_nonneg line 251
  17. lemma OAI.SharpLogRamsey.PreparedVariance.weights_le_one line 260
  18. lemma OAI.SharpLogRamsey.PreparedVariance.weights_total line 269
  19. theorem OAI.SharpLogRamsey.PreparedVariance.exists_regular line 286