Samplinglib mathematical lesson

Integrable norm tails outside expanding Euclidean balls vanish

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

Read this first

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

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.

Download module (.lean)

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

Proof roadmap

1Construct 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.
2Show 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.
3Use 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.

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

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

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.

Download module (.lean)

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

Exact module and namespace context

Scope and omitted-condition boundaries

No rate of tail decay is given.

Sources, dependencies, and reuse

Source and reuse

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

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