Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Positive-radius radial cutoffs are smooth

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_contDiff · theorem · Teaching coverage

Statement

Let E be a real inner-product space, not necessarily finite-dimensional or complete, and let R>0. The function χ_R:E→ℝ is infinitely continuously differentiable on all of E, including the origin.

\[R>0\quad\Longrightarrow\quad\chi_R\in C^\infty(E,\mathbb R).\]

All objects and hypotheses

  • E is a normed additive commutative group with a real inner-product-space structure.
  • R∈ℝ and R>0. There is no finite-dimensionality, completeness, or nontriviality hypothesis.

Mathematical proof

1. Separate the inner plateau from the nonzero region

Smoothness is checked at an arbitrary point x. Split according to whether ‖x‖<R. These two cases include the inner sphere in the second branch.

\[E=\{x:\|x\|<R\}\cup\{x:R\le\|x\|\}.\]
Corresponding Lean step

rw [contDiff_iff_contDiffAt]; intro x; by_cases hx : ‖x‖ < R

2. Use a constant neighborhood inside the plateau

If ‖x‖<R, the ball around x of radius R−‖x‖ is a neighborhood. Every y in it satisfies ‖y‖≤‖x‖+‖y−x‖<R, so χ_R(y)=1. A function agreeing with a constant near x is smooth at x.

\[d(y,x)<R-\|x\|\ \Longrightarrow\ \|y\|<R\ \Longrightarrow\ \chi_R(y)=1.\]
Corresponding Lean step

Metric.ball_mem_nhds x (sub_pos.mpr hx); radialSmoothCutoff_eq_one_of_norm_le hR; norm_add_le x (y - x); hconst.congr_of_eventuallyEq

3. Compose smooth functions away from the origin

In the remaining case R≤‖x‖, positivity implies x≠0. The norm on a real inner-product space is smooth at nonzero points. Compose it with division by the fixed R, then with the scalar smooth cutoff q.

\[x\ne0,\qquad \chi_R=q\circ(t\mapsto t/R)\circ\|\cdot\|,\qquad \chi_R\text{ is }C^\infty\text{ at }x.\]
Corresponding Lean step

contDiffAt_norm ℝ hx_ne; contDiff_id.div_const R; hdiv.contDiffAt.comp x hnorm; smoothUnitCutoff_contDiff.contDiffAt.comp x hscaled

Lean statement · radialSmoothCutoff_contDiff

`ContDiff ℝ (⊤ : ℕ∞)` means derivatives of every finite order exist and are continuous. The inner-product assumption is used for smoothness of the norm away from zero; the plateau handles the origin. The source's surrounding Radial section contributes the implicit type E and its NormedAddCommGroup instance; further structures appear explicitly in the declaration.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem radialSmoothCutoff_contDiff [InnerProductSpace ℝ E] {R : ℝ} (hR : 0 < R) :
    ContDiff ℝ (⊤ : ℕ∞) (radialSmoothCutoff R : E → ℝ)

Exact module and namespace context

Lean proof · radialSmoothCutoff_contDiff

Actual proof outline: Separate the inner plateau from the nonzero region: `ContDiff` is global smoothness; `contDiff_iff_contDiffAt` allows a point-by-point argument. Use a constant neighborhood inside the plateau: `heq` records equality on a neighborhood, which is stronger than equality only at x. The library transfers smoothness of the constant function along this local equality. Compose smooth functions away from the origin: The norm-smoothness theorem is invoked only after proving x≠0. This avoids making a false smoothness assertion about the norm itself at zero.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem radialSmoothCutoff_contDiff [InnerProductSpace ℝ E] {R : ℝ} (hR : 0 < R) :
    ContDiff ℝ (⊤ : ℕ∞) (radialSmoothCutoff R : E → ℝ) := by
  rw [contDiff_iff_contDiffAt]
  intro x
  by_cases hx : ‖x‖ < R
  · have heq : ∀ᶠ y in 𝓝 x, radialSmoothCutoff R y = 1 := by
      have hball : Metric.ball x (R - ‖x‖) ∈ 𝓝 x :=
        Metric.ball_mem_nhds x (sub_pos.mpr hx)
      filter_upwards [hball] with y hy
      apply radialSmoothCutoff_eq_one_of_norm_le hR
      rw [Metric.mem_ball, dist_eq_norm] at hy
      have hynorm : ‖y‖ ≤ ‖x‖ + ‖y - x‖ := by
        calc
          ‖y‖ = ‖x + (y - x)‖ := by congr 1; abel
          _ ≤ ‖x‖ + ‖y - x‖ := norm_add_le x (y - x)
      linarith
    have hconst : ContDiffAt ℝ (⊤ : ℕ∞) (fun _ : E => (1 : ℝ)) x :=
      contDiffAt_const
    apply hconst.congr_of_eventuallyEq
    filter_upwards [heq] with y hy
    simp [hy]
  · push Not at hx
    have hx_ne : x ≠ 0 := by
      intro hzero
      rw [hzero, norm_zero] at hx
      linarith
    have hnorm : ContDiffAt ℝ (⊤ : ℕ∞) (fun y : E => ‖y‖) x :=
      contDiffAt_norm ℝ hx_ne
    have hdiv : ContDiff ℝ (⊤ : ℕ∞) (fun t : ℝ => t / R) :=
      contDiff_id.div_const R
    have hscaled : ContDiffAt ℝ (⊤ : ℕ∞) (fun y : E => ‖y‖ / R) x :=
      hdiv.contDiffAt.comp x hnorm
    exact smoothUnitCutoff_contDiff.contDiffAt.comp x hscaled

/-- A single positive constant controls the first derivative of every
positive-scale radial cutoff by `C / R`.  The quantifier order records the
scale-uniformity needed by cutoff exhaustion arguments. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • This proves genuine smoothness of χ_R, unlike the preceding totalized derivative bound for the scaled norm.
  • The source does not weaken the ambient assumption here to an arbitrary normed space.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • contDiff_iff_contDiffAt
  • Metric.ball_mem_nhds
  • norm_add_le
  • ContDiffAt.congr_of_eventuallyEq
  • contDiffAt_norm
  • ContDiff.div_const
  • ContDiffAt.comp

Mathematical sources

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.