Samplinglib mathematical lesson

The cutoff main term converges under integration

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

Read this first

Mathematical statement

Let μ be any measure on P, let W be a real normed vector space, and let H:P→W be μ-integrable. Multiplication by η_R(x)=χ_R(Tx) converges to the identity under the Mathlib Bochner integral as R→+∞.

\[\lim_{R\to+\infty}\int_P\eta_R(x)H(x)\,d\mu(x)=\int_PH(x)\,d\mu(x).\]

Lean statement · tendsto_integral_radialSmoothCutoff_comp_toLp_smul

The codomain type named F in Lean is called W here to distinguish it from a vector field. No completeness assumption is added; the statement uses Mathlib's totalized Bochner integral conventions.

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 tendsto_integral_radialSmoothCutoff_comp_toLp_smul
    {n : ℕ} {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    {μ : Measure (Fin (n + 1) → ℝ)}
    {H : (Fin (n + 1) → ℝ) → F}
    (hH : Integrable H μ) :
    Tendsto
      (fun R : ℝ => ∫ x,
        Cutoff.radialSmoothCutoff R
          (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x ∂μ)
      atTop (𝓝 (∫ x, H x ∂μ))

Exact module and namespace context

Proof roadmap

1Check eventual measurability
For R>0, η_R is continuous by smoothness of χ_R and continuity of T. Its product with the a.e. strongly measurable H is a.e. strongly measurable.
2Dominate by the source norm
Every cutoff value lies in [0,1], for all real R. Thus ‖η_R(x)H(x)‖≤‖H(x)‖, with integrable right side.
3Use pointwise plateau exhaustion
For every fixed x, χ_R(Tx)→1. Continuity of scalar multiplication gives η_R(x)H(x)→H(x).
4Pass to the integral
Apply the filter version of dominated convergence with bound ‖H‖ and limit H.

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.
W is a normed additive commutative group with NormedSpace ℝ W; no CompleteSpace hypothesis is retained.
μ is any measure on P; H:P→W satisfies Integrable H μ.

Mathematical proof

1. Check eventual measurability

For R>0, η_R is continuous by smoothness of χ_R and continuity of T. Its product with the a.e. strongly measurable H is a.e. strongly measurable.

\[\eta_R\text{ continuous},\quad \eta_R H\text{ a.e. strongly measurable}\quad(R>0).\]

Corresponding Lean step

Cutoff.radialSmoothCutoff_contDiff; PiLp.continuous_toLp; AEStronglyMeasurable.smul.

2. Dominate by the source norm

Every cutoff value lies in [0,1], for all real R. Thus ‖η_R(x)H(x)‖≤‖H(x)‖, with integrable right side.

\[0\le\eta_R\le1,\qquad \|\eta_R(x)H(x)\|\le\|H(x)\|,\qquad \|H\|\in L^1(\mu).\]

Corresponding Lean step

Cutoff.radialSmoothCutoff_mem_Icc; norm_smul; abs_of_nonneg; hH.norm.

3. Use pointwise plateau exhaustion

For every fixed x, χ_R(Tx)→1. Continuity of scalar multiplication gives η_R(x)H(x)→H(x).

\[\eta_R(x)\to1\quad\Longrightarrow\quad\eta_R(x)H(x)\to H(x).\]

Corresponding Lean step

Cutoff.radialSmoothCutoff_tendsto_one (WithLp.toLp 2 x); .smul_const (H x).

4. Pass to the integral

Apply the filter version of dominated convergence with bound ‖H‖ and limit H.

\[\int \eta_RH\,d\mu\longrightarrow\int H\,d\mu.\]

Corresponding Lean step

MeasureTheory.tendsto_integral_filter_of_dominated_convergence.

Lean verification

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

Lean proof · tendsto_integral_radialSmoothCutoff_comp_toLp_smul

The source first for R>0, η_R is continuous by smoothness of χ_R and continuity of T. Its product with the a.e. strongly measurable H is a.e. strongly measurable. It finishes as follows: Apply the filter version of dominated convergence with bound ‖H‖ and limit H. Intermediate steps below identify the actual helper calls and the conditions each one needs.

Download module (.lean)

theorem tendsto_integral_radialSmoothCutoff_comp_toLp_smul
    {n : ℕ} {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    {μ : Measure (Fin (n + 1) → ℝ)}
    {H : (Fin (n + 1) → ℝ) → F}
    (hH : Integrable H μ) :
    Tendsto
      (fun R : ℝ => ∫ x,
        Cutoff.radialSmoothCutoff R
          (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x ∂μ)
      atTop (𝓝 (∫ x, H x ∂μ)) := by
  have hmeas :
      ∀ᶠ R : ℝ in atTop,
        AEStronglyMeasurable
          (fun x : Fin (n + 1) → ℝ =>
            Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x) μ := by
    filter_upwards [eventually_gt_atTop (0 : ℝ)] with R hR
    exact
      (((Cutoff.radialSmoothCutoff_contDiff hR).continuous.comp
        (PiLp.continuous_toLp 2 _)).aestronglyMeasurable).smul
        hH.aestronglyMeasurable
  have hdom :
      ∀ᶠ R : ℝ in atTop, ∀ᵐ x ∂μ,
        ‖Cutoff.radialSmoothCutoff R
            (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x‖ ≤
          ‖H x‖ := by
    filter_upwards with R
    filter_upwards with x
    have hcutoff :=
      Cutoff.radialSmoothCutoff_mem_Icc R
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))
    rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg hcutoff.1]
    exact mul_le_of_le_one_left (norm_nonneg _) hcutoff.2
  have hpoint :
      ∀ᵐ x ∂μ,
        Tendsto
          (fun R : ℝ =>
            Cutoff.radialSmoothCutoff R
              (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x)
          atTop (𝓝 (H x)) := by
    filter_upwards with x
    simpa using
      (Cutoff.radialSmoothCutoff_tendsto_one
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))).smul_const (H x)
  exact MeasureTheory.tendsto_integral_filter_of_dominated_convergence
    (μ := μ) (l := atTop)
    (F := fun R x =>
      Cutoff.radialSmoothCutoff R
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) • H x)
    (f := H) (fun x => ‖H x‖) hmeas hdom hH.norm hpoint

Exact module and namespace context

Scope and omitted-condition boundaries

No Gibbs-specific integrability, derivative cross-term estimate, or integration-by-parts identity is inferred.
The usual Banach-space integral reading applies when W is complete; the exact Lean theorem does not require that extra hypothesis.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

PiLp.continuous_toLp
MeasureTheory.AEStronglyMeasurable.smul
norm_smul
MeasureTheory.tendsto_integral_filter_of_dominated_convergence

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_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.Cutoff.radialSmoothCutoff_mem_Icc — 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_tendsto_one — 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.continuous_toLp — 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.

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