OAI/Probability/LogConcave/JetEstimates/ArrayMatrix.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.TensorEnergy.arrayMatrix line 16
  2. lemma OAI.LogConcaveSampling.TensorEnergy.matrixArray_arrayMatrix line 19
  3. lemma OAI.LogConcaveSampling.TensorEnergy.matrixArray_injective line 35
  4. lemma OAI.LogConcaveSampling.TensorEnergy.arrayMatrix_matrixArray line 48
  5. lemma OAI.LogConcaveSampling.TensorEnergy.arrayMatrix_add line 52
  6. lemma OAI.LogConcaveSampling.TensorEnergy.arrayMatrix_smul line 57
  7. def OAI.LogConcaveSampling.TensorSum.matrixEval line 65
  8. lemma OAI.LogConcaveSampling.TensorSum.matrixEval_add line 69
  9. lemma OAI.LogConcaveSampling.TensorSum.matrixEval_scale line 75
  10. def OAI.LogConcaveSampling.TensorSum.matrixComp line 82
  11. lemma OAI.LogConcaveSampling.TensorSum.matrixComp_weight line 85
  12. lemma OAI.LogConcaveSampling.TensorSum.matrixEval_comp line 89
  13. lemma OAI.LogConcaveSampling.TensorSum.matrixEval_smoothAt line 101
  14. lemma OAI.LogConcaveSampling.TensorSum.HasMaterial.matrixEval_path line 113
  15. def OAI.LogConcaveSampling.TensorSum.firstMatrix line 135
  16. lemma OAI.LogConcaveSampling.TensorSum.firstMatrix_weight line 139
  17. lemma OAI.LogConcaveSampling.TensorSum.firstMatrix_eval line 144
  18. def OAI.LogConcaveSampling.TensorSum.material line 159
  19. lemma OAI.LogConcaveSampling.TensorSum.material_weight line 161
  20. lemma OAI.LogConcaveSampling.TensorSum.material_spec line 163
  21. def OAI.LogConcaveSampling.TensorSum.terminalQ line 166
  22. lemma OAI.LogConcaveSampling.TensorSum.terminalQ_zero_eval line 176
  23. lemma OAI.LogConcaveSampling.TensorSum.terminalQ_succ_eval line 182
  24. lemma OAI.LogConcaveSampling.terminalJacobian_first_Q line 199
  25. lemma OAI.LogConcaveSampling.terminalJacobian_Q_deriv line 210
  26. theorem OAI.LogConcaveSampling.terminalJacobian_iteratedDeriv_Q line 233
  27. theorem OAI.LogConcaveSampling.terminalJacobian_iteratedDeriv_Q_closed line 254
  28. lemma OAI.LogConcaveSampling.TensorEnergy.matrixArray_mulVec line 301
  29. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.matrixArray_norm_le line 314
  30. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.of_spatialTensor_zero line 328
  31. lemma OAI.LogConcaveSampling.TensorSum.matrixEval_norm_le line 353
  32. lemma OAI.LogConcaveSampling.terminalBackward_measurePreserving line 368
  33. lemma OAI.LogConcaveSampling.terminalJacobian_iteratedDeriv_norm_le line 379
  34. theorem OAI.LogConcaveSampling.terminalJacobian_iteratedDeriv_eLpNorm line 396