OAI/Geometry/LatticeCovering/RadialBounds.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Prekopa.radial_integral_set line 17
  2. lemma OAI.SingleLatticeCovering.Prekopa.weighted_profile_tendsto_zero line 34
  3. theorem OAI.SingleLatticeCovering.Prekopa.ScalarLogConcave.exists_shell_radius line 58
  4. def OAI.SingleLatticeCovering.Radial.radialInf line 95
  5. lemma OAI.SingleLatticeCovering.Radial.radialInf_bddBelow line 98
  6. lemma OAI.SingleLatticeCovering.Radial.radialInf_nonneg line 102
  7. lemma OAI.SingleLatticeCovering.Radial.radialInf_le line 107
  8. lemma OAI.SingleLatticeCovering.Radial.radialInf_le_self line 111
  9. lemma OAI.SingleLatticeCovering.Radial.radialInf_invariant line 114
  10. lemma OAI.SingleLatticeCovering.Radial.radialInf_norm_eq line 125
  11. lemma OAI.SingleLatticeCovering.Radial.radialInf_upperSemicontinuous line 131
  12. lemma OAI.SingleLatticeCovering.Radial.radialInf_logConcave line 136
  13. lemma OAI.SingleLatticeCovering.Radial.radialInf_approximation line 149
  14. lemma OAI.SingleLatticeCovering.Radial.logConcave_min line 163
  15. lemma OAI.SingleLatticeCovering.Radial.radialInf_smul_mono line 178
  16. lemma OAI.SingleLatticeCovering.Radial.radialInf_abs_sub_le line 199
  17. lemma OAI.SingleLatticeCovering.Radial.continuous_radialInf line 215
  18. lemma OAI.SingleLatticeCovering.Radial.radialInf_pos line 241
  19. lemma OAI.SingleLatticeCovering.Radial.radialInf_integrable line 258
  20. lemma OAI.SingleLatticeCovering.Radial.scalarLogConcave_profile line 264
  21. theorem OAI.SingleLatticeCovering.Radial.radialInf_shell_radius line 271
  22. lemma OAI.SingleLatticeCovering.Radial.setIntegral_transfer_error line 309
  23. lemma OAI.SingleLatticeCovering.Radial.radialInf_integral_le line 339
  24. theorem OAI.SingleLatticeCovering.Radial.radial_model_shell line 347
  25. lemma OAI.SingleLatticeCovering.Prekopa.euclidean_sq_weighted line 386
  26. def OAI.SingleLatticeCovering.Prekopa.smoothingKernel line 397
  27. lemma OAI.SingleLatticeCovering.Prekopa.smoothingKernel_positive line 400
  28. lemma OAI.SingleLatticeCovering.Prekopa.smoothingKernel_le_one line 403
  29. lemma OAI.SingleLatticeCovering.Prekopa.continuous_smoothingKernel line 408
  30. lemma OAI.SingleLatticeCovering.Prekopa.continuous_smoothingKernel_right line 413
  31. lemma OAI.SingleLatticeCovering.Prekopa.smoothingKernel_weighted line 418
  32. lemma OAI.SingleLatticeCovering.Prekopa.soft_smoothing_gaussianBound line 431
  33. lemma OAI.SingleLatticeCovering.Prekopa.soft_smoothing_integral_tendsto line 441
  34. lemma OAI.SingleLatticeCovering.Prekopa.soft_smoothing_integral_inequality line 463
  35. theorem OAI.SingleLatticeCovering.Prekopa.logConcave_smoothed_volume line 495
  36. lemma OAI.SingleLatticeCovering.Prekopa.tail_quantiles_of_second_moment line 520
  37. lemma OAI.SingleLatticeCovering.Prekopa.scalar_tail_of_second_moment line 542
  38. lemma OAI.SingleLatticeCovering.Prekopa.scalar_abs_tail line 550
  39. lemma OAI.SingleLatticeCovering.Prekopa.lintegral_fourth_eq_tails line 567
  40. def OAI.SingleLatticeCovering.Prekopa.fourthMomentConstant line 582
  41. lemma OAI.SingleLatticeCovering.Prekopa.fourth_weight_integrable line 584
  42. lemma OAI.SingleLatticeCovering.Prekopa.fourth_weight_integral line 589
  43. lemma OAI.SingleLatticeCovering.Prekopa.lintegral_fourth_le line 596
  44. lemma OAI.SingleLatticeCovering.Prekopa.fourth_moment_bound line 620