Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Differentiate the radial cutoff after PiLp transport

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

Read this first

Mathematical 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).\]
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.

Download module (.lean)
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

Proof roadmap

  1. 1Differentiate the linear coordinate conversion

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

  2. 2Differentiate 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.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

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.

Download module (.lean)
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

Exact module and namespace context

Scope and omitted-condition boundaries
  • Pointwise derivative producer only; no support enclosure in a box or integral estimate.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

  • PiLp.hasFDerivAt_toLp
  • HasFDerivAt.comp

Mathematical sources

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