OAI/Combinatorics/BooleanFunctions/SmoothSelector.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareRootDegree.SmoothSelector.clip line 13
  2. theorem OAI.SquareRootDegree.SmoothSelector.clip_continuous line 15
  3. theorem OAI.SquareRootDegree.SmoothSelector.clip_nonneg line 17
  4. theorem OAI.SquareRootDegree.SmoothSelector.clip_le_one line 18
  5. theorem OAI.SquareRootDegree.SmoothSelector.clip_mono line 19
  6. theorem OAI.SquareRootDegree.SmoothSelector.clip_of_nonpos line 20
  7. theorem OAI.SquareRootDegree.SmoothSelector.clip_of_one_le line 22
  8. def OAI.SquareRootDegree.SmoothSelector.hat line 26

    Source documentation

    The consecutive ramp differences form an exact finite partition on a grid.

    def hat (N : ℕ) (δ : ℝ) (i : Fin (2*N+1)) (t : ℝ) : ℝ :=
…
  9. theorem OAI.SquareRootDegree.SmoothSelector.hat_continuous line 29
  10. theorem OAI.SquareRootDegree.SmoothSelector.hat_nonneg line 32
  11. theorem OAI.SquareRootDegree.SmoothSelector.hats_sum line 37
  12. theorem OAI.SquareRootDegree.SmoothSelector.hats_sum_le_one line 49
  13. theorem OAI.SquareRootDegree.SmoothSelector.hats_sum_eq_one line 54
  14. def OAI.SquareRootDegree.SmoothSelector.middle line 66
  15. def OAI.SquareRootDegree.SmoothSelector.weight line 68
  16. theorem OAI.SquareRootDegree.SmoothSelector.weight_continuous line 71
  17. theorem OAI.SquareRootDegree.SmoothSelector.weight_nonneg line 76
  18. theorem OAI.SquareRootDegree.SmoothSelector.weight_sum line 81
  19. def OAI.SquareRootDegree.SmoothSelector.center line 84
  20. theorem OAI.SquareRootDegree.SmoothSelector.center_middle line 86
  21. theorem OAI.SquareRootDegree.SmoothSelector.hat_local line 89
  22. theorem OAI.SquareRootDegree.SmoothSelector.hat_support line 106
  23. theorem OAI.SquareRootDegree.SmoothSelector.hat_compactSupport line 117