OAI/Probability/LogConcave/JetEstimates/ReindexedMatrix.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.sum_norm line 15
  2. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.sum line 26
  3. lemma OAI.LogConcaveSampling.TensorEnergy.splitEnvelope_le_pow line 33
  4. lemma OAI.LogConcaveSampling.natural_moment_sum_finset line 40
  5. lemma OAI.LogConcaveSampling.natural_moment_mul line 62
  6. lemma OAI.LogConcaveSampling.natural_moment_const_mul line 83
  7. def OAI.LogConcaveSampling.TensorEnergy.reindexedMatrix line 105
  8. lemma OAI.LogConcaveSampling.TensorEnergy.matrix_norm_reindex line 108
  9. def OAI.LogConcaveSampling.TensorEnergy.splitFin line 116
  10. lemma OAI.LogConcaveSampling.TensorEnergy.spatialAdjoint_matrix_norm line 121
  11. theorem OAI.LogConcaveSampling.spatialAdjoint_split_eLpNorm line 142
  12. lemma OAI.LogConcaveSampling.spatialAdjoint_polySmooth line 180
  13. lemma OAI.LogConcaveSampling.traceDimensionRoot line 186
  14. theorem OAI.LogConcaveSampling.spatialAdjoint_envelope_moment line 200