OAI/Combinatorics/SquareDifference/CrossProducts.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.crossEdges_factor line 11
  2. lemma OAI.SquareDifference.graphValidity_singleton_cut line 29
  3. def OAI.SquareDifference.tupleZeroIndex line 43
  4. instance OAI.SquareDifference.tupleEmptyIndexSubsingleton line 46
  5. def OAI.SquareDifference.tupleLeadingEntry line 54
  6. def OAI.SquareDifference.tupleLeadingGraph line 63
  7. lemma OAI.SquareDifference.graphPullback_no_opp line 66
  8. lemma OAI.SquareDifference.graphPullback_no_loop line 74
  9. lemma OAI.SquareDifference.tupleLeadingGraph_no_opp line 80
  10. lemma OAI.SquareDifference.tupleLeadingGraph_no_loop line 83
  11. lemma OAI.SquareDifference.tupleComponent_leading_integral line 86
  12. def OAI.SquareDifference.graphCondConstant line 105
  13. lemma OAI.SquareDifference.graphCondConstant_nonneg line 110
  14. lemma OAI.SquareDifference.mem_graphPullback line 114
  15. def OAI.SquareDifference.graphRest line 118
  16. lemma OAI.SquareDifference.graphRest_le_one line 122
  17. lemma OAI.SquareDifference.split_merge line 131
  18. lemma OAI.SquareDifference.graphValidity_singleton_reindex line 139
  19. lemma OAI.SquareDifference.singleton_list_conditional_mixing line 153
  20. lemma OAI.SquareDifference.graph_conditional_mixing line 175
  21. lemma OAI.SquareDifference.tupleLeading_conditional_mixing line 191
  22. lemma OAI.SquareDifference.tupleComponent_marginal line 205
  23. lemma OAI.SquareDifference.tupleComponent_conditional_contraction line 213
  24. lemma OAI.SquareDifference.jointDensity_smul line 224
  25. lemma OAI.SquareDifference.jointDensity_sum line 231
  26. lemma OAI.SquareDifference.conditionalEnergy_sum_le line 237
  27. def OAI.SquareDifference.tupleSubmixture line 251
  28. lemma OAI.SquareDifference.tupleSubmixture_apply line 255
  29. lemma OAI.SquareDifference.tupleSubmixture_nonneg line 261
  30. lemma OAI.SquareDifference.tupleSubmixture_mass_lower line 268
  31. lemma OAI.SquareDifference.tupleSubmixture_marginal line 277
  32. def OAI.SquareDifference.tupleSubLaw line 282
  33. lemma OAI.SquareDifference.tupleSubLaw_probability line 286
  34. lemma OAI.SquareDifference.tupleSubLaw_nonneg line 292
  35. lemma OAI.SquareDifference.tupleSubLaw_marginal line 298
  36. lemma OAI.SquareDifference.tupleMixtureWeight_small line 306
  37. lemma OAI.SquareDifference.le_univ_sum_real line 313
  38. def OAI.SquareDifference.tupleConditionalNumerator line 317
  39. lemma OAI.SquareDifference.tupleConditionalNumerator_nonneg line 321
  40. lemma OAI.SquareDifference.tupleSubmixture_conditional line 325
  41. def OAI.SquareDifference.tupleConditionalConstant line 384
  42. def OAI.SquareDifference.tupleConditionalThreshold line 386
  43. lemma OAI.SquareDifference.rpow_absorb_32 line 389
  44. lemma OAI.SquareDifference.tupleSubLaw_conditional line 401
  45. lemma OAI.SquareDifference.linearMap_expect line 429
  46. def OAI.SquareDifference.squarePairAverage line 436
  47. lemma OAI.SquareDifference.square_affine_pair_average line 439
  48. lemma OAI.SquareDifference.tupleComponent_pair_congr line 460
  49. lemma OAI.SquareDifference.tupleComponent_pair_square line 474
  50. lemma OAI.SquareDifference.expect_eval line 503