OAI/Probability/LogConcave/JetEstimates/Squared.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.TensorEnergy.sum_fintype_irrel line 15
  2. def OAI.LogConcaveSampling.TensorEnergy.squared line 20
  3. lemma OAI.LogConcaveSampling.TensorEnergy.squared_nonneg line 21
  4. lemma OAI.LogConcaveSampling.TensorEnergy.squared_reindex line 23
  5. lemma OAI.LogConcaveSampling.TensorEnergy.squared_sum line 26
  6. lemma OAI.LogConcaveSampling.TensorEnergy.squared_add line 32
  7. lemma OAI.LogConcaveSampling.TensorEnergy.squared_zero line 37
  8. def OAI.LogConcaveSampling.spatialSquared line 42
  9. lemma OAI.LogConcaveSampling.spatialSquared_nonneg line 45
  10. lemma OAI.LogConcaveSampling.spatialSquared_full line 48
  11. lemma OAI.LogConcaveSampling.extendedSpatial_squared line 65
  12. lemma OAI.LogConcaveSampling.spatialContractTerm_squared line 70
  13. lemma OAI.LogConcaveSampling.spatialSquared_contract line 92
  14. lemma OAI.LogConcaveSampling.PolySmooth.sq line 149
  15. lemma OAI.LogConcaveSampling.spatialSquared_polySmooth line 152
  16. def OAI.LogConcaveSampling.spatialEnergy line 157
  17. lemma OAI.LogConcaveSampling.spatialEnergy_nonneg line 160
  18. lemma OAI.LogConcaveSampling.singleContract_polySmooth line 164
  19. lemma OAI.LogConcaveSampling.spatialEnergy_contract line 172
  20. def OAI.LogConcaveSampling.insideZeroColor line 189
  21. def OAI.LogConcaveSampling.insideOneColor line 196
  22. lemma OAI.LogConcaveSampling.spatialInside_zero_squared line 205
  23. lemma OAI.LogConcaveSampling.spatialInside_one_squared line 212
  24. lemma OAI.LogConcaveSampling.spatialAdjointLeading_energy line 231