OAI/Combinatorics/Sidorenko/Charts.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SidorenkoCounterexample.uniformMean_injection line 13
  2. def OAI.SidorenkoCounterexample.canonicalStratumMass line 33
  3. def OAI.SidorenkoCounterexample.chartRatio line 36
  4. theorem OAI.SidorenkoCounterexample.chartRatio_nonneg line 41
  5. theorem OAI.SidorenkoCounterexample.chartRatio_bound line 44
  6. theorem OAI.SidorenkoCounterexample.canonicalStratum_card line 54
  7. theorem OAI.SidorenkoCounterexample.canonicalLag_card_pos line 62
  8. theorem OAI.SidorenkoCounterexample.canonicalStratumMass_pos line 66
  9. theorem OAI.SidorenkoCounterexample.canonicalStratumMass_bound line 75
  10. theorem OAI.SidorenkoCounterexample.signed_normalization_eventually line 100
  11. def OAI.SidorenkoCounterexample.faceLocal line 127
  12. theorem OAI.SidorenkoCounterexample.faceLocal_empty line 131
  13. theorem OAI.SidorenkoCounterexample.faceLocal_singleton line 134
  14. theorem OAI.SidorenkoCounterexample.faceLocal_pair line 140
  15. theorem OAI.SidorenkoCounterexample.faceLocal_full line 149
  16. def OAI.SidorenkoCounterexample.pairPolynomial line 158
  17. theorem OAI.SidorenkoCounterexample.signs_polynomial line 161
  18. theorem OAI.SidorenkoCounterexample.pairPolynomial_eq line 167
  19. def OAI.SidorenkoCounterexample.facePolynomial line 177
  20. def OAI.SidorenkoCounterexample.faceTransverse line 183
  21. theorem OAI.SidorenkoCounterexample.facePolynomial_full line 186
  22. def OAI.SidorenkoCounterexample.faceError line 198
  23. theorem OAI.SidorenkoCounterexample.faceError_nonneg line 202
  24. theorem OAI.SidorenkoCounterexample.faceLocal_error line 207
  25. def OAI.SidorenkoCounterexample.boolMonomial line 268
  26. theorem OAI.SidorenkoCounterexample.boolMonomial_empty line 271
  27. theorem OAI.SidorenkoCounterexample.bool_factor line 272
  28. theorem OAI.SidorenkoCounterexample.bool_indicator_product line 276
  29. theorem OAI.SidorenkoCounterexample.bool_indicator_expansion line 290
  30. theorem OAI.SidorenkoCounterexample.bool_law_expansion line 298
  31. theorem OAI.SidorenkoCounterexample.uniformMean_test_fibers line 306
  32. theorem OAI.SidorenkoCounterexample.boolean_law_tendsto line 320
  33. theorem OAI.SidorenkoCounterexample.boolean_test_tendsto line 337
  34. theorem OAI.SidorenkoCounterexample.pairBool_test_tendsto line 352
  35. theorem OAI.SidorenkoCounterexample.uniformMean_two_differences line 377
  36. def OAI.SidorenkoCounterexample.faceBound line 391
  37. theorem OAI.SidorenkoCounterexample.faceBound_one line 395
  38. theorem OAI.SidorenkoCounterexample.faceLocal_nonneg line 402
  39. theorem OAI.SidorenkoCounterexample.faceLocal_bound line 406
  40. theorem OAI.SidorenkoCounterexample.pairPolynomial_abs_le line 430
  41. theorem OAI.SidorenkoCounterexample.facePolynomial_abs_le line 436
  42. theorem OAI.SidorenkoCounterexample.faceBound_tendsto line 451
  43. theorem OAI.SidorenkoCounterexample.faceError_mean_tendsto line 460
  44. abbrev OAI.SidorenkoCounterexample.CanonicalLag line 493
  45. instance OAI.SidorenkoCounterexample.canonicalDual_finite line 494
  46. def OAI.SidorenkoCounterexample.canonicalKernel line 496
  47. theorem OAI.SidorenkoCounterexample.canonicalKernel_nonneg line 500
  48. theorem OAI.SidorenkoCounterexample.rankKernel_chart_bound line 505
  49. theorem OAI.SidorenkoCounterexample.canonicalKernel_prod line 523
  50. theorem OAI.SidorenkoCounterexample.canonicalKernel_mean line 540
  51. theorem OAI.SidorenkoCounterexample.faceLocal_chart_bound line 551