OAI/Combinatorics/SquareDifference/MarkedTuples.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.tuple_marked_uniform line 11
  2. lemma OAI.SquareDifference.tuple_marking_domination line 24
  3. lemma OAI.SquareDifference.truncated_sum_nonneg_of_pairs line 38
  4. lemma OAI.SquareDifference.balanced_rpow_error line 58
  5. lemma OAI.SquareDifference.tupleUnmarkedConstant_nonneg line 78
  6. def OAI.SquareDifference.tupleReflectionThreshold line 82
  7. lemma OAI.SquareDifference.tuple_pair_positive line 86
  8. def OAI.SquareDifference.tupleMixtureWeight line 116
  9. lemma OAI.SquareDifference.tupleMixtureWeight_nonneg line 119
  10. lemma OAI.SquareDifference.tupleMixtureWeight_insert line 122
  11. def OAI.SquareDifference.tupleMixture line 130
  12. lemma OAI.SquareDifference.tupleMixture_reflection_positive line 135
  13. lemma OAI.SquareDifference.tupleMixture_symmetric line 151
  14. def OAI.SquareDifference.tupleComponentMap line 162
  15. def OAI.SquareDifference.tupleMixtureMap line 172
  16. lemma OAI.SquareDifference.tupleMixtureMap_apply line 199
  17. lemma OAI.SquareDifference.tupleMixture_nonneg line 203
  18. def OAI.SquareDifference.tupleLeadingEdges line 212
  19. def OAI.SquareDifference.tupleLeadingMassLower line 214
  20. def OAI.SquareDifference.tupleMassThreshold line 216
  21. lemma OAI.SquareDifference.tupleLeadingMassLower_pos line 219
  22. lemma OAI.SquareDifference.error_le_of_square_threshold line 221
  23. lemma OAI.SquareDifference.leading_mass_lower_of_count line 238
  24. lemma OAI.SquareDifference.tupleLeading_mass_lower line 254
  25. lemma OAI.SquareDifference.tupleMixture_mass_lower line 263
  26. lemma OAI.SquareDifference.tupleMixtureWeight_le_one line 279
  27. lemma OAI.SquareDifference.tupleMixture_mass_upper line 285
  28. def OAI.SquareDifference.tupleLaw line 299
  29. lemma OAI.SquareDifference.tupleLaw_probability line 303
  30. lemma OAI.SquareDifference.tupleLaw_nonneg line 309
  31. lemma OAI.SquareDifference.tupleLaw_reflection_positive line 314
  32. lemma OAI.SquareDifference.tupleLaw_symmetric line 323
  33. def OAI.SquareDifference.finiteIntegral line 331
  34. lemma OAI.SquareDifference.finiteIntegral_nonneg line 337
  35. lemma OAI.SquareDifference.linearFunctional_density line 341
  36. lemma OAI.SquareDifference.cut_cauchy_schwarz line 353
  37. def OAI.SquareDifference.multilinearIntegral line 383
  38. def OAI.SquareDifference.diagonalIntegral line 387
  39. lemma OAI.SquareDifference.multilinearIntegral_div line 391
  40. lemma OAI.SquareDifference.diagonalIntegral_div line 404
  41. lemma OAI.SquareDifference.holder_of_finite_maximum line 412
  42. lemma OAI.SquareDifference.prod_word_split line 456
  43. lemma OAI.SquareDifference.foldWord_half line 465
  44. lemma OAI.SquareDifference.foldWord_reflect_half line 469
  45. lemma OAI.SquareDifference.reflect_comm line 477
  46. lemma OAI.SquareDifference.foldWord_opposite_half line 482
  47. lemma OAI.SquareDifference.foldWord_opposite_reflect_half line 488
  48. def OAI.SquareDifference.halfProduct line 495