OAI/Probability/LogConcave/JetEstimates/ForestTensor.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.singleContract_frobenius line 12
  2. def OAI.LogConcaveSampling.TensorEnergy.forestTensor line 48
  3. def OAI.LogConcaveSampling.TensorEnergy.forestRoot line 54
  4. def OAI.LogConcaveSampling.TensorEnergy.forestBranches line 66
  5. def OAI.LogConcaveSampling.TensorEnergy.forestShuffle line 76
  6. def OAI.LogConcaveSampling.TensorEnergy.forestOutput line 80
  7. def OAI.LogConcaveSampling.TensorEnergy.forestColours line 86
  8. lemma OAI.LogConcaveSampling.TensorEnergy.forestTensor_succ line 92
  9. theorem OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.forest line 131
  10. def OAI.LogConcaveSampling.TensorEnergy.multilinearTensor line 174
  11. lemma OAI.LogConcaveSampling.TensorEnergy.multilinear_coordinate_expansion line 179
  12. lemma OAI.LogConcaveSampling.TensorEnergy.multilinearTensor_compAlong line 198
  13. theorem OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.compAlong line 210
  14. theorem OAI.LogConcaveSampling.TensorEnergy.iteratedFDeriv_comp_allSplit line 225
  15. lemma OAI.LogConcaveSampling.JetCalculus.jet_eq_iteratedFDeriv line 256
  16. lemma OAI.LogConcaveSampling.JetCalculus.jet_finRange_eq_iteratedFDeriv line 267
  17. lemma OAI.LogConcaveSampling.multilinearTensor_iterated_mean line 281
  18. lemma OAI.LogConcaveSampling.conditionalMean_iterated_allSplit line 300
  19. def OAI.LogConcaveSampling.TensorEnergy.arrayTensor line 335
  20. lemma OAI.LogConcaveSampling.TensorEnergy.arrayTensor_coordinate_expansion line 341
  21. lemma OAI.LogConcaveSampling.TensorEnergy.arrayTensor_compAlong line 355
  22. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.array_compAlong line 367
  23. lemma OAI.LogConcaveSampling.TensorEnergy.iteratedFDeriv_array_comp_allSplit line 383
  24. lemma OAI.LogConcaveSampling.TensorEnergy.spatialTensor_eq_arrayTensor line 401
  25. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.of_spatialTensor line 412