OAI/Combinatorics/SquareDifference/AffineTuples.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareDifference.affineEquiv line 11
  2. lemma OAI.SquareDifference.tupleComponent_affine line 17
  3. lemma OAI.SquareDifference.tupleMixture_affine line 37
  4. lemma OAI.SquareDifference.tupleLaw_affine line 43
  5. lemma OAI.SquareDifference.invariant_marginal_uniform line 49
  6. lemma OAI.SquareDifference.tupleLaw_marginal line 75
  7. lemma OAI.SquareDifference.diagonalRoot_one line 83
  8. lemma OAI.SquareDifference.holder_mean line 88
  9. lemma OAI.SquareDifference.lawDensity_equiv line 108
  10. lemma OAI.SquareDifference.tensorLaw_equiv line 116
  11. lemma OAI.SquareDifference.productTupleLaw_affine line 136
  12. lemma OAI.SquareDifference.productTupleLaw_probability line 144
  13. lemma OAI.SquareDifference.productTupleLaw_marginal line 149
  14. lemma OAI.SquareDifference.productTupleLaw_mean line 160
  15. lemma OAI.SquareDifference.weighted_expect_cauchy line 169
  16. lemma OAI.SquareDifference.weighted_expect_cauchy_le line 180
  17. lemma OAI.SquareDifference.ratio_energy_pointwise line 189
  18. lemma OAI.SquareDifference.bayes_energy_bound line 211
  19. def OAI.SquareDifference.conditionalEnergy line 232
  20. lemma OAI.SquareDifference.conditionalEnergy_nonneg line 236
  21. lemma OAI.SquareDifference.conditionalEnergy_le line 241
  22. lemma OAI.SquareDifference.conditionalEnergy_uniform line 256
  23. lemma OAI.SquareDifference.ratio_add_le line 264
  24. lemma OAI.SquareDifference.conditionalEnergy_add_le line 280
  25. lemma OAI.SquareDifference.conditionalEnergy_smul line 302
  26. lemma OAI.SquareDifference.conditionalEnergy_leading line 314
  27. lemma OAI.SquareDifference.bilinear_l2_bound line 338
  28. lemma OAI.SquareDifference.list_mixing_l2 line 365
  29. lemma OAI.SquareDifference.listKernel_nonneg line 378
  30. lemma OAI.SquareDifference.listKernel_le_one line 385
  31. lemma OAI.SquareDifference.list_conditional_mixing line 392
  32. def OAI.SquareDifference.jointDensity line 416
  33. lemma OAI.SquareDifference.lawDensity_expect line 420
  34. lemma OAI.SquareDifference.jointDensity_integral line 429
  35. lemma OAI.SquareDifference.jointDensity_nonneg line 439
  36. lemma OAI.SquareDifference.jointDensity_marginal line 446
  37. lemma OAI.SquareDifference.jointDensity_uniform line 469
  38. lemma OAI.SquareDifference.conditionalEnergy_equiv line 478
  39. def OAI.SquareDifference.splitIndex line 491
  40. def OAI.SquareDifference.crossEdges line 500
  41. def OAI.SquareDifference.crossDir line 504