ASTIS mathematical exposition

A Gibbs L2 representative is locally Lebesgue L2

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2.lp_locallyMemLp_volume · theorem · Teaching coverage

Statement

The squared norm of the selected representative a is locally integrable with respect to volume. For every compact K⊆E, that same representative belongs to L²(dx restricted to K), including its required almost-everywhere strong measurability.

\[a\in L^2(\mu;F)\quad\Longrightarrow\quad \|a\|^2\in L^1_{\mathrm{loc}}(dx),\qquad \forall K\Subset E,\ a\in L^2(K,dx;F).\]

All objects and hypotheses

E is a finite-dimensional real inner-product space, including dimension zero, with its Borel measurable structure and canonical volume dx. F is any normed additive commutative group; no scalar structure or completeness of F is assumed.
W:E→R is continuous and exp(-W) is volume-integrable. Let Z=∫exp(-W)dx and μ=Z⁻¹exp(-W)dx. The positive finite normalization is justified, not an unspecified density constant.
a is an arbitrary element of L²(μ;F). Its function coercion denotes the selected almost-everywhere representative. There is no continuity, differentiability or initially assumed volume measurability of a.

Mathematical proof

1. Use the squared-norm characterization of L2

Membership in Gibbs L2 supplies almost-everywhere strong measurability and integrability of the real-valued squared norm. Even if F has no real scalar action, this norm-squared function is a real function, so change of density can be applied to it.

\[\int \|a(x)\|^2\,d\mu(x)<\infty.\]

Corresponding Lean step

hs via memLp_two_iff_integrable_sq_norm and Lp.memLp

2. Remove only the Gibbs normalization

The tilted-measure integrability equivalence gives integrability of exp(-W) times the squared norm for volume. The assumption on exp(-W) makes the normalization finite; positivity prevents a degenerate normalized measure. No uniform bound on W is needed.

\[e^{-W}\|a\|^2\in L^1(dx).\]

Corresponding Lean step

hw via integrable_tilted_iff hI; smul_eq_mul

3. Invert the weight locally

The inverse weight exp(W) is continuous. A continuous multiplier preserves local integrability. Multiplying the preceding integrable function locally and cancelling the two exponentials proves the local squared-norm assertion. This step is local: the inverse weight may be unbounded on the whole space.

\[e^W(e^{-W}\|a\|^2)=\|a\|^2\in L^1_{\mathrm{loc}}(dx).\]

Corresponding Lean step

hw.locallyIntegrable.continuous_mul; Real.exp_add; hl

4. Transfer measurability to volume

Gibbs L2 initially gives strong measurability only almost everywhere for μ. The positive exponential density and finite normalization imply dx is absolutely continuous with respect to μ. Thus any exceptional μ-null set is also volume-null, and the same representative is strongly measurable almost everywhere for volume and its restrictions.

\[dx\ll\mu,\qquad a\text{ is a.e. strongly measurable for }dx|_K.\]

Corresponding Lean step

hm via AEStronglyMeasurable.mono_ac (absolutelyContinuous_tilted hI); hm.restrict

5. Restrict to an arbitrary compact set

Local integrability implies integrability on every compact K. Combine this squared-norm integral with the restricted strong measurability and apply the L2 characterization in reverse. The consumer test applies exactly this conclusion to an existing resolvent solution, its gradient, and its forcing, retaining the same weak PDE.

\[\forall K\Subset E,\quad\int_K\|a(x)\|^2\,dx<\infty\quad\Longrightarrow\quad a\in L^2(dx|_K;F).\]

Corresponding Lean step

hl.integrableOn_isCompact hK; memLp_two_iff_integrable_sq_norm hm.restrict

Lean statement · lp_locallyMemLp_volume

Exact spaces, representative coercion and compact-set quantifiers are shown in the closed disclosure.

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 lp_locallyMemLp_volume {F : Type*} [NormedAddCommGroup F]
    (W : E → ℝ) (hW : Continuous W)
    (hI : Integrable (fun x => Real.exp (-W x)))
    (a : Lp F 2 ((volume : Measure E).tilted (fun x => -W x))) :
    LocallyIntegrable (fun x => ‖a x‖ ^ 2) (volume : Measure E) ∧
      ∀ K : Set E, IsCompact K → MemLp (fun x => a x) 2 (volume.restrict K)

Exact module and namespace context

Lean proof · lp_locallyMemLp_volume

Squared norm → remove weight → invert locally → transfer measurability → compact restriction.

theorem lp_locallyMemLp_volume {F : Type*} [NormedAddCommGroup F]
    (W : E → ℝ) (hW : Continuous W)
    (hI : Integrable (fun x => Real.exp (-W x)))
    (a : Lp F 2 ((volume : Measure E).tilted (fun x => -W x))) :
    LocallyIntegrable (fun x => ‖a x‖ ^ 2) (volume : Measure E) ∧
      ∀ K : Set E, IsCompact K → MemLp (fun x => a x) 2 (volume.restrict K) := by
  have hs := (memLp_two_iff_integrable_sq_norm (Lp.memLp a).aestronglyMeasurable).mp
    (Lp.memLp a)
  have hw : Integrable (fun x => Real.exp (-W x) * ‖a x‖ ^ 2) := by
    simpa only [smul_eq_mul] using (integrable_tilted_iff hI _).mp hs
  have hl : LocallyIntegrable (fun x => ‖a x‖ ^ 2) (volume : Measure E) := by
    have h := hw.locallyIntegrable.continuous_mul (Real.continuous_exp.comp hW)
    simpa only [Function.comp_apply, ← mul_assoc, ← Real.exp_add, add_neg_cancel,
      Real.exp_zero, one_mul]
      using h
  refine ⟨hl, ?_⟩
  intro K hK
  have hm : AEStronglyMeasurable (fun x => a x) (volume : Measure E) :=
    (Lp.memLp a).aestronglyMeasurable.mono_ac (absolutelyContinuous_tilted hI)
  exact (memLp_two_iff_integrable_sq_norm hm.restrict).mpr
    (hl.integrableOn_isCompact hK)

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2

Exact module and namespace context

Scope and omitted-condition boundaries

Local square integrability only: no global unweighted L2 bound, quantitative embedding constant, derivative regularity, H2 theorem, Sobolev-domain converse, Poincare or paper completion.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.memLp_two_iff_integrable_sq_norm
MeasureTheory.Lp.memLp
MeasureTheory.integrable_tilted_iff
MeasureTheory.LocallyIntegrable.continuous_mul
MeasureTheory.absolutelyContinuous_tilted
MeasureTheory.AEStronglyMeasurable.mono_ac
MeasureTheory.LocallyIntegrable.integrableOn_isCompact

Mathematical sources

PBPS Appendix C.1: authored analytic prerequisite — Elementary localization supporting the closed-gradient/weighted-Poisson route, not a quoted paper theorem.
Kolesnikov–Milman §2.5: weighted Sobolev background — Background only; no compact-manifold regularity theorem is imported.

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