OAI/Combinatorics/SquareDifference/ReflectionLaw.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.expect_two_halves line 11
  2. lemma OAI.SquareDifference.tupleValidity_half line 25
  3. lemma OAI.SquareDifference.tupleWeight_half line 45
  4. lemma OAI.SquareDifference.tupleCutForm_unmarked_factor line 59
  5. lemma OAI.SquareDifference.weighted_average_sq_le line 103
  6. lemma OAI.SquareDifference.list_factorized_quadratic line 111
  7. lemma OAI.SquareDifference.list_factorized_lower line 131
  8. def OAI.SquareDifference.tupleUnmarkedMoment line 165
  9. lemma OAI.SquareDifference.tupleUnmarkedMoment_nonneg line 173
  10. lemma OAI.SquareDifference.tuple_unmarked_error_exact line 180
  11. lemma OAI.SquareDifference.card_tupleHalfEntry_le line 194
  12. lemma OAI.SquareDifference.card_relation_le_sq line 214
  13. lemma OAI.SquareDifference.card_tupleCrossEdges_le line 221
  14. def OAI.SquareDifference.tupleUnmarkedConstant line 226
  15. lemma OAI.SquareDifference.tuple_unmarked_error line 229
  16. lemma OAI.SquareDifference.tupleUnmarkedGraph_terminal line 250
  17. lemma OAI.SquareDifference.tuple_terminal_positive line 257
  18. abbrev OAI.SquareDifference.TupleCutWord line 267
  19. def OAI.SquareDifference.orderedPermEquiv line 270
  20. lemma OAI.SquareDifference.card_orderedPerm line 277
  21. lemma OAI.SquareDifference.card_tupleCutWord line 283
  22. def OAI.SquareDifference.tupleMarkAddress line 287
  23. def OAI.SquareDifference.tupleUnmarkAddress line 291
  24. lemma OAI.SquareDifference.tupleUnmarkAddress_at line 295
  25. lemma OAI.SquareDifference.tupleMark_unmark line 301
  26. lemma OAI.SquareDifference.tupleUnmark_mark line 308
  27. def OAI.SquareDifference.tupleHalfAddressEquiv line 318
  28. def OAI.SquareDifference.tupleMarkIndexEquiv line 334
  29. def OAI.SquareDifference.tupleRegroupEquiv line 341
  30. lemma OAI.SquareDifference.expect_ge_single line 348
  31. lemma OAI.SquareDifference.expect_prod_function line 356
  32. lemma OAI.SquareDifference.expect_restrict_first line 366
  33. lemma OAI.SquareDifference.tupleRegroup_fst line 375
  34. lemma OAI.SquareDifference.tupleRegroup_snd line 380
  35. def OAI.SquareDifference.tupleWordOfHalf line 387
  36. lemma OAI.SquareDifference.tupleRegroup_projection line 390
  37. lemma OAI.SquareDifference.tuple_regroup_edges line 400
  38. lemma OAI.SquareDifference.graphValidity_antitone line 418
  39. lemma OAI.SquareDifference.tuple_regroup_validity line 424
  40. lemma OAI.SquareDifference.tuple_regroup_moment line 435
  41. lemma OAI.SquareDifference.card_cutHalf_eq_div line 474
  42. def OAI.SquareDifference.tupleHalfCount line 480
  43. lemma OAI.SquareDifference.card_tupleHalf line 482
  44. lemma OAI.SquareDifference.tupleR_one_le line 486
  45. def OAI.SquareDifference.tupleMarkedConstant line 488
  46. lemma OAI.SquareDifference.tupleMarkedConstant_pos line 492
  47. lemma OAI.SquareDifference.tupleMarkedConstant_le line 496