OAI/Probability/LogConcave/JetEstimates/TensorTerm.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.polynomialTime_smooth line 12
  2. structure OAI.LogConcaveSampling.TensorTerm line 18
  3. def OAI.LogConcaveSampling.TensorTerm.eval line 26
  4. lemma OAI.LogConcaveSampling.TensorTerm.timeSmooth line 30
  5. def OAI.LogConcaveSampling.TensorTerm.relabel line 38
  6. lemma OAI.LogConcaveSampling.TensorTerm.relabel_eval line 41
  7. def OAI.LogConcaveSampling.TensorTerm.scale line 45
  8. lemma OAI.LogConcaveSampling.TensorTerm.scale_eval line 48
  9. def OAI.LogConcaveSampling.TensorTerm.adjoint line 54
  10. lemma OAI.LogConcaveSampling.TensorTerm.adjoint_eval line 57
  11. def OAI.LogConcaveSampling.TensorTerm.contract line 80
  12. lemma OAI.LogConcaveSampling.TensorTerm.contract_eval line 84
  13. structure OAI.LogConcaveSampling.TensorSum line 97
  14. instance OAI.LogConcaveSampling.TensorSum.(instance at line 104) line 104
  15. def OAI.LogConcaveSampling.TensorSum.eval line 106
  16. def OAI.LogConcaveSampling.TensorSum.weightLE line 109
  17. lemma OAI.LogConcaveSampling.TensorSum.timeSmooth line 111
  18. def OAI.LogConcaveSampling.TensorSum.pure line 118
  19. lemma OAI.LogConcaveSampling.TensorSum.pure_eval line 119
  20. def OAI.LogConcaveSampling.TensorSum.add line 125
  21. lemma OAI.LogConcaveSampling.TensorSum.add_eval line 126
  22. def OAI.LogConcaveSampling.TensorSum.relabel line 133
  23. lemma OAI.LogConcaveSampling.TensorSum.relabel_eval line 135
  24. def OAI.LogConcaveSampling.TensorSum.scale line 139
  25. lemma OAI.LogConcaveSampling.TensorSum.scale_eval line 141
  26. def OAI.LogConcaveSampling.TensorSum.adjoint line 147
  27. lemma OAI.LogConcaveSampling.TensorSum.adjoint_eval line 150
  28. def OAI.LogConcaveSampling.TensorSum.contract line 164
  29. lemma OAI.LogConcaveSampling.TensorSum.contract_eval line 168
  30. lemma OAI.LogConcaveSampling.jointMean_direction line 196
  31. def OAI.LogConcaveSampling.TensorAtom.one line 211
  32. lemma OAI.LogConcaveSampling.TensorAtom.one_weight line 214
  33. lemma OAI.LogConcaveSampling.TensorAtom.one_eval line 216
  34. def OAI.LogConcaveSampling.TensorAtom.insertOne line 225
  35. lemma OAI.LogConcaveSampling.TensorAtom.insertOne_weight line 228
  36. lemma OAI.LogConcaveSampling.TensorAtom.insertOne_eval line 232
  37. lemma OAI.LogConcaveSampling.TensorAtom.insertOne_mean line 243
  38. lemma OAI.LogConcaveSampling.JetCalculus.gadj_slice_congr_at line 260