Actual compact weak Poisson: complex Schwartz, TD and Sobolev

Samplinglib explicit compact-Schwartz/TD/Bessel-Sobolev analytic prerequisite to Chen, Chewi, Lu and Zhang AppendixC.1; not a quoted numbered theorem, conditional Poincare or completed source result.

Complete source statement (Samplinglib restatement)

Under the exact ordinary-volume global L2/support and real compact-C2 PDE assumptions, Construct actual vc,Fc in complex L2(volume), with vc=volume-a.e. ofReal(v) and Fc=volume-a.e. ofReal(F). For every complex Schwartz psi, both (Delta psi)*ofReal(v) and psi*ofReal(F) are L1 and their integrals equal. For T_v=Lp.toTemperedDistribution(vc) and T_F=Lp.toTemperedDistribution(Fc), derive Delta T_v=T_F and MemSobolev 2 2 T_v. The latter uses B2 T=T-(2pi)^(-2) Delta T and a genuine complex L2 witness, not a supplied regularity result.

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

Actual compact weak Poisson: complex Schwartz, TD and Sobolev

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeakPoissonSobolev.compact_weak_poisson_sobolev · theorem · Teaching coverage

Read this first

Mathematical statement

\[v,F\in L^2(dx),\ \operatorname{tsupp}(v),\operatorname{tsupp}(F)\subseteq K;\quad\int v\Delta\varphi=\int F\varphi\ (\varphi\in C_c^2)\ \Longrightarrow\ \Delta T_v=T_F,\quad B_2T_v=T_v-(2\pi)^{-2}T_F\in\operatorname{LpTD}(L^2),\quad T_v\in H^2_{\rm Bessel}.\]

Lean statement · compact_weak_poisson_sobolev

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 compact_weak_poisson_sobolev (v F : E → ℝ) (K : Set E)
    (hK : IsCompact K) (hv : tsupport v ⊆ K) (hF : tsupport F ⊆ K)
    (hv2 : MemLp v 2 volume) (hF2 : MemLp F 2 volume)
    (hweak : ∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
      Integrable (fun x => v x * (Δ φ) x) volume ∧
      Integrable (fun x => F x * φ x) volume ∧
      (∫ x, v x * (Δ φ) x) = ∫ x, F x * φ x) :
    ∃ vc Fc : Lp ℂ 2 (volume : Measure E),
      vc =ᵐ[volume] (fun x => (v x : ℂ)) ∧
      Fc =ᵐ[volume] (fun x => (F x : ℂ)) ∧
      (∀ ψ : SchwartzMap E ℂ,
        Integrable (fun x => (Δ ψ) x * (v x : ℂ)) volume ∧
        Integrable (fun x => ψ x * (F x : ℂ)) volume ∧
        (∫ x, (Δ ψ) x * (v x : ℂ)) = ∫ x, ψ x * (F x : ℂ)) ∧
      Δ (Lp.toTemperedDistribution vc) = Lp.toTemperedDistribution Fc ∧
      MemSobolev 2 2 (Lp.toTemperedDistribution vc)

Exact module and namespace context

Proof roadmap

1Enclose the actual supports with one smooth outer plateau
Use compactness to choose a positive inner radius enclosing K strictly. The actual unnormalized smooth bump theta has larger outer radius, compact support and equals1 in a neighborhood of each x in K. No normalized mollifier, tail limit, derivative-bound certificate or positive-dimension premise is used.
2Actually extend real tests to every complex Schwartz test
For arbitrary psi test the given real PDE with theta*Re psi and theta*Im psi. These are genuine C2 compact tests. Laplacian locality and real-linear CLM composition derive Delta(theta Re psi)=Re(Delta psi) on K, and likewise imaginary part; outside K the actual v/F are zero. The same theta/K works independently of psi.
3Prove legal complex products before combining integrals
Actual global volume L2, MemLp.ofReal and Schwartz L2 of psi and Delta psi yield both bilinear products L1 through Holder2/2/1. Only then integral_re/integral_im and Complex.ext combine the genuine real equalities. There is no complex conjugation or conjugated inner-product substitution.
4Build and identify actual AE-linked L2 distributions
Build vc/Fc using actual complex MemLp.toLp. State their volume-AE equalities explicitly before each integral transfer. The genuine LpTD pairing is integral psi*vc. Its distribution Laplacian acts on Delta psi with positive sign, giving Delta T_v=T_F by extensionality on all complex Schwartz tests; no class-support claim is made for the selected quotient representatives.
5Construct the Fourier-normalized Bessel witness
Order2 Bessel multiplier is 1+norm(x)^2. The pinned Fourier Laplacian is -(2pi)^2 times the norm-square multiplier. Actual multiplier linearity and real-to-complex scalar cancellation derive B2 T=T-(2pi)^(-2) Delta T. The complex L2 class vc-(a:complex)*Fc witnesses the definition, equivalently using the true L2 embeddings and their subtraction/scalar linearity.
6Return this exact interface and retain its boundary
Return the actual classes, AE links, both complex integrabilities/all-Schwartz equation, TD Laplacian and Bessel-Sobolev membership. Dimension0 needs no unit vector or division by dimension. Real mixed-second representatives/Hessian, original weighted closure-domain/core and Bochner extension are separate next producers; neither BL/Poincare nor a source main theorem follows here.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real Hilbert space with Borel measurable structure and canonical full-space volume, including dimension zero. v and F are real pointwise functions with genuine global volume MemLp2; K is compact and tsupport v and tsupport F are contained in K.
For every real C2 compact phi, v*Delta phi and F*phi are integrable for volume and integral v*Delta phi=integral F*phi. This generic analytic interface is consumed with these inputs actually derived by the same-D localized resolvent; no all-Schwartz, TD equation or final Sobolev certificate is supplied.
All rough functions/class representatives are differentiated only as distributions. Complex test derivatives are real Frechet derivatives on E, real/imaginary projections are real-linear CLMs, and the complex TD pairing is bilinear integral psi*v without conjugation. No Nontrivial or positive-dimensional assumption is added.

