ASTIS mathematical exposition

Integrable norm tails outside expanding Euclidean balls vanish

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

Statement

For any measure μ on P, real normed vector space W, and μ-integrable H:P→W, the integral of ‖H(x)‖ over the closed exterior set {x:R≤‖Tx‖₂} tends to zero as R→+∞.

\[\lim_{R\to+\infty}\int_{\{x:R\le\|Tx\|_2\}}\|H(x)\|\,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.
W is a real normed vector space; no completeness assumption.
μ is any measure on P; H:P→W is μ-integrable. The integral itself is real-valued.

Mathematical proof

1. Construct a decreasing measurable family

The norm of Tx is continuous, so E_R={x:R≤‖Tx‖₂} is measurable. If R≤S, then E_S⊆E_R.

\[E_R=\{x:R\le\|Tx\|_2\},\qquad R\le S\Longrightarrow E_S\subseteq E_R.\]

Corresponding Lean step

measurableSet_le; continuous_norm.comp (PiLp.continuous_toLp 2 _); hs_antitone.

2. Show that no point survives all tail sets

For fixed x, choosing R=‖Tx‖₂+1 excludes x. Hence the intersection over all real R is empty.

\[\bigcap_{R\in\mathbb R}E_R=\varnothing.\]

Corresponding Lean step

Set.mem_iInter.mp hx (‖WithLp.toLp 2 x‖ + 1) and the resulting impossible inequality.

3. Use decreasing-set integral convergence

The integrable function ‖H‖ is integrable on E_0. The antitone set-integral theorem gives convergence to its integral over the empty intersection, which is zero.

\[\int_{E_R}\|H\|\,d\mu\longrightarrow\int_{\cap_RE_R}\|H\|\,d\mu=0.\]

Corresponding Lean step

tendsto_setIntegral_of_antitone hs_measurable hs_antitone ⟨0, hH.norm.integrableOn⟩.

Lean statement · tendsto_setIntegral_norm_norm_ge_comp_toLp

The tail boundary is included by the non-strict inequality. This generic measure-theoretic theorem does not assume that μ is finite, has a density, or is a Gibbs measure.

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

Exact module and namespace context

Lean proof · tendsto_setIntegral_norm_norm_ge_comp_toLp

The source first the norm of Tx is continuous, so E_R={x:R≤‖Tx‖₂} is measurable. If R≤S, then E_S⊆E_R. It finishes as follows: The integrable function ‖H‖ is integrable on E_0. The antitone set-integral theorem gives convergence to its integral over the empty intersection, which is zero. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem tendsto_setIntegral_norm_norm_ge_comp_toLp
    {n : ℕ} {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    {μ : Measure (Fin (n + 1) → ℝ)}
    {H : (Fin (n + 1) → ℝ) → F}
    (hH : Integrable H μ) :
    Tendsto
      (fun R : ℝ => ∫ x in
        {x : Fin (n + 1) → ℝ |
          R ≤ ‖(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))‖},
        ‖H x‖ ∂μ)
      atTop (𝓝 0) := by
  let s : ℝ → Set (Fin (n + 1) → ℝ) :=
    fun R => {x | R ≤ ‖(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))‖}
  have hs_measurable : ∀ R, MeasurableSet (s R) := by
    intro R
    exact measurableSet_le measurable_const
      ((continuous_norm.comp (PiLp.continuous_toLp 2 _)).measurable)
  have hs_antitone : Antitone s := by
    intro R S hRS x hx
    exact hRS.trans hx
  have hs_iInter : ⋂ R : ℝ, s R = ∅ := by
    apply Set.Subset.antisymm
    · intro x hx
      have hx' := Set.mem_iInter.mp hx
        (‖(WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))‖ + 1)
      simp only [s, Set.mem_ofPred_eq] at hx'
      linarith
    · exact Set.empty_subset _
  have htail := tendsto_setIntegral_of_antitone
    hs_measurable hs_antitone ⟨0, hH.norm.integrableOn⟩
  simpa [s, hs_iInter] using htail

/-- The trace contribution of `χ'.smulRight G` over the standard finite Pi
basis is exactly the scalar derivative `χ'` applied to `G`.

This is pure finite-dimensional linear algebra.  It identifies the cutoff
cross term used by the divergence product rule but proves no measurability,
integrability, convergence, or boundary result. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No rate of tail decay is given.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

measurableSet_le
PiLp.continuous_toLp
MeasureTheory.tendsto_setIntegral_of_antitone

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: PiLp.continuous_toLp — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: MeasureTheory.tendsto_setIntegral_of_antitone — 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.