OAI/Probability/LogConcave/JetEstimates/TensorExpression.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.LogConcaveSampling.TensorExpression line 13
  2. def OAI.LogConcaveSampling.TensorExpression.weight line 22
  3. def OAI.LogConcaveSampling.TensorExpression.eval line 28
  4. lemma OAI.LogConcaveSampling.TensorExpression.eval_polySmooth line 38
  5. def OAI.LogConcaveSampling.TensorExpression.physicalBase line 48
  6. lemma OAI.LogConcaveSampling.TensorExpression.physicalBase_polySmooth line 52
  7. lemma OAI.LogConcaveSampling.TensorExpression.physicalBase_eq_U line 74
  8. def OAI.LogConcaveSampling.TensorExpression.jointBase line 97
  9. lemma OAI.LogConcaveSampling.TensorExpression.jointBase_slice line 102
  10. lemma OAI.LogConcaveSampling.TensorExpression.jointBase_timeSmooth line 108
  11. def OAI.LogConcaveSampling.TensorExpression.jointEval line 131
  12. lemma OAI.LogConcaveSampling.TensorExpression.jointEval_timeSmooth line 141
  13. lemma OAI.LogConcaveSampling.TensorExpression.jointEval_slice line 156
  14. structure OAI.LogConcaveSampling.TensorAtom line 195
  15. def OAI.LogConcaveSampling.TensorAtom.eval line 204
  16. def OAI.LogConcaveSampling.TensorAtom.relabel line 207
  17. lemma OAI.LogConcaveSampling.TensorAtom.relabel_eval line 210
  18. def OAI.LogConcaveSampling.TensorAtom.reindex line 214
  19. lemma OAI.LogConcaveSampling.TensorAtom.reindex_eval line 220
  20. lemma OAI.LogConcaveSampling.TensorAtom.reindex_weight line 228
  21. def OAI.LogConcaveSampling.TensorAtom.lastEquiv line 235
  22. lemma OAI.LogConcaveSampling.TensorAtom.lastEquiv_castSucc line 238
  23. lemma OAI.LogConcaveSampling.TensorAtom.lastEquiv_last line 241
  24. lemma OAI.LogConcaveSampling.TensorAtom.lastEquiv_snoc line 244
  25. def OAI.LogConcaveSampling.TensorAtom.contract line 252
  26. lemma OAI.LogConcaveSampling.TensorAtom.contract_weight line 260
  27. lemma OAI.LogConcaveSampling.TensorAtom.contract_eval line 265
  28. def OAI.LogConcaveSampling.TensorAtom.adjoint line 287
  29. lemma OAI.LogConcaveSampling.TensorAtom.adjoint_weight line 291
  30. lemma OAI.LogConcaveSampling.TensorAtom.adjoint_eval line 295