ASTIS mathematical exposition

The cutoff-gradient cross term tends to zero in L¹

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

Statement

Let μ be any measure on raw P and G:P→P be μ-integrable. With η_R=χ_R∘T, the integral of the absolute value of Dη_R(x) applied to G(x) tends to zero as the real radius R tends to positive infinity.

\[\lim_{R\to+\infty}\int_P\bigl|D\eta_R(x)[G(x)]\bigr|\,d\mu(x)=0.\]

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.
μ is an arbitrary measure on P; no finiteness or probability assumption.
G:P→P is Integrable G μ, including a.e. strong measurability and integrability of its supremum norm.
For every real R the integrand is expressed by totalized fderiv. For the eventually positive radii used in the proof, η_R is smooth and fderiv is its genuine derivative.

Mathematical proof

1. Fix a first-derivative constant and an integrable dominator

Choose C>0 from the Euclidean radial derivative bound. Since ‖G‖ is integrable, so is b(x)=C‖T‖op‖G(x)‖.

\[\|D\chi_R(y)\|_{\rm op}\le C/R,\qquad b(x):=C\|T\|_{\rm op}\|G(x)\|\in L^1(\mu).\]

Corresponding Lean step

Cutoff.radialSmoothCutoff_fderiv_bound; hG.norm.const_mul.

2. Establish a.e. strong measurability for positive radii

The composition η_R is smooth for R>0, so its derivative is continuous. Evaluating this continuous linear-map field on the a.e. strongly measurable G, then taking the norm, gives an a.e. strongly measurable integrand.

\[x\mapsto D\eta_R(x)\text{ continuous},\qquad x\mapsto |D\eta_R(x)[G(x)]|\text{ a.e. strongly measurable}.\]

Corresponding Lean step

PiLp.contDiff_toLp; ContDiff.continuous_fderiv; ContinuousLinearMap.flip (ContinuousLinearMap.apply ℝ ℝ); aestronglyMeasurable_comp₂.

3. Keep the norm-conversion constant in the derivative estimate

The transported chain rule and operator norm inequalities give |Dη_R(x)[G(x)]|≤(C/R)‖T‖op‖G(x)‖. For R≥1 this is at most b(x).

\[|D\eta_R(x)[G(x)]|\le\frac{C}{R}\|T\|_{\rm op}\|G(x)\|\le b(x)\quad(R\ge1).\]

Corresponding Lean step

hasFDerivAt_radialSmoothCutoff_comp_toLp ... .fderiv; ContinuousLinearMap.le_opNorm; ContinuousLinearMap.opNorm_comp_le; div_le_self.

4. Prove pointwise decay by squeezing

At each fixed x the right side is a constant times 1/R, hence tends to zero. Nonnegativity squeezes the integrand to zero.

\[0\le |D\eta_R(x)[G(x)]|\le\frac{C\|T\|_{\rm op}\|G(x)\|}{R}\longrightarrow0.\]

Corresponding Lean step

squeeze_zero'; tendsto_const_nhds.div_atTop tendsto_id and .mul_const.

5. Apply dominated convergence along real radii

The real atTop filter has a countable basis. Eventual measurability, eventual domination by b∈L¹, and a.e. pointwise convergence allow the limit through the integral; the integral of zero is zero.

\[\int_P |D\eta_R[G]|\,d\mu\longrightarrow\int_P0\,d\mu=0.\]

Corresponding Lean step

MeasureTheory.tendsto_integral_filter_of_dominated_convergence with bound, hmeas, hdom, hbound_integrable, hpoint.

Lean statement · tendsto_integral_norm_fderiv_radialSmoothCutoff_comp_toLp_apply