Mathematical proof

1. Enclose the actual supports with one smooth outer plateau

Use compactness to choose a positive inner radius enclosing K strictly. The actual unnormalized smooth bump theta has larger outer radius, compact support and equals1 in a neighborhood of each x in K. No normalized mollifier, tail limit, derivative-bound certificate or positive-dimension premise is used.

\[K\subset B(0,R),\quad\theta\in C_c^\infty,\quad\theta=1\ \text{near every }x\in K.\]

Corresponding Lean step

outer_cutoff; Bornology.IsBounded.subset_ball_lt; ContDiffBump.eventuallyEq_one_of_mem_ball

2. Actually extend real tests to every complex Schwartz test

For arbitrary psi test the given real PDE with theta*Re psi and theta*Im psi. These are genuine C2 compact tests. Laplacian locality and real-linear CLM composition derive Delta(theta Re psi)=Re(Delta psi) on K, and likewise imaginary part; outside K the actual v/F are zero. The same theta/K works independently of psi.

\[\int v\operatorname{Re}(\Delta\psi)=\int F\operatorname{Re}\psi,\qquad\int v\operatorname{Im}(\Delta\psi)=\int F\operatorname{Im}\psi.\]

Corresponding Lean step

real_schwartz_component; laplacian_congr_nhds; ContDiffAt.laplacian_CLM_comp_left; image_eq_zero_of_notMem_tsupport

3. Prove legal complex products before combining integrals

Actual global volume L2, MemLp.ofReal and Schwartz L2 of psi and Delta psi yield both bilinear products L1 through Holder2/2/1. Only then integral_re/integral_im and Complex.ext combine the genuine real equalities. There is no complex conjugation or conjugated inner-product substitution.

\[\int(\Delta\psi)(v:\mathbb C)=\int\psi(F:\mathbb C),\quad(\Delta\psi)v,\psi F\in L^1(dx).\]

Corresponding Lean step

complex_schwartz_pde; MemLp.integrable_mul; integral_re; integral_im; Complex.ext

4. Build and identify actual AE-linked L2 distributions

Build vc/Fc using actual complex MemLp.toLp. State their volume-AE equalities explicitly before each integral transfer. The genuine LpTD pairing is integral psi*vc. Its distribution Laplacian acts on Delta psi with positive sign, giving Delta T_v=T_F by extensionality on all complex Schwartz tests; no class-support claim is made for the selected quotient representatives.

\[v_C=_{dx\text{-ae}}(v:\mathbb C),\quad F_C=_{dx\text{-ae}}(F:\mathbb C),\quad\Delta T_v=T_F.\]

Corresponding Lean step

actual_tempered_laplacian; MemLp.coeFn_toLp; Lp.toTemperedDistribution_apply; TemperedDistribution.laplacian_apply_apply

5. Construct the Fourier-normalized Bessel witness

Order2 Bessel multiplier is 1+norm(x)^2. The pinned Fourier Laplacian is -(2pi)^2 times the norm-square multiplier. Actual multiplier linearity and real-to-complex scalar cancellation derive B2 T=T-(2pi)^(-2) Delta T. The complex L2 class vc-(a:complex)*Fc witnesses the definition, equivalently using the true L2 embeddings and their subtraction/scalar linearity.

\[a=(2\pi)^{-2},\quad B_2T_v=\operatorname{LpTD}(v_C-aF_C),\quad\mathrm{MemSobolev}\ 2\ 2\ T_v.\]

Corresponding Lean step

bessel_two_identity; laplacian_eq_fourierMultiplierCLM; sobolev_of_compact_pde; memSobolev_zero_iff; MemSobolev.sub; MemSobolev.smul

6. Return this exact interface and retain its boundary

Return the actual classes, AE links, both complex integrabilities/all-Schwartz equation, TD Laplacian and Bessel-Sobolev membership. Dimension0 needs no unit vector or division by dimension. Real mixed-second representatives/Hessian, original weighted closure-domain/core and Bochner extension are separate next producers; neither BL/Poincare nor a source main theorem follows here.

\[\text{actual complex Bessel-Sobolev interface};\quad\text{real Hessian/core/BL remain open}.\]

Corresponding Lean step

compact_weak_poisson_sobolev

Lean verification

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

Lean proof · compact_weak_poisson_sobolev

Enclose the actual supports with one smooth outer plateau; Actually extend real tests to every complex Schwartz test; Prove legal complex products before combining integrals; Build and identify actual AE-linked L2 distributions; Construct the Fourier-normalized Bessel witness; Return this exact interface and retain its boundary

Download module (.lean)

theorem compact_weak_poisson_sobolev (v F : E → ℝ) (K : Set E)
    (hK : IsCompact K) (hv : tsupport v ⊆ K) (hF : tsupport F ⊆ K)
    (hv2 : MemLp v 2 volume) (hF2 : MemLp F 2 volume)
    (hweak : ∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
      Integrable (fun x => v x * (Δ φ) x) volume ∧
      Integrable (fun x => F x * φ x) volume ∧
      (∫ x, v x * (Δ φ) x) = ∫ x, F x * φ x) :
    ∃ vc Fc : Lp ℂ 2 (volume : Measure E),
      vc =ᵐ[volume] (fun x => (v x : ℂ)) ∧
      Fc =ᵐ[volume] (fun x => (F x : ℂ)) ∧
      (∀ ψ : SchwartzMap E ℂ,
        Integrable (fun x => (Δ ψ) x * (v x : ℂ)) volume ∧
        Integrable (fun x => ψ x * (F x : ℂ)) volume ∧
        (∫ x, (Δ ψ) x * (v x : ℂ)) = ∫ x, ψ x * (F x : ℂ)) ∧
      Δ (Lp.toTemperedDistribution vc) = Lp.toTemperedDistribution Fc ∧
      MemSobolev 2 2 (Lp.toTemperedDistribution vc) := by
  let vc : Lp ℂ 2 (volume : Measure E) :=
    (hv2.ofReal (K := ℂ)).toLp (fun x => (v x : ℂ))
  let Fc : Lp ℂ 2 (volume : Measure E) :=
    (hF2.ofReal (K := ℂ)).toLp (fun x => (F x : ℂ))
  refine ⟨vc,Fc,(hv2.ofReal (K := ℂ)).coeFn_toLp,
    (hF2.ofReal (K := ℂ)).coeFn_toLp,?_,
    actual_tempered_laplacian v F K hK hv hF hv2 hF2 hweak,
    sobolev_of_compact_pde v F K hK hv hF hv2 hF2 hweak⟩
  intro ψ
  exact ⟨((Δ ψ).memLp 2 volume).integrable_mul hv2.ofReal,
    (ψ.memLp 2 volume).integrable_mul hF2.ofReal,
    complex_schwartz_pde v F K hK hv hF hv2 hF2 hweak ψ⟩

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeakPoissonSobolev

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source Euclidean C2 positive-curvature reflected conditional route.	E is a finite-dimensional real Hilbert space with Borel measurable structure and canonical full-space volume, including dimension zero. v and F are real pointwise functions with genuine global volume MemLp2; K is compact and tsupport v and tsupport F are contained in K. For every real C2 compact phi, vDelta phi and Fphi are integrable for volume and integral vDelta phi=integral Fphi. This generic analytic interface is consumed with these inputs actually derived by the same-D localized resolvent; no all-Schwartz, TD equation or final Sobolev certificate is supplied. All rough functions/class representatives are differentiated only as distributions. Complex test derivatives are real Frechet derivatives on E, real/imaginary projections are real-linear CLMs, and the complex TD pairing is bilinear integral psi*v without conjugation. No Nontrivial or positive-dimensional assumption is added.	generalization	Generic real compact-C2 weak Poisson interface, finite Hilbert/Borel/zero dimension, ordinary volume and complex distributions are disclosed; actual source V C2/curvature/eta cap and reflected law unchanged.
AppendixC.1 domain extension omits this real-test/Schwartz/Sobolev adapter.	Under the exact ordinary-volume global L2/support and real compact-C2 PDE assumptions, Construct actual vc,Fc in complex L2(volume), with vc=volume-a.e. ofReal(v) and Fc=volume-a.e. ofReal(F). For every complex Schwartz psi, both (Delta psi)ofReal(v) and psiofReal(F) are L1 and their integrals equal. For T_v=Lp.toTemperedDistribution(vc) and T_F=Lp.toTemperedDistribution(Fc), derive Delta T_v=T_F and MemSobolev 2 2 T_v. The latter uses B2 T=T-(2pi)^(-2) Delta T and a genuine complex L2 witness, not a supplied regularity result.	source-implicit	Derive all-Schwartz tests/actual AE-linked L2TD Laplacian and Fourier-normalized Sobolev witness; neither final Schwartz equation nor H2/core certificate supplied.
Source Poincare/macroscopic extension and SPHMC4.1 BL covariance bound.	Derive actual all-complex-Schwartz tested PDE with both products L1, genuine complex volume-L2 classes/AE embeddings, actual TD Laplacian and MemSobolev2 using B2=I-(2pi)^-2 Delta. Genuine conditional same originalD before epsilon/f, one actualu before allC2 compactcutoffs; retain parent properties. No real mixed-second representatives/Hessian, original weighted localized-domain membership/core/Bochner, BL/Poincare/epsilon0/measurable fiber selector/full4.1/main/composition. Reflected/RGO laws/operators/scales distinct; TV does not transfer unbounded cost.	unresolved	Complex Bessel-Sobolev alone does not certify real mixed-second reps, original weighted core/Bochner/coercivity, law/operator scale adapter, source full4.1 or main/composition.

Derive actual all-complex-Schwartz tested PDE with both products L1, genuine complex volume-L2 classes/AE embeddings, actual TD Laplacian and MemSobolev2 using B2=I-(2pi)^-2 Delta. Genuine conditional same originalD before epsilon/f, one actualu before allC2 compactcutoffs; retain parent properties. No real mixed-second representatives/Hessian, original weighted localized-domain membership/core/Bochner, BL/Poincare/epsilon0/measurable fiber selector/full4.1/main/composition. Reflected/RGO laws/operators/scales distinct; TV does not transfer unbounded cost.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

Derive actual all-complex-Schwartz tested PDE with both products L1, genuine complex volume-L2 classes/AE embeddings, actual TD Laplacian and MemSobolev2 using B2=I-(2pi)^-2 Delta. Genuine conditional same originalD before epsilon/f, one actualu before allC2 compactcutoffs; retain parent properties. No real mixed-second representatives/Hessian, original weighted localized-domain membership/core/Bochner, BL/Poincare/epsilon0/measurable fiber selector/full4.1/main/composition. Reflected/RGO laws/operators/scales distinct; TV does not transfer unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

ContDiffBump.eventuallyEq_one_of_mem_ball
laplacian_congr_nhds
ContDiffAt.laplacian_CLM_comp_left
SchwartzMap.laplacian_apply
SchwartzMap.memLp
MemLp.ofReal
MemLp.integrable_mul
MemLp.coeFn_toLp
Lp.toTemperedDistribution_apply
TemperedDistribution.laplacian_apply_apply
TemperedDistribution.laplacian_eq_fourierMultiplierCLM
memSobolev_zero_iff
MemSobolev.sub
MemSobolev.smul

Mathematical sources

PBPS AppendixC.1 authored analytic prerequisite — Derive actual all-complex-Schwartz tested PDE with both products L1, genuine complex volume-L2 classes/AE embeddings, actual TD Laplacian and MemSobolev2 using B2=I-(2pi)^-2 Delta. Genuine conditional same originalD before epsilon/f, one actualu before allC2 compactcutoffs; retain parent properties. No real mixed-second representatives/Hessian, original weighted localized-domain membership/core/Bochner, BL/Poincare/epsilon0/measurable fiber selector/full4.1/main/composition. Reflected/RGO laws/operators/scales distinct; TV does not transfer unbounded cost.

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

Actual compact weak Poisson: complex Schwartz, TD and Sobolev

Complete source statement (Samplinglib restatement)

Actual compact weak Poisson: complex Schwartz, TD and Sobolev

Read the formalized proofs

Actual compact weak Poisson: complex Schwartz, TD and Sobolev

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Enclose the actual supports with one smooth outer plateau

2. Actually extend real tests to every complex Schwartz test

3. Prove legal complex products before combining integrals

4. Build and identify actual AE-linked L2 distributions

5. Construct the Fourier-normalized Bessel witness

6. Return this exact interface and retain its boundary

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?