ASTIS mathematical exposition

The unit cutoff is infinitely differentiable

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

Statement

The fixed function q:ℝ→ℝ is C∞ on the whole real line, including t=0.

\[q\in C^\infty(\mathbb R;\mathbb R).\]

All objects and hypotheses

No parameters or additional hypotheses.

Mathematical proof

1. Use joint smoothness in the valid bump-parameter region

The bump base is jointly smooth on (1,∞)×ℝ. For any t, the point (2,t) belongs to this open set, so it has a neighborhood on which the joint function is smooth.

\[(2,t)\in(1,\infty)\times\mathbb R,\qquad B_{\mathbb R}\text{ is }C^\infty\text{ near }(2,t).\]

Corresponding Lean step

have hmem := ⟨by norm_num, Set.mem_univ x⟩
have hnhds := (isOpen_Ioi.prod isOpen_univ).mem_nhds hmem
have hbase := (ContDiffBumpBase.ofInnerProductSpace ℝ).smooth.contDiffAt hnhds

2. Insert the fixed parameter smoothly

The map t↦(2,t) is smooth because its coordinates are a constant and the identity.

\[J(t)=(2,t),\qquad J\in C^\infty.\]

Corresponding Lean step

have hpair := (contDiffAt_const (c := (2 : ℝ))).prodMk contDiffAt_id

3. Compose and conclude at every point

The cutoff is Bℝ∘J. Compose the two smooth maps at each t, then use the pointwise characterization of global C∞ regularity.

\[q=B_{\mathbb R}\circ J\in C^\infty.\]

Corresponding Lean step

rw [contDiff_iff_contDiffAt]
intro x
-- after hbase and hpair:
exact hbase.comp x hpair

Lean statement · smoothUnitCutoff_contDiff

ContDiff ℝ (⊤ : ℕ∞) is the C∞ assertion. Smoothness comes from the bump family, whose plateau resolves the apparent absolute-value singularity.

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 smoothUnitCutoff_contDiff : ContDiff ℝ (⊤ : ℕ∞) smoothUnitCutoff

Exact module and namespace context

Lean proof · smoothUnitCutoff_contDiff

Actual proof outline: Use joint smoothness in the valid bump-parameter region: hnhds turns the open-domain membership into the neighborhood condition needed to pass from ContDiffOn to ContDiffAt. Insert the fixed parameter smoothly: prodMk pairs two smooth component functions. Compose and conclude at every point: The pointwise proof is repeated for arbitrary x. It does not assume that the norm itself is smooth at the origin.

theorem smoothUnitCutoff_contDiff : ContDiff ℝ (⊤ : ℕ∞) smoothUnitCutoff := by
  rw [contDiff_iff_contDiffAt]
  intro x
  have hmem :
      ((2 : ℝ), x) ∈ (Set.Ioi (1 : ℝ) ×ˢ (Set.univ : Set ℝ)) := by
    exact ⟨by norm_num, Set.mem_univ x⟩
  have hnhds :
      (Set.Ioi (1 : ℝ) ×ˢ (Set.univ : Set ℝ)) ∈ 𝓝 ((2 : ℝ), x) := by
    exact (isOpen_Ioi.prod isOpen_univ).mem_nhds hmem
  have hbase :
      ContDiffAt ℝ (⊤ : ℕ∞)
        (Function.uncurry (ContDiffBumpBase.ofInnerProductSpace ℝ).toFun)
        ((2 : ℝ), x) :=
    (ContDiffBumpBase.ofInnerProductSpace ℝ).smooth.contDiffAt hnhds
  have hpair : ContDiffAt ℝ (⊤ : ℕ∞) (fun y : ℝ => ((2 : ℝ), y)) x :=
    (contDiffAt_const (c := (2 : ℝ))).prodMk contDiffAt_id
  change ContDiffAt ℝ (⊤ : ℕ∞)
    (fun y : ℝ =>
      Function.uncurry (ContDiffBumpBase.ofInnerProductSpace ℝ).toFun ((2 : ℝ), y)) x
  exact hbase.comp x hpair

/-- The unit cutoff is one when `|x| <= 1`. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Global one-dimensional smoothness; no radial-space or radius assumptions occur yet.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff

Mathlib API called (external library)

contDiff_iff_contDiffAt
ContDiffBumpBase.ofInnerProductSpace
ContDiffOn.contDiffAt
ContDiffAt.prodMk
ContDiffAt.comp
contDiffAt_const
contDiffAt_id

Mathematical sources

Current ASTIS declaration and complete body — Authority for the statement, local assumptions, and actual proof/construction documented here.
Existing module card — Existing curated entry for this declaration. Attribution is preserved as local card evidence only, without a new external-source audit or source-equivalence verdict.
ContDiffBumpBase.ofInnerProductSpace — Exact checked local Mathlib dependency definition or theorem.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
Existing test source — Existing direct example invocation inspected; no build or test run was performed.

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