OAI/Combinatorics/SharpRamsey/Marking/RowSpan.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

High-rank geometric supports and entropy estimates.

  1. def OAI.SharpLogRamsey.HighRankCoverage.rowSpan line 17
  2. lemma OAI.SharpLogRamsey.HighRankCoverage.le_rowSpan line 21
  3. lemma OAI.SharpLogRamsey.HighRankCoverage.rowSpan_eq line 25
  4. lemma OAI.SharpLogRamsey.HighRankCoverage.rowSpan_rank line 30
  5. lemma OAI.SharpLogRamsey.HighRankCoverage.indicator_all line 42
  6. theorem OAI.SharpLogRamsey.HighRankCoverage.stagnation_mass line 54
  7. theorem OAI.SharpLogRamsey.HighRankCoverage.span_growth line 68
  8. def OAI.SharpLogRamsey.HighRankCoverage.projectiveSubmoduleEquiv line 98
  9. lemma OAI.SharpLogRamsey.HighRankCoverage.projective_card line 125
  10. lemma OAI.SharpLogRamsey.HighRankCoverage.geom_sum_le_twice line 134
  11. lemma OAI.SharpLogRamsey.HighRankCoverage.small_span_card line 144
  12. lemma OAI.SharpLogRamsey.HighRankCoverage.marginal_mass line 159
  13. lemma OAI.SharpLogRamsey.HighRankCoverage.marginal_cap line 168
  14. def OAI.SharpLogRamsey.HighRankCoverage.hitSpace line 181
  15. lemma OAI.SharpLogRamsey.HighRankCoverage.escape_mass line 186
  16. theorem OAI.SharpLogRamsey.HighRankCoverage.projective_span_growth line 199
  17. lemma OAI.SharpLogRamsey.HighRankGrowth.run_span_le line 228
  18. lemma OAI.SharpLogRamsey.HighRankGrowth.run_le_full line 242
  19. lemma OAI.SharpLogRamsey.HighRankGrowth.block_mean line 256
  20. theorem OAI.SharpLogRamsey.HighRankGrowth.raw_row_span_growth line 271
  21. def OAI.SharpLogRamsey.FiniteEventBounds.indicator line 306
  22. lemma OAI.SharpLogRamsey.FiniteEventBounds.indicator_nonneg line 307
  23. lemma OAI.SharpLogRamsey.FiniteEventBounds.indicator_le_one line 308
  24. lemma OAI.SharpLogRamsey.FiniteEventBounds.indicator_mono line 309
  25. lemma OAI.SharpLogRamsey.FiniteEventBounds.indicator_or_le line 316
  26. lemma OAI.SharpLogRamsey.FiniteEventBounds.indicator_or_five line 319
  27. def OAI.SharpLogRamsey.FiniteEventBounds.mean2 line 330
  28. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_nonneg line 333
  29. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_mono line 343
  30. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_add line 353
  31. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_const line 357
  32. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_left line 362
  33. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_right line 366
  34. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_symm line 370
  35. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_cover_five line 381
  36. lemma OAI.SharpLogRamsey.FiniteEventBounds.mean2_sum line 398
  37. lemma OAI.SharpLogRamsey.FiniteEventBounds.average_with_exception line 414
  38. def OAI.SharpLogRamsey.HighRankCoverageProbability.conflictMass line 443
  39. theorem OAI.SharpLogRamsey.HighRankCoverageProbability.raw_coverage_union line 449