OAI/Combinatorics/HalvingLines/CrossingEstimate.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarHalving.FiniteSampling.weight line 12
  2. def OAI.PlanarHalving.FiniteSampling.expect line 15
  3. lemma OAI.PlanarHalving.FiniteSampling.weight_nonneg line 18
  4. lemma OAI.PlanarHalving.FiniteSampling.expect_prod line 27
  5. lemma OAI.PlanarHalving.FiniteSampling.expect_const line 38
  6. lemma OAI.PlanarHalving.FiniteSampling.expect_mono line 45
  7. lemma OAI.PlanarHalving.FiniteSampling.expect_sum line 51
  8. lemma OAI.PlanarHalving.FiniteSampling.expect_add line 58
  9. lemma OAI.PlanarHalving.FiniteSampling.expect_sub line 63
  10. lemma OAI.PlanarHalving.FiniteSampling.expect_mul_const line 68
  11. lemma OAI.PlanarHalving.FiniteSampling.expect_const_mul line 73
  12. def OAI.PlanarHalving.FiniteSampling.keep line 79
  13. lemma OAI.PlanarHalving.FiniteSampling.keep_prod line 82
  14. lemma OAI.PlanarHalving.FiniteSampling.expect_keep line 95
  15. lemma OAI.PlanarHalving.FiniteSampling.exists_ge_expect line 111
  16. lemma OAI.PlanarHalving.FiniteSampling.expect_single line 119
  17. lemma OAI.PlanarHalving.FiniteSampling.expect_pair line 126
  18. lemma OAI.PlanarHalving.FiniteSampling.expect_xor line 133
  19. def OAI.PlanarHalving.FiniteSampling.bit line 143
  20. lemma OAI.PlanarHalving.FiniteSampling.expect_cut line 148
  21. def OAI.PlanarHalving.PlaneGraph.Drawing.sample line 170
  22. lemma OAI.PlanarHalving.PlaneGraph.Drawing.sample_crossings line 180
  23. lemma OAI.PlanarHalving.PlaneGraph.Drawing.expect_vertices line 188
  24. lemma OAI.PlanarHalving.PlaneGraph.Drawing.expect_edges line 198
  25. lemma OAI.PlanarHalving.PlaneGraph.Drawing.expect_crossings line 216
  26. theorem OAI.PlanarHalving.PlaneGraph.Drawing.sample_crossing_bound line 234
  27. def OAI.PlanarHalving.PlaneGraph.Drawing.Bipartite line 247
  28. def OAI.PlanarHalving.PlaneGraph.twoProb line 250
  29. lemma OAI.PlanarHalving.PlaneGraph.Drawing.twoProb_edge line 254
  30. lemma OAI.PlanarHalving.PlaneGraph.Drawing.twoProb_vertices line 261
  31. lemma OAI.PlanarHalving.PlaneGraph.Drawing.bipartite_sample_bound line 279
  32. theorem OAI.PlanarHalving.PlaneGraph.crossing_sampling_algebra line 312
  33. theorem OAI.PlanarHalving.PlaneGraph.Drawing.bipartite_dense line 334
  34. def OAI.PlanarHalving.PlaneGraph.Drawing.cut line 360
  35. def OAI.PlanarHalving.PlaneGraph.Drawing.cutSide line 366
  36. lemma OAI.PlanarHalving.PlaneGraph.Drawing.cutSide_vertices line 371
  37. lemma OAI.PlanarHalving.PlaneGraph.Drawing.cutSide_designated line 377
  38. lemma OAI.PlanarHalving.PlaneGraph.Drawing.cut_bipartite line 386
  39. lemma OAI.PlanarHalving.PlaneGraph.Drawing.cut_crossings_le line 395
  40. lemma OAI.PlanarHalving.PlaneGraph.Drawing.cut_edges line 406
  41. lemma OAI.PlanarHalving.PlaneGraph.Drawing.cut_card line 410
  42. lemma OAI.PlanarHalving.PlaneGraph.Drawing.expect_cut_card line 418
  43. lemma OAI.PlanarHalving.PlaneGraph.Drawing.exists_large_cut line 437
  44. theorem OAI.PlanarHalving.PlaneGraph.Drawing.designated_dense line 446
  45. theorem OAI.PlanarHalving.PlaneGraph.Drawing.designated_crossing line 473