OAI/Combinatorics/BooleanFunctions/SmoothGaussian.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareRootDegree.SmoothGaussian.tent line 16

    Source documentation

    A continuous probability of passing a rare interval test. It vanishes outside the interval, and is rounded to deterministic tests on each finite input alphabet before constructing any final observation.

    def tent (a h x : ℝ) : ℝ := max 0 (1 - |x-a| / h)
  2. theorem OAI.SquareRootDegree.SmoothGaussian.continuous_tent line 18
  3. theorem OAI.SquareRootDegree.SmoothGaussian.tent_nonneg line 22
  4. theorem OAI.SquareRootDegree.SmoothGaussian.tent_le_one line 24
  5. theorem OAI.SquareRootDegree.SmoothGaussian.tent_eq_zero line 29
  6. theorem OAI.SquareRootDegree.SmoothGaussian.tent_ne_zero_iff line 36
  7. theorem OAI.SquareRootDegree.SmoothGaussian.tent_support line 47
  8. theorem OAI.SquareRootDegree.SmoothGaussian.tent_compactSupport line 54
  9. theorem OAI.SquareRootDegree.SmoothGaussian.tent_half line 60
  10. theorem OAI.SquareRootDegree.SmoothGaussian.integrable_tent_mul line 66
  11. theorem OAI.SquareRootDegree.SmoothGaussian.pdf_lower line 72
  12. theorem OAI.SquareRootDegree.SmoothGaussian.beta_lower line 80
  13. def OAI.SquareRootDegree.SmoothGaussian.mass line 117
  14. def OAI.SquareRootDegree.SmoothGaussian.mean line 119
  15. def OAI.SquareRootDegree.SmoothGaussian.variance line 121
  16. theorem OAI.SquareRootDegree.SmoothGaussian.integral_weight_sub_sq line 124
  17. theorem OAI.SquareRootDegree.SmoothGaussian.mean_mul_mass line 136
  18. theorem OAI.SquareRootDegree.SmoothGaussian.variance_mul_mass line 140
  19. theorem OAI.SquareRootDegree.SmoothGaussian.weighted_interval_bounds line 151
  20. theorem OAI.SquareRootDegree.SmoothGaussian.tent_mass_pos line 205
  21. theorem OAI.SquareRootDegree.SmoothGaussian.tent_moments line 210