Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

The cutoff main term converges under integration

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

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

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

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

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.

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_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

/-- The `L¹` norm of an integrable field on the complement of an expanding
Euclidean ball tends to zero, expressed in raw finite-Pi coordinates.

The tail sets are `R ≤ ‖WithLp.toLp 2 x‖`.  They form an antitone family with
empty intersection, so Mathlib's antitone set-integral convergence theorem
applies to `‖H‖`.  This is measure-generic and contains no Gibbs, generator,
integration-by-parts, or invariance semantics. -/

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

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

Mathematical sources

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