`Integrable G μ` is the only analytic input. The output integrates a real norm of a scalar derivative application. All estimates are required only eventually in R, so no assertion about nonpositive-radius smoothness is needed.

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 tendsto_integral_norm_fderiv_radialSmoothCutoff_comp_toLp_apply
    {n : ℕ} {μ : Measure (Fin (n + 1) → ℝ)}
    {G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ}
    (hG : Integrable G μ) :
    Tendsto
      (fun R : ℝ =>
        ∫ x, ‖fderiv ℝ
          (fun z => Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
          x (G x)‖ ∂μ)
      atTop (𝓝 0)

Exact module and namespace context

Lean proof · tendsto_integral_norm_fderiv_radialSmoothCutoff_comp_toLp_apply

The source first choose C>0 from the Euclidean radial derivative bound. Since ‖G‖ is integrable, so is b(x)=C‖T‖op‖G(x)‖. It finishes as follows: The real atTop filter has a countable basis. Eventual measurability, eventual domination by b∈L¹, and a.e. pointwise convergence allow the limit through the integral; the integral of zero is zero. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem tendsto_integral_norm_fderiv_radialSmoothCutoff_comp_toLp_apply
    {n : ℕ} {μ : Measure (Fin (n + 1) → ℝ)}
    {G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ}
    (hG : Integrable G μ) :
    Tendsto
      (fun R : ℝ =>
        ∫ x, ‖fderiv ℝ
          (fun z => Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
          x (G x)‖ ∂μ)
      atTop (𝓝 0) := by
  let e : EuclideanSpace ℝ (Fin (n + 1)) ≃L[ℝ] (Fin (n + 1) → ℝ) :=
    PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin (n + 1) => ℝ)
  obtain ⟨C, hC_pos, hC⟩ :=
    Cutoff.radialSmoothCutoff_fderiv_bound
      (E := EuclideanSpace ℝ (Fin (n + 1)))
  let bound : (Fin (n + 1) → ℝ) → ℝ :=
    fun x => (C * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖
  have hbound_integrable : Integrable bound μ := by
    exact (hG.norm.const_mul (C * ‖e.symm.toContinuousLinearMap‖))
  have hmeas :
      ∀ᶠ R : ℝ in atTop,
        AEStronglyMeasurable
          (fun x => ‖fderiv ℝ
            (fun z => Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
            x (G x)‖) μ := by
    filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
    have hsmooth :
        ContDiff ℝ (⊤ : ℕ∞)
          (fun z : Fin (n + 1) → ℝ =>
            Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1)))) :=
      (Cutoff.radialSmoothCutoff_contDiff hR).comp
        (PiLp.contDiff_toLp (𝕜 := ℝ) (E := fun _ : Fin (n + 1) => ℝ))
    have hderiv :
        AEStronglyMeasurable
          (fun x => fderiv ℝ
            (fun z : Fin (n + 1) → ℝ =>
              Cutoff.radialSmoothCutoff R
                (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
            x) μ :=
      (hsmooth.continuous_fderiv
        (WithTop.coe_ne_zero.mpr WithTop.top_ne_zero)).aestronglyMeasurable
    let eval :
        ((Fin (n + 1) → ℝ) →L[ℝ] ℝ) →L[ℝ]
          (Fin (n + 1) → ℝ) →L[ℝ] ℝ :=
      ContinuousLinearMap.flip (ContinuousLinearMap.apply ℝ ℝ)
    exact
      (eval.aestronglyMeasurable_comp₂
        hderiv hG.aestronglyMeasurable).norm
  have hdom :
      ∀ᶠ R : ℝ in atTop, ∀ᵐ x ∂μ,
        ‖(fun x => ‖fderiv ℝ
          (fun z => Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
          x (G x)‖) x‖ ≤ bound x := by
    filter_upwards [eventually_ge_atTop (1 : ℝ)] with R hR
    filter_upwards with x
    have hR_pos : 0 < R := lt_of_lt_of_le zero_lt_one hR
    have hfderiv :
        fderiv ℝ
          (fun z => Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
          x =
        (fderiv ℝ
          (Cutoff.radialSmoothCutoff R :
            EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
          (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap :=
      (hasFDerivAt_radialSmoothCutoff_comp_toLp hR_pos x).fderiv
    rw [norm_norm, hfderiv]
    calc
      ‖((fderiv ℝ
          (Cutoff.radialSmoothCutoff R :
            EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
          (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap) (G x)‖
          ≤ ‖(fderiv ℝ
              (Cutoff.radialSmoothCutoff R :
                EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
              (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap‖ * ‖G x‖ :=
        ContinuousLinearMap.le_opNorm _ _
      _ ≤ ((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖ := by
        gcongr
        exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
          (mul_le_mul_of_nonneg_right
            (hC R hR_pos (WithLp.toLp 2 x)) (norm_nonneg _))
      _ ≤ bound x := by
        dsimp [bound]
        gcongr
        exact div_le_self hC_pos.le hR
  have hpoint :
      ∀ᵐ x ∂μ,
        Tendsto
          (fun R : ℝ => ‖fderiv ℝ
            (fun z => Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
            x (G x)‖)
          atTop (𝓝 0) := by
    filter_upwards with x
    refine squeeze_zero'
      (g := fun R =>
        ((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖) ?_ ?_ ?_
    · exact Filter.Eventually.of_forall fun R => norm_nonneg _
    · filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
      have hfderiv :
          fderiv ℝ
            (fun z => Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
            x =
          (fderiv ℝ
            (Cutoff.radialSmoothCutoff R :
              EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
            (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap :=
        (hasFDerivAt_radialSmoothCutoff_comp_toLp hR x).fderiv
      rw [hfderiv]
      calc
        ‖((fderiv ℝ
            (Cutoff.radialSmoothCutoff R :
              EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
            (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap) (G x)‖
            ≤ ‖(fderiv ℝ
                  (Cutoff.radialSmoothCutoff R :
                    EuclideanSpace ℝ (Fin (n + 1)) → ℝ)
                  (WithLp.toLp 2 x)).comp e.symm.toContinuousLinearMap‖ *
                  ‖G x‖ := ContinuousLinearMap.le_opNorm _ _
        _ ≤ ((C / R) * ‖e.symm.toContinuousLinearMap‖) * ‖G x‖ := by
          gcongr
          exact (ContinuousLinearMap.opNorm_comp_le _ _).trans
            (mul_le_mul_of_nonneg_right
              (hC R hR (WithLp.toLp 2 x)) (norm_nonneg _))
    · simpa [mul_assoc] using
        (tendsto_const_nhds.div_atTop tendsto_id).mul_const
          (‖e.symm.toContinuousLinearMap‖ * ‖G x‖)
  have hDCT :=
    MeasureTheory.tendsto_integral_filter_of_dominated_convergence
      (μ := μ) (l := atTop)
      (F := fun R x => ‖fderiv ℝ
        (fun z => Cutoff.radialSmoothCutoff R
          (WithLp.toLp 2 z : EuclideanSpace ℝ (Fin (n + 1))))
        x (G x)‖)
      (f := fun _ => (0 : ℝ)) bound hmeas hdom hbound_integrable hpoint
  simpa using hDCT

/-- Multiplication by the PiLp-wrapped radial cutoff converges to the identity
under integration for every integrable real normed-space-valued source field.

The statement is measure-generic and uses only integrability of the source.
It proves the cutoff main-term limit, but no Gibbs-specific integrability,
cutoff-gradient estimate, integration by parts, generator-domain result, or
invariant-law statement. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The raw supremum norm is not identified with the Euclidean norm: the factor ‖T‖op is retained.
This proves a generic cross-term limit, not integrability of any particular physical field or invariance.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

PiLp.contDiff_toLp
ContDiff.continuous_fderiv
ContinuousLinearMap.aestronglyMeasurable_comp₂
ContinuousLinearMap.le_opNorm
ContinuousLinearMap.opNorm_comp_le
MeasureTheory.tendsto_integral_filter_of_dominated_convergence
squeeze_zero'

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_fderiv_bound — 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: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.hasFDerivAt_radialSmoothCutoff_comp_toLp — 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 — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Called library/source declaration: PiLp.contDiff_toLp — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: ContDiff.continuous_fderiv — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: ContinuousLinearMap.aestronglyMeasurable_comp₂ — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: ContinuousLinearMap.opNorm_comp_le — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: MeasureTheory.tendsto_integral_filter_of_dominated_convergence — 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.