OAI/Computability/MinUncut/Analysis/GaussianDensityError.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.FiniteGaussian.baseDensity line 11
  2. def OAI.MinUncut.FiniteGaussian.gIntegral line 12
  3. lemma OAI.MinUncut.FiniteGaussian.continuous_baseDensity line 14
  4. lemma OAI.MinUncut.FiniteGaussian.gIntegral_pos line 16
  5. lemma OAI.MinUncut.FiniteGaussian.gIntegral_large line 21
  6. lemma OAI.MinUncut.FiniteGaussian.residual_bounds line 42
  7. def OAI.MinUncut.FiniteGaussian.gCell line 68
  8. def OAI.MinUncut.FiniteGaussian.qCell line 71
  9. lemma OAI.MinUncut.FiniteGaussian.sum_gCell line 74
  10. lemma OAI.MinUncut.FiniteGaussian.sum_qCell line 83
  11. lemma OAI.MinUncut.FiniteGaussian.gCell_nonneg line 90
  12. lemma OAI.MinUncut.FiniteGaussian.gCell_le_qCell line 94
  13. lemma OAI.MinUncut.FiniteGaussian.grid_product_bound line 105
  14. abbrev OAI.MinUncut.FiniteGaussian.gaussianConstant line 123
  15. lemma OAI.MinUncut.FiniteGaussian.gaussianConstant_pos line 125
  16. lemma OAI.MinUncut.FiniteGaussian.gaussian_Ioc line 128
  17. lemma OAI.MinUncut.FiniteGaussian.gaussian_cube_pos line 139
  18. lemma OAI.MinUncut.FiniteGaussian.gaussian_cube line 149
  19. lemma OAI.MinUncut.FiniteGaussian.gaussian_cubeCell line 158