OAI/Geometry/LatticeCovering/ProjectionBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.GaussianProjection.integrable_normalizedProjection line 11
  2. lemma OAI.SingleLatticeCovering.GaussianProjection.integral_normalizedProjection line 19
  3. lemma OAI.SingleLatticeCovering.GaussianProjection.continuous_normalizedProjection line 26
  4. lemma OAI.SingleLatticeCovering.GaussianProjection.normalizedProjection_pos line 31
  5. def OAI.SingleLatticeCovering.GaussianProjection.scaleVariance line 53
  6. lemma OAI.SingleLatticeCovering.GaussianProjection.scaleVariance_pos line 56
  7. lemma OAI.SingleLatticeCovering.GaussianProjection.scaleVariance_integrable line 62
  8. lemma OAI.SingleLatticeCovering.GaussianProjection.scaleVariance_mean line 69
  9. def OAI.SingleLatticeCovering.GaussianProjection.normalizedModel line 79
  10. lemma OAI.SingleLatticeCovering.GaussianProjection.normalizedModel_mixture line 83
  11. def OAI.SingleLatticeCovering.GaussianProjection.projectionError line 88
  12. lemma OAI.SingleLatticeCovering.GaussianProjection.projectionError_nonneg line 91
  13. lemma OAI.SingleLatticeCovering.GaussianProjection.exists_normalized_projection line 95
  14. theorem OAI.SingleLatticeCovering.GaussianProjection.actual_model_shell line 111
  15. lemma OAI.SingleLatticeCovering.GaussianDensity.probability_interval_lower line 158
  16. theorem OAI.SingleLatticeCovering.GaussianDensity.mixture_shell_scales line 175
  17. lemma OAI.SingleLatticeCovering.GaussianDensity.good_scale_anchors line 217
  18. lemma OAI.SingleLatticeCovering.GaussianDensity.scale_interval_ratio line 248
  19. lemma OAI.SingleLatticeCovering.GaussianDensity.scale_ratio_le_two line 265
  20. def OAI.SingleLatticeCovering.GaussianProjection.shellError line 283
  21. def OAI.SingleLatticeCovering.GaussianProjection.shellLoss line 288
  22. lemma OAI.SingleLatticeCovering.GaussianProjection.scaleVariance_measurable line 291
  23. theorem OAI.SingleLatticeCovering.GaussianProjection.actual_good_scales line 298
  24. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_ratio line 353
  25. lemma OAI.SingleLatticeCovering.GaussianDensity.inverse_scale_ratio_lower line 362
  26. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_ratio_lower line 380
  27. lemma OAI.SingleLatticeCovering.GaussianDensity.normalizer_variance_mono line 411
  28. lemma OAI.SingleLatticeCovering.GaussianDensity.density_variance_le_peak line 419
  29. lemma OAI.SingleLatticeCovering.GaussianDensity.integrable_mixture_at line 428
  30. lemma OAI.SingleLatticeCovering.GaussianDensity.density_scales_lower line 439
  31. theorem OAI.SingleLatticeCovering.GaussianDensity.mixture_lower line 459
  32. theorem OAI.SingleLatticeCovering.GaussianProjection.actual_smoothed_lower line 495
  33. def OAI.SingleLatticeCovering.GaussianDensity.densityFloor line 535
  34. lemma OAI.SingleLatticeCovering.GaussianDensity.densityFloor_pos line 538
  35. lemma OAI.SingleLatticeCovering.GaussianDensity.variance_density_floor line 542
  36. lemma OAI.SingleLatticeCovering.GaussianDensity.variance_density_nearby line 557
  37. lemma OAI.SingleLatticeCovering.GaussianProjection.surjective_of_smoothed_lower line 603