OAI/Geometry/SurfaceImmersion/Correction/SmoothingKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Smooth compactly supported smoothing kernels with arbitrarily many vanishing moments, constructed from finitely many positive dilations.

  1. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.continuous_monomial line 16
  2. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_dilate line 20
  3. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_dilate line 24
  4. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.integrable_moment_dilate line 30
  5. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.moment_sum_dilates line 38
  6. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.basicBump line 56
  7. def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.basicKernel line 58
  8. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.smooth_basicKernel line 60
  9. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.compact_basicKernel line 62
  10. lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.integral_basicKernel line 64
  11. theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_smoothing_kernel line 68

    Source documentation

    A concrete kernel used for finite-order smoothing. Its mass is one and all nonconstant coordinate moments through degree r vanish.

    theorem exists_smoothing_kernel (r : ℕ) :
    ∃ K : Base → ℝ, ContDiff ℝ ∞ K ∧ HasCompactSupport K ∧
      (∫ x, K x) = 1 ∧ ∀ α : Fin 2 → ℕ, 1 ≤ degree α → degree α ≤ r →
        (∫ x, monomial α x * K x) = 0 := by
…

    Mentions: OAI.ClosedSurfaceR4.FiniteOrderSmoothing.degree, OAI.ClosedSurfaceR4.FiniteOrderSmoothing.monomial