OAI/Combinatorics/SquareDifference/TupleWeights.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.expect_two_evals line 11
  2. lemma OAI.SquareDifference.tupleProjection_cycle_ne line 21
  3. lemma OAI.SquareDifference.tupleValidity_terminal line 36
  4. lemma OAI.SquareDifference.tupleComponent_pair_uniform line 42
  5. lemma OAI.SquareDifference.filtered_powerset_sum line 59
  6. lemma OAI.SquareDifference.filtered_card_split line 65
  7. def OAI.SquareDifference.tupleFamily line 79
  8. lemma OAI.SquareDifference.mem_tupleFamily line 82
  9. lemma OAI.SquareDifference.empty_mem_tupleFamily line 85
  10. lemma OAI.SquareDifference.tupleSubmixture_full line 88
  11. lemma OAI.SquareDifference.tupleSubLaw_full line 95
  12. def OAI.SquareDifference.tupleGoodLaw line 100
  13. def OAI.SquareDifference.tupleTerminalFamily line 103
  14. lemma OAI.SquareDifference.mem_tupleTerminalFamily line 106
  15. lemma OAI.SquareDifference.tupleSubmixture_split line 110
  16. def OAI.SquareDifference.tupleExceptionalLaw line 118
  17. def OAI.SquareDifference.tupleEta line 122
  18. lemma OAI.SquareDifference.tupleExceptionalLaw_nonneg line 124
  19. lemma OAI.SquareDifference.tupleEta_nonneg line 130
  20. lemma OAI.SquareDifference.tupleLaw_decomposition line 133
  21. lemma OAI.SquareDifference.tupleGoodLaw_pair line 155
  22. lemma OAI.SquareDifference.tupleExceptionalLaw_pair line 170
  23. lemma OAI.SquareDifference.tupleLaw_pair line 183
  24. lemma OAI.SquareDifference.tupleGoodLaw_probability line 190
  25. lemma OAI.SquareDifference.tupleGoodLaw_nonneg line 194
  26. lemma OAI.SquareDifference.tupleGoodLaw_marginal line 198
  27. lemma OAI.SquareDifference.tupleLaw_conditional line 203
  28. lemma OAI.SquareDifference.tupleGoodLaw_conditional line 211
  29. def OAI.SquareDifference.tupleExceptionalConstant line 218
  30. lemma OAI.SquareDifference.tupleEta_le line 221
  31. def OAI.SquareDifference.kernelForm line 259
  32. def OAI.SquareDifference.conditionalGram line 263
  33. lemma OAI.SquareDifference.kernelForm_conditionalGram line 267
  34. lemma OAI.SquareDifference.conditionalGram_symm line 290
  35. lemma OAI.SquareDifference.conditionalGram_row line 295
  36. lemma OAI.SquareDifference.kernelForm_nonneg_iff line 309
  37. lemma OAI.SquareDifference.conditionalGram_posSemidef line 335
  38. lemma OAI.SquareDifference.kernelForm_symmetric line 343
  39. lemma OAI.SquareDifference.kernelForm_const_right line 355
  40. lemma OAI.SquareDifference.kernelForm_center line 362
  41. def OAI.SquareDifference.noiseKernel line 380
  42. lemma OAI.SquareDifference.kernelForm_noise line 384
  43. lemma OAI.SquareDifference.centered_square_mean line 401
  44. lemma OAI.SquareDifference.conditionalGram_noise_domination line 407
  45. lemma OAI.SquareDifference.matrix_prod_monotone line 430
  46. lemma OAI.SquareDifference.product_kernel_monotone line 467
  47. lemma OAI.SquareDifference.expect_update_dep line 480
  48. def OAI.SquareDifference.coordOp line 495
  49. def OAI.SquareDifference.patch line 501
  50. lemma OAI.SquareDifference.patch_empty line 504
  51. lemma OAI.SquareDifference.patch_univ line 507