OAI/Combinatorics/SquareDifference/WordReflection.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.prod_word_fold line 11
  2. lemma OAI.SquareDifference.prod_word_opposite_fold line 21
  3. lemma OAI.SquareDifference.wordIntegral_folding line 32
  4. lemma OAI.SquareDifference.word_diagonal_nonneg line 61
  5. lemma OAI.SquareDifference.word_signed_holder line 73
  6. lemma OAI.SquareDifference.tupleLaw_diagonal_nonneg line 99
  7. lemma OAI.SquareDifference.tupleLaw_signed_holder line 106
  8. lemma OAI.SquareDifference.multilinearIntegral_sum line 114
  9. lemma OAI.SquareDifference.diagonalIntegral_smul line 126
  10. def OAI.SquareDifference.diagonalRoot line 133
  11. lemma OAI.SquareDifference.diagonalRoot_nonneg line 137
  12. lemma OAI.SquareDifference.diagonalRoot_pow line 142
  13. lemma OAI.SquareDifference.diagonalRoot_smul line 150
  14. lemma OAI.SquareDifference.diagonalIntegral_add_le line 162
  15. lemma OAI.SquareDifference.diagonalRoot_add_le line 183
  16. def OAI.SquareDifference.functionalSeminorm line 196
  17. def OAI.SquareDifference.cutKernel line 205
  18. lemma OAI.SquareDifference.cut_form_eq_sum line 209
  19. lemma OAI.SquareDifference.cutKernel_posSemidef line 229
  20. lemma OAI.SquareDifference.matrix_prod_posSemidef line 251
  21. lemma OAI.SquareDifference.cut_positive_of_kernel line 274
  22. lemma OAI.SquareDifference.cut_symmetric_of_kernel line 283
  23. def OAI.SquareDifference.lawDensity line 299
  24. def OAI.SquareDifference.tensorLaw line 303
  25. lemma OAI.SquareDifference.tensorLaw_fubini line 311
  26. lemma OAI.SquareDifference.tensorLaw_probability line 323
  27. lemma OAI.SquareDifference.tensorLaw_nonneg line 331
  28. lemma OAI.SquareDifference.prod_indicator_forall line 343
  29. lemma OAI.SquareDifference.tensorLaw_cutKernel line 353
  30. lemma OAI.SquareDifference.tensorLaw_cut_positive line 381
  31. lemma OAI.SquareDifference.tensorLaw_word_symmetric line 405
  32. lemma OAI.SquareDifference.tensorLaw_word_positive line 430
  33. def OAI.SquareDifference.productTupleLaw line 448
  34. lemma OAI.SquareDifference.productTupleLaw_diagonal_nonneg line 453
  35. lemma OAI.SquareDifference.productTupleLaw_signed_holder line 464
  36. lemma OAI.SquareDifference.squareIndicator_mul_sq line 479
  37. lemma OAI.SquareDifference.tupleValidity_affine line 499