OAI/Combinatorics/EuclideanRamsey/Discretization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.EuclideanRamsey.compact_taylor_bound line 23
  2. lemma OAI.EuclideanRamsey.linear_moment_contract line 66
  3. lemma OAI.EuclideanRamsey.bilinear_moment_contract line 82
  4. abbrev OAI.EuclideanRamsey.realLattice line 116
  5. def OAI.EuclideanRamsey.latticeSample line 117
  6. lemma OAI.EuclideanRamsey.latticeSample_injective line 119
  7. lemma OAI.EuclideanRamsey.latticeSample_mem_grid line 127
  8. lemma OAI.EuclideanRamsey.grid_surjective line 137
  9. lemma OAI.EuclideanRamsey.lattice_tsum_eq_grid line 150
  10. theorem OAI.EuclideanRamsey.lattice_riemann line 168
  11. lemma OAI.EuclideanRamsey.latticeSample_finite_support line 190