ASTIS mathematical exposition

Differentiate the radial cutoff after PiLp transport

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.hasFDerivAt_radialSmoothCutoff_comp_toLp · theorem · Teaching coverage

Statement

Let n∈ℕ, R>0 and x∈P. Write χ_R for the Euclidean radial cutoff and η_R=χ_R∘T on raw coordinates. Then η_R has derivative Dχ_R(Tx)∘T at x, where T is regarded as a continuous linear map.

\[D\eta_R(x)=D\chi_R(Tx)\circ T,\qquad \eta_R(x)=\chi_R(Tx).\]

All objects and hypotheses

n∈ℕ, d=n+1≥1, P=(Fin d→ℝ) with its usual supremum norm, V=EuclideanSpace ℝ (Fin d) with its ℓ² norm. T:P→V is WithLp.toLp 2, a continuous linear equivalence, and e=T⁻¹=WithLp.ofLp.
R∈ℝ with R>0; x∈P; χ_R is Cutoff.radialSmoothCutoff on V.

Mathematical proof

1. Differentiate the linear coordinate conversion

The derivative of T at every point is its own continuous linear map.

\[DT(x)=T.\]

Corresponding Lean step

PiLp.hasFDerivAt_toLp; the derivative is e.symm.toContinuousLinearMap.

2. Differentiate the smooth Euclidean cutoff and compose

Positive radius makes χ_R smooth on V, hence differentiable at Tx. The Fréchet chain rule gives the claimed composite derivative.

\[D(\chi_R\circ T)(x)=D\chi_R(Tx)\circ T.\]

Corresponding Lean step

Cutoff.radialSmoothCutoff_contDiff hR; .differentiable ... .hasFDerivAt; hcutoff.comp x htoLp.

Lean statement · hasFDerivAt_radialSmoothCutoff_comp_toLp

The result is `HasFDerivAt`, so it certifies genuine differentiability, not merely a totalized fderiv expression. The inverse of e is T.

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 hasFDerivAt_radialSmoothCutoff_comp_toLp
    {n : ℕ} {R : ℝ} (hR : 0 < R) (x : Fin (n + 1) → ℝ) :
    HasFDerivAt
      (fun z => Cutoff.radialSmoothCutoff R
        (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
      ((fderiv ℝ
          (Cutoff.radialSmoothCutoff R :
            EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
          (WithLp.toLp 2 x)).comp
        (PiLp.continuousLinearEquiv
          2 ℝ (fun _ : Fin (n + 1) => ℝ)).symm.toContinuousLinearMap)
      x

Exact module and namespace context

Lean proof · hasFDerivAt_radialSmoothCutoff_comp_toLp

The source first the derivative of T at every point is its own continuous linear map. It finishes as follows: Positive radius makes χ_R smooth on V, hence differentiable at Tx. The Fréchet chain rule gives the claimed composite derivative. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem hasFDerivAt_radialSmoothCutoff_comp_toLp
    {n : ℕ} {R : ℝ} (hR : 0 < R) (x : Fin (n + 1) → ℝ) :
    HasFDerivAt
      (fun z => Cutoff.radialSmoothCutoff R
        (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
      ((fderiv ℝ
          (Cutoff.radialSmoothCutoff R :
            EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
          (WithLp.toLp 2 x)).comp
        (PiLp.continuousLinearEquiv
          2 ℝ (fun _ : Fin (n + 1) => ℝ)).symm.toContinuousLinearMap)
      x := by
  let e : EuclideanSpace ℝ (Fin (n + 1)) ≃L[ℝ] (Fin (n + 1) → ℝ) :=
    PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin (n + 1) => ℝ)
  have htoLp : HasFDerivAt
      (fun z : Fin (n + 1) → ℝ =>
        (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
      e.symm.toContinuousLinearMap x := by
    simpa [e] using
      (PiLp.hasFDerivAt_toLp (𝕜 := ℝ)
        (E := fun _ : Fin (n + 1) => ℝ) 2 x)
  have hcutoff : HasFDerivAt
      (Cutoff.radialSmoothCutoff R :
        EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
      (fderiv ℝ
        (Cutoff.radialSmoothCutoff R :
          EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
        (WithLp.toLp 2 x))
      (WithLp.toLp 2 x) :=
    ((Cutoff.radialSmoothCutoff_contDiff hR).differentiable
      (WithTop.coe_ne_zero.mpr WithTop.top_ne_zero)
      (WithLp.toLp 2 x)).hasFDerivAt
  simpa [Function.comp_def, e] using hcutoff.comp x htoLp

/-- For an integrable finite Pi-space vector field, the `L¹` norm of the
radial-cutoff gradient applied to that field vanishes as the cutoff scale tends
to infinity.

The domination retains the operator norm of the inverse `PiLp` equivalence:
the raw Pi norm is not identified with the Euclidean `L²` norm.  This theorem
only controls the cutoff-gradient cross term; it proves no source-field
integrability, main-term convergence, integration by parts, or invariant-law
statement. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Pointwise derivative producer only; no support enclosure in a box or integral estimate.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

PiLp.hasFDerivAt_toLp
HasFDerivAt.comp

Mathematical sources

Current ASTIS source — Exact statement and actual proof/construction authority; raw code intentionally omitted from this packet.
Existing curated module card — Existing declaration-specific attribution entry, read as documentation without a new source-equivalence verdict.
Called library/source declaration: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Called library/source declaration: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_contDiff — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Called library/source declaration: PiLp.hasFDerivAt_toLp — Exact existing Mathlib theorem used by the documented argument.
Existing focused test — Exact named declaration invocation located in an existing example; no test was run.

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