OAI/Probability/LogConcave/JetEstimates/Slice.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.TensorAtom.slice line 17
  2. lemma OAI.LogConcaveSampling.TensorAtom.slice_polySmooth line 21
  3. def OAI.LogConcaveSampling.TensorAtom.spatialBound line 30
  4. lemma OAI.LogConcaveSampling.TensorAtom.spatialBound_nonneg line 35
  5. lemma OAI.LogConcaveSampling.TensorAtom.spatialBound_measurable line 40
  6. lemma OAI.LogConcaveSampling.TensorAtom.spatialBound_allSplit line 48
  7. lemma OAI.LogConcaveSampling.TensorAtom.spatialBound_Lp line 65
  8. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.abs_const_mul line 81
  9. lemma OAI.LogConcaveSampling.spatialTensor_const_mul line 89
  10. lemma OAI.LogConcaveSampling.spatialTensor_sum line 97
  11. def OAI.LogConcaveSampling.TensorSum.slice line 107
  12. def OAI.LogConcaveSampling.TensorSum.spatialBound line 110
  13. lemma OAI.LogConcaveSampling.TensorSum.spatialBound_nonneg line 115
  14. lemma OAI.LogConcaveSampling.TensorSum.spatialBound_measurable line 120
  15. lemma OAI.LogConcaveSampling.TensorSum.slice_polySmooth line 128
  16. lemma OAI.LogConcaveSampling.TensorSum.spatialBound_allSplit line 138
  17. def OAI.LogConcaveSampling.TensorSum.momentBudget line 175
  18. lemma OAI.LogConcaveSampling.TensorSum.momentBudget_ne_top line 182
  19. lemma OAI.LogConcaveSampling.TensorSum.spatialBound_Lp line 191
  20. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.frobeniusSquared_row line 239
  21. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.frobeniusSquared line 246