SmoothingMoments.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Finite moment cancellation for smoothing kernels on the coordinate plane. Distinct positive dilations give a kernel of mass one whose required low moments vanish. This is the algebraic step in finite-order smoothing.

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_dilation_weights line 19

Source documentation

The transpose Vandermonde system prescribes all moments through order r.

theorem exists_dilation_weights (r : ℕ) (b : Fin (r + 1) → ℝ)
    (hb : Function.Injective b) :
    ∃ c : Fin (r + 1) → ℝ, ∀ j : Fin (r + 1),
      ∑ i, c i * b i ^ j.val = if j = 0 then 1 else 0 := by
…

theorem OAI.ClosedSurfaceR4.FiniteOrderSmoothing.exists_positive_dilation_weights line 36
Source documentation
Positive integral dilation factors suffice, so each dilation preserves compact support and smoothness.
```
theorem exists_positive_dilation_weights (r : ℕ) :
    ∃ c : Fin (r + 1) → ℝ, ∀ j : Fin (r + 1),
      ∑ i, c i * ((i.val + 1 : ℕ) : ℝ) ^ j.val = if j = 0 then 1 else 0 := by
…
```
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.monomial line 44
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.degree line 46
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.monomial_smul line 48
def OAI.ClosedSurfaceR4.FiniteOrderSmoothing.dilate line 54
Source documentation
The normalized dilation is appropriate to the two-dimensional chart.
```
def dilate (K : Base → ℝ) (a : ℝ) (x : Base) : ℝ := (a ^ 2)⁻¹ * K (a⁻¹ • x)
```
lemma OAI.ClosedSurfaceR4.FiniteOrderSmoothing.moment_dilate line 56