OAI/Combinatorics/Sidorenko/RandomHost.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Sampling a finite simple counterexample

The strict kernel inequality survives independent random sampling at sufficiently large finite size. Homomorphism counts include noninjective maps, whose collision error is bounded separately. The resulting simple graph has at least one edge.

  1. lemma OAI.SidorenkoCounterexample.FiniteLaw.independent_mean_unit line 19
  2. lemma OAI.SidorenkoCounterexample.FiniteLaw.independent_mean_apply line 25
  3. lemma OAI.SidorenkoCounterexample.FiniteLaw.independent_mean_two line 30
  4. lemma OAI.SidorenkoCounterexample.FiniteLaw.uniform_mean_equal line 48
  5. def OAI.SidorenkoCounterexample.FiniteLaw.coin line 54
  6. def OAI.SidorenkoCounterexample.FiniteLaw.boolValue line 56
  7. lemma OAI.SidorenkoCounterexample.FiniteLaw.boolValue_nonneg line 57
  8. lemma OAI.SidorenkoCounterexample.FiniteLaw.boolValue_le_one line 58
  9. lemma OAI.SidorenkoCounterexample.FiniteLaw.coin_mean line 59
  10. def OAI.SidorenkoCounterexample.bitsGraph line 64
  11. lemma OAI.SidorenkoCounterexample.bitsGraph_edgeIndicator line 69
  12. def OAI.SidorenkoCounterexample.edgeCoinLaw line 72
  13. lemma OAI.SidorenkoCounterexample.edgeCoinLaw_mean line 77
  14. def OAI.SidorenkoCounterexample.cornerEdge line 97
  15. lemma OAI.SidorenkoCounterexample.cornerEdge_injective line 98
  16. lemma OAI.SidorenkoCounterexample.mappedCorner_injective line 108
  17. lemma OAI.SidorenkoCounterexample.mappedCorner_ne line 112
  18. lemma OAI.SidorenkoCounterexample.expectedHom_conditional line 115
  19. def OAI.SidorenkoCounterexample.hostBitsLaw line 126
  20. lemma OAI.SidorenkoCounterexample.expectedHom_injective line 128
  21. lemma OAI.SidorenkoCounterexample.expectedEdge line 135
  22. lemma OAI.SidorenkoCounterexample.expectedHom_nonneg line 144
  23. lemma OAI.SidorenkoCounterexample.expectedHom_le_one line 147
  24. abbrev OAI.SidorenkoCounterexample.CollisionPair line 162
  25. def OAI.SidorenkoCounterexample.sourceFinEquiv line 163
  26. lemma OAI.SidorenkoCounterexample.collisionPair_card line 164
  27. def OAI.SidorenkoCounterexample.collisionValue line 169
  28. lemma OAI.SidorenkoCounterexample.collisionValue_nonneg line 171
  29. def OAI.SidorenkoCounterexample.noninjectiveIndicator line 173
  30. lemma OAI.SidorenkoCounterexample.noninjective_le_collisionSum line 175
  31. lemma OAI.SidorenkoCounterexample.collisionPair_ne line 191
  32. lemma OAI.SidorenkoCounterexample.collisionValue_mean line 193
  33. lemma OAI.SidorenkoCounterexample.noninjective_mean_bound line 199
  34. lemma OAI.SidorenkoCounterexample.uniformMean_offdiag line 222
  35. lemma OAI.SidorenkoCounterexample.expectedEdgeDensity line 233
  36. lemma OAI.SidorenkoCounterexample.expectedHom_map_bound line 241
  37. lemma OAI.SidorenkoCounterexample.expectedHomDensity_bound line 250
  38. lemma OAI.SidorenkoCounterexample.finiteHost_arithmetic line 264
  39. lemma OAI.SidorenkoCounterexample.finiteHost_exists_at_size line 282
  40. lemma OAI.SidorenkoCounterexample.finiteHost_main line 300
  41. theorem OAI.SidorenkoCounterexample.main_proved line 307
  42. theorem OAI.SidorenkoCounterexample.main line 319

    Source documentation

    The exact finite simple host conclusion of the counterexample theorem.

    Distinct definitions of this name: ComparatorChallenges/SidorenkoCounterexample.lean:41 (different declaration text). Qualify references as OAI.SidorenkoCounterexample.main@path.

    theorem main : ∃ n : ℕ, 0 < n ∧ ∃ G : SimpleGraph (Fin n),
    (∃ u v, G.Adj u v) ∧ homDensity H G < (edgeDensity G) ^ 66 := by
…

    Mentions: OAI.SidorenkoCounterexample.homDensity, OAI.SidorenkoCounterexample.edgeDensity