OAI/Combinatorics/SquareDifference/ProductBounds.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.patch_insert_update line 11
  2. def OAI.SquareDifference.partialOp line 19
  3. lemma OAI.SquareDifference.partialOp_empty line 25
  4. lemma OAI.SquareDifference.partialOp_smul line 30
  5. lemma OAI.SquareDifference.partialOp_insert line 37
  6. lemma OAI.SquareDifference.partialOp_eigen line 60
  7. lemma OAI.SquareDifference.product_kernel_eigen line 70
  8. def OAI.SquareDifference.ExactSupport line 77
  9. lemma OAI.SquareDifference.coordOp_noise line 83
  10. lemma OAI.SquareDifference.noise_product_exactSupport line 97
  11. lemma OAI.SquareDifference.exactSupport_orthogonal line 115
  12. lemma OAI.SquareDifference.orthogonal_sum_square line 130
  13. lemma OAI.SquareDifference.kernelForm_eigen_sum line 142
  14. lemma OAI.SquareDifference.noise_product_bound line 163
  15. lemma OAI.SquareDifference.expect_prod_pi line 178
  16. lemma OAI.SquareDifference.conditionalGram_product line 185
  17. lemma OAI.SquareDifference.tensor_conditional_decay line 199
  18. lemma OAI.SquareDifference.conditional_bilinear_sq line 239
  19. lemma OAI.SquareDifference.prod_le_average_powers line 270
  20. lemma OAI.SquareDifference.positiveLaw_mono line 286
  21. lemma OAI.SquareDifference.positiveLaw_abs line 293
  22. lemma OAI.SquareDifference.positiveLaw_product_bound line 302
  23. lemma OAI.SquareDifference.tensorLaw_density line 332
  24. lemma OAI.SquareDifference.jointDensity_tensor line 349
  25. lemma OAI.SquareDifference.tensorLaw_conditional_decay line 366
  26. lemma OAI.SquareDifference.law_slot_bilinear_sq line 401
  27. lemma OAI.SquareDifference.law_slot_product_sq line 416
  28. lemma OAI.SquareDifference.tensorLaw_marginal line 443
  29. lemma OAI.SquareDifference.tensorLaw_prime_conductor_energy line 471
  30. lemma OAI.SquareDifference.tupleGoodTensor_conductor_energy line 496
  31. lemma OAI.SquareDifference.tupleTensor_conductor_energy line 510