OAI/Probability/LogConcave/Sampling/TensorVector.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.lie_chain line 16
  2. def OAI.LogConcaveSampling.tensorVector line 35
  3. lemma OAI.LogConcaveSampling.tensorVector_norm_sq line 38
  4. lemma OAI.LogConcaveSampling.tensorVector_contDiff line 42
  5. lemma OAI.LogConcaveSampling.lie_vector_chain line 48
  6. def OAI.LogConcaveSampling.leftCoordinates line 73
  7. def OAI.LogConcaveSampling.rightCoordinates line 74
  8. lemma OAI.LogConcaveSampling.coordinateProjection_left line 76
  9. lemma OAI.LogConcaveSampling.coordinateProjection_right line 80
  10. lemma OAI.LogConcaveSampling.productPointEquiv_basis_left line 85
  11. lemma OAI.LogConcaveSampling.productPointEquiv_basis_right line 97
  12. lemma OAI.LogConcaveSampling.directional_comp_linear line 110
  13. lemma OAI.LogConcaveSampling.productPotential_directional_left line 116
  14. lemma OAI.LogConcaveSampling.productPotential_directional_right line 139
  15. lemma OAI.LogConcaveSampling.spatialEnergy_leftLift line 175
  16. def OAI.LogConcaveSampling.jointSkewEntry line 206
  17. def OAI.LogConcaveSampling.jointSkew line 216
  18. lemma OAI.LogConcaveSampling.jointSkew_skew line 220
  19. lemma OAI.LogConcaveSampling.jointSkew_polySmooth line 227
  20. lemma OAI.LogConcaveSampling.skewLieField_coordinate line 243
  21. lemma OAI.LogConcaveSampling.directional_gaussianPotential line 249
  22. lemma OAI.LogConcaveSampling.adjointCoordinate_const_mul line 258
  23. lemma OAI.LogConcaveSampling.adjointCoordinate_zero line 268
  24. def OAI.LogConcaveSampling.pairLabels line 285
  25. lemma OAI.LogConcaveSampling.eq_pairLabels line 287
  26. lemma OAI.LogConcaveSampling.pair_lift_in line 291
  27. lemma OAI.LogConcaveSampling.pair_lift_out_left line 300
  28. lemma OAI.LogConcaveSampling.pair_lift_out_right line 306
  29. lemma OAI.LogConcaveSampling.left_not_right line 313
  30. lemma OAI.LogConcaveSampling.right_not_left line 318
  31. lemma OAI.LogConcaveSampling.jointSkew_eq_lifts line 324
  32. lemma OAI.LogConcaveSampling.spatialTensor_add line 367
  33. theorem OAI.LogConcaveSampling.jointSkew_spatial_bound line 376
  34. theorem OAI.LogConcaveSampling.centering_jointSkew_spatial_bound line 409
  35. lemma OAI.LogConcaveSampling.scoreLabels_eq line 435
  36. lemma OAI.LogConcaveSampling.scalarSlot_lift_in line 442
  37. lemma OAI.LogConcaveSampling.scalarSlot_lift_out line 449
  38. lemma OAI.LogConcaveSampling.scoreField_product line 456
  39. lemma OAI.LogConcaveSampling.scoreField_product_allSplit line 474