Actual compact weak Poisson: one smooth function/gradient/Laplacian sequence

Samplinglib authored actual compact ordinary smooth graph prerequisite to Chen, Chewi, Lu and Zhang AppendixC.1/SPHMC4.1 covariance-upper route; not a quoted numbered theorem or weighted core/BL/main result.

Complete source statement (Samplinglib restatement)

From the exact compact-supported volumeL2 and original weak-gradient/PDE inputs, Derive one real Schwartz sequence phi_n with one common outer compact Kprime containing every tsupport(phi_n), chosen before all n and all three limits. Actual volumeL2 classes of phi_n converge to v; actual classical gradient(phi_n) is MemLp2 and its class converges to the original G; actual Laplacian(phi_n) classes converge to F. Every phi_n is C-infinity and compactly supported. The same sequence realizes all limits. Kprime need not equal K. No classical derivatives of rough v, real Hessian family, quantitative source complexity constant or weighted operator core is claimed.

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: one smooth function/gradient/Laplacian sequence

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactPoissonSmoothGraph.compact_weak_poisson_smooth_graph_approximation · theorem · Teaching coverage

Read this first

Mathematical statement

\[\int\psi\langle G,a\rangle=-\int vD_a\psi,\quad\int v\Delta\psi=\int F\psi\ \Longrightarrow\ \exists K\prime,\varphi_n\in C_c^\infty(K\prime):\quad\varphi_n\to v,\ \nabla\varphi_n\to G,\ \Delta\varphi_n\to F\ \text{in }L^2(dx).\]

Lean statement · compact_weak_poisson_smooth_graph_approximation

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_smooth_graph_approximation
    (v F : E → ℝ) (G : E → E) (K : Set E) (hK : IsCompact K)
    (hv : tsupport v ⊆ K) (hF : tsupport F ⊆ K) (hG : tsupport G ⊆ K)
    (hv2 : MemLp v 2 volume) (hF2 : MemLp F 2 volume) (hG2 : MemLp G 2 volume)
    (hd : ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => ψ x * inner ℝ (G x) a) volume ∧
      Integrable (fun x => v x * fderiv ℝ ψ x a) volume ∧
      (∫ x, ψ x * inner ℝ (G x) a) = -∫ x, v x * fderiv ℝ ψ x a)
    (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) :
    ∃ K' : Set E, IsCompact K' ∧ ∃ φ : ℕ → SchwartzMap E ℝ,
      (∀ n, tsupport (φ n) ⊆ K') ∧
      Filter.Tendsto (fun n => (φ n).toLp 2 volume) Filter.atTop (𝓝 (hv2.toLp v)) ∧
      ∃ hφG : ∀ n, MemLp (gradient (φ n : E → ℝ)) 2 volume,
        Filter.Tendsto (fun n => (hφG n).toLp (gradient (φ n : E → ℝ)))
          Filter.atTop (𝓝 (hG2.toLp G)) ∧
        Filter.Tendsto (fun n => (Δ (φ n)).toLp 2 volume)
          Filter.atTop (𝓝 (hF2.toLp F))

Exact module and namespace context

Proof roadmap

1Derive the actual Bessel-L2 witness from the original compact PDE
Call the accepted real compact-test producer with actual supports and L2 data. It constructs AE-linked complex classes vc/Fc, the true TD Laplacian and Sobolev2. Choose the genuine order2 L2 witness w and invert Bessel; plain L2 approximation of v would not control derivatives.
2Construct chosen norm-controlled continuous L2 spectral maps
For each actual bounded temperate complex symbol g, use its genuine Linfinity class, Holder infinity/2/2 bilinear CLM and forward/inverse L2 Fourier isometries to construct A_g. Prove norm(A_g f)≤C norm(f), true Lp/TD compatibility and equality with Schwartz multipliers by LpTD injectivity. The symbols m0, inner(x,a)*m0 and norm(x)^2*m0 have bounds1,norm(a),1; attach exact2pi i and -(2pi)^2 scalars to derivatives.
3Use one Schwartz approximation of w for every graph component
Actual L2 density and sequential closure choose q_n.toLp → w. Define s_n=FM(m0)q_n. Continuity of the chosen fixed maps gives same-sequence function, Laplacian and every direction derivative limits. Identify function with vc through true Bessel inversion, and Laplacian with Fc through the actual TD PDE/injectivity. Preserve exact complex casts/Fourier normalization.
4Identify the original real gradient, not a newly chosen derivative
The actual spectral limit satisfies T_ga=D_a T_vc. Test it with ofReal of each genuine real compact smooth test, use actual HolderL1 before integral_re, and compare with the original all-C1 weak gradient. Locally integrable compact-test uniqueness identifies Re ga=inner(G,a) AE. Continuous real projection and finite orthonormal-basis reconstruction give the actual full vector-gradient limit; dimension0 has an empty basis.
5Construct one fixed outer plateau and all bounded coefficient maps
Choose an actual unnormalized smooth compact theta equal1 near K. Its genuine Schwartz function, gradient and Laplacian supply actual Linfinity coefficients; Holder gives continuous maps on real/vectorL2. Neighborhood locality makes gradtheta/Deltatheta zero on K, while actual v/G/F vanish outsideK. Derive exact limiting identities and zero cross terms without weighted tails or extra position moments.
6Apply actual product rules to the same sequence
Set phi_n=theta*Re s_n, a genuine smooth compact function with common supportKprime. Reuse the existing public gradient product rule and the canonical local-C2 LaplacianProduct.laplacian_mul at each point. The already globally smooth factors discharge its local regularity. Actual quotient/AE products and continuous bounded coefficient maps pass all three identities to the limit; the duplicate private Laplacian calculus is removed.
7Return actual compact graph convergence and stop before weighted core
Expose real Schwartz approximants/common compact support, actual gradient MemLp witnesses and true function/gradient/Laplacian quotient convergence from input L2 proofs. Weighted transfer, original localized D-domain membership, adjoint/generator identification, global cutoff removal/Bochner/Poincare/BL and source main guarantees remain distinct producers.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real Hilbert/Borel space E with canonical ordinary full-space volume, including dimension zero. Real pointwise v,F and vector G are genuinely global volumeL2; their topological supports lie in the same compact K.
Every real C1 compact test psi and every a satisfies both L1 products and integral psi*inner(G,a)=-integral v*D_a psi. Every real C2 compact psi has both L1 products and integral v*Delta psi=integral F*psi. These actual weak equations, measurability/L2 and supports are inputs; graph density, Sobolev membership, smooth sequence, real mixed Hessian and weighted core are not supplied.
The rough v/G/F representatives are differentiated only in the actual weak/distributional sense. Classical gradients and Laplacians in the conclusion belong to actual smooth approximants. SchwartzMap E real is genuinely C-infinity/rapidly decaying; common compact support is additionally derived. No positive dimension, jointly measurable selector, source C-infinity potential or normalized plateau is assumed.

Mathematical proof

1. Derive the actual Bessel-L2 witness from the original compact PDE

Call the accepted real compact-test producer with actual supports and L2 data. It constructs AE-linked complex classes vc/Fc, the true TD Laplacian and Sobolev2. Choose the genuine order2 L2 witness w and invert Bessel; plain L2 approximation of v would not control derivatives.

\[B_2T_v=T_w,\quad B_2=I-(2\pi)^{-2}\Delta,\quad B_{-2}T_w=T_v.\]

Corresponding Lean step

CompactWeakPoissonSobolev.compact_weak_poisson_sobolev; spectral_graph

2. Construct chosen norm-controlled continuous L2 spectral maps

For each actual bounded temperate complex symbol g, use its genuine Linfinity class, Holder infinity/2/2 bilinear CLM and forward/inverse L2 Fourier isometries to construct A_g. Prove norm(A_g f)≤C norm(f), true Lp/TD compatibility and equality with Schwartz multipliers by LpTD injectivity. The symbols m0, inner(x,a)*m0 and norm(x)^2*m0 have bounds1,norm(a),1; attach exact2pi i and -(2pi)^2 scalars to derivatives.

\[A_g=\mathcal F^{-1}(g\,\mathcal F\cdot),\quad\|A_gf\|_2\le C\|f\|_2;\quad m_0=(1+\|\xi\|^2)^{-1}.\]

Corresponding Lean step

actualMul; actual_bounded_multiplier_norm; mzero_bound; mdir_bound; mlap_bound; inverse_dir; inverse_lap

3. Use one Schwartz approximation of w for every graph component

Actual L2 density and sequential closure choose q_n.toLp → w. Define s_n=FM(m0)q_n. Continuity of the chosen fixed maps gives same-sequence function, Laplacian and every direction derivative limits. Identify function with vc through true Bessel inversion, and Laplacian with Fc through the actual TD PDE/injectivity. Preserve exact complex casts/Fourier normalization.

\[s_n=A_{m_0}q_n,\quad s_n\to v_C,\quad\Delta s_n\to F_C,\quad D_as_n\to g_a.\]

Corresponding Lean step

schwartz_approx; spectral_graph; besselPotential_neg_apply_eq_iff; lp_td_injective

4. Identify the original real gradient, not a newly chosen derivative

The actual spectral limit satisfies T_ga=D_a T_vc. Test it with ofReal of each genuine real compact smooth test, use actual HolderL1 before integral_re, and compare with the original all-C1 weak gradient. Locally integrable compact-test uniqueness identifies Re ga=inner(G,a) AE. Continuous real projection and finite orthonormal-basis reconstruction give the actual full vector-gradient limit; dimension0 has an empty basis.

\[\operatorname{Re}g_a=_{dx\text{-ae}}\langle G,a\rangle,\quad\operatorname{Re}s_n\to v,\quad\nabla\operatorname{Re}s_n\to G,\quad\Delta\operatorname{Re}s_n\to F.\]

Corresponding Lean step

identify_real_gradient; real_projection_class; finite_gradient_reconstruction; real_schwartz_graph

5. Construct one fixed outer plateau and all bounded coefficient maps

Choose an actual unnormalized smooth compact theta equal1 near K. Its genuine Schwartz function, gradient and Laplacian supply actual Linfinity coefficients; Holder gives continuous maps on real/vectorL2. Neighborhood locality makes gradtheta/Deltatheta zero on K, while actual v/G/F vanish outsideK. Derive exact limiting identities and zero cross terms without weighted tails or extra position moments.

\[\theta=1\text{ near }K,\quad\nabla\theta=\Delta\theta=0\text{ on }K,\quad K\prime=\operatorname{tsupp}\theta.\]

Corresponding Lean step

outer_plateau; coeff_holder_ae; coeff_holder_class; plateau_point_identities

6. Apply actual product rules to the same sequence

Set phi_n=theta*Re s_n, a genuine smooth compact function with common supportKprime. Reuse the existing public gradient product rule and the canonical local-C2 LaplacianProduct.laplacian_mul at each point. The already globally smooth factors discharge its local regularity. Actual quotient/AE products and continuous bounded coefficient maps pass all three identities to the limit; the duplicate private Laplacian calculus is removed.

\[\nabla(\theta r_n)=\theta\nabla r_n+r_n\nabla\theta;\quad\Delta(\theta r_n)=\theta\Delta r_n+2\langle\nabla\theta,\nabla r_n\rangle+r_n\Delta\theta.\]

Corresponding Lean step

GradientAlgebra.gradient_mul_eq_of_differentiableAt; AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LaplacianProduct.laplacian_mul; cutoff_schwartz_graph

7. Return actual compact graph convergence and stop before weighted core

Expose real Schwartz approximants/common compact support, actual gradient MemLp witnesses and true function/gradient/Laplacian quotient convergence from input L2 proofs. Weighted transfer, original localized D-domain membership, adjoint/generator identification, global cutoff removal/Bochner/Poincare/BL and source main guarantees remain distinct producers.

\[\varphi_n\to v,\quad\nabla\varphi_n\to G,\quad\Delta\varphi_n\to F\text{ in }L^2(dx);\quad\text{weighted core remains open}.\]

Corresponding Lean step

compact_weak_poisson_smooth_graph_approximation

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_smooth_graph_approximation

Derive the actual Bessel-L2 witness from the original compact PDE; Construct chosen norm-controlled continuous L2 spectral maps; Use one Schwartz approximation of w for every graph component; Identify the original real gradient, not a newly chosen derivative; Construct one fixed outer plateau and all bounded coefficient maps; Apply actual product rules to the same sequence; Return actual compact graph convergence and stop before weighted core

Download module (.lean)

theorem compact_weak_poisson_smooth_graph_approximation
    (v F : E → ℝ) (G : E → E) (K : Set E) (hK : IsCompact K)
    (hv : tsupport v ⊆ K) (hF : tsupport F ⊆ K) (hG : tsupport G ⊆ K)
    (hv2 : MemLp v 2 volume) (hF2 : MemLp F 2 volume) (hG2 : MemLp G 2 volume)
    (hd : ∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => ψ x * inner ℝ (G x) a) volume ∧
      Integrable (fun x => v x * fderiv ℝ ψ x a) volume ∧
      (∫ x, ψ x * inner ℝ (G x) a) = -∫ x, v x * fderiv ℝ ψ x a)
    (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) :
    ∃ K' : Set E, IsCompact K' ∧ ∃ φ : ℕ → SchwartzMap E ℝ,
      (∀ n, tsupport (φ n) ⊆ K') ∧
      Filter.Tendsto (fun n => (φ n).toLp 2 volume) Filter.atTop (𝓝 (hv2.toLp v)) ∧
      ∃ hφG : ∀ n, MemLp (gradient (φ n : E → ℝ)) 2 volume,
        Filter.Tendsto (fun n => (hφG n).toLp (gradient (φ n : E → ℝ)))
          Filter.atTop (𝓝 (hG2.toLp G)) ∧
        Filter.Tendsto (fun n => (Δ (φ n)).toLp 2 volume)
          Filter.atTop (𝓝 (hF2.toLp F)) := by
  obtain ⟨vc,Fc,hvc,hFc,_,hl,hs⟩ :=
    CompactWeakPoissonSobolev.compact_weak_poisson_sobolev v F K hK hv hF hv2 hF2 hweak
  obtain ⟨r,hrv,hrG,hrF⟩ := real_schwartz_graph v F G hv2 hF2 hG2 vc Fc hvc hFc hs hl hd
  obtain ⟨K',hK',φ,hφs,hφv,hφG,hφF⟩ :=
    cutoff_schwartz_graph v F G K hK hv hF hG hv2 hF2 hG2 r hrv hrG hrF
  have hφgrad (n : ℕ) : MemLp (gradient (φ n : E → ℝ)) 2 volume := by
    have he : (schwartz_gradient (φ n) : E → E) = gradient (φ n : E → ℝ) := by
      funext x; exact schwartz_gradient_apply (φ n) x
    rw [← he]
    exact (schwartz_gradient (φ n)).memLp 2 volume
  have heq (n : ℕ) : (hφgrad n).toLp (gradient (φ n : E → ℝ)) =
      (schwartz_gradient (φ n)).toLp 2 volume := by
    apply Lp.ext
    filter_upwards [(hφgrad n).coeFn_toLp,(schwartz_gradient (φ n)).coeFn_toLp 2 volume]
      with x hx hy
    rw [hx,hy,schwartz_gradient_apply]
  exact ⟨K',hK',φ,hφs,hφv,hφgrad,by simpa only [heq] using hφG,hφF⟩

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactPoissonSmoothGraph

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source C2 curvature-bounded reflected conditional route.	Finite-dimensional real Hilbert/Borel space E with canonical ordinary full-space volume, including dimension zero. Real pointwise v,F and vector G are genuinely global volumeL2; their topological supports lie in the same compact K. Every real C1 compact test psi and every a satisfies both L1 products and integral psiinner(G,a)=-integral vD_a psi. Every real C2 compact psi has both L1 products and integral vDelta psi=integral Fpsi. These actual weak equations, measurability/L2 and supports are inputs; graph density, Sobolev membership, smooth sequence, real mixed Hessian and weighted core are not supplied. The rough v/G/F representatives are differentiated only in the actual weak/distributional sense. Classical gradients and Laplacians in the conclusion belong to actual smooth approximants. SchwartzMap E real is genuinely C-infinity/rapidly decaying; common compact support is additionally derived. No positive dimension, jointly measurable selector, source C-infinity potential or normalized plateau is assumed.	generalization	Generic weak-gradient/PDE compact graph interface is disclosed; actual source V C2/curvature/eta and reflected law/ordinary volume retained including zero dimension.
Smooth-test/density analytic details omitted in AppendixC.1; no Laplacian graph sequence supplied.	From the exact compact-supported volumeL2 and original weak-gradient/PDE inputs, Derive one real Schwartz sequence phi_n with one common outer compact Kprime containing every tsupport(phi_n), chosen before all n and all three limits. Actual volumeL2 classes of phi_n converge to v; actual classical gradient(phi_n) is MemLp2 and its class converges to the original G; actual Laplacian(phi_n) classes converge to F. Every phi_n is C-infinity and compactly supported. The same sequence realizes all limits. Kprime need not equal K. No classical derivatives of rough v, real Hessian family, quantitative source complexity constant or weighted operator core is claimed.	source-implicit	Derive actual Bessel witness, chosen continuous spectral maps, original real-gradient identification and one common compact triple-limit sequence; no final approximation/core certificate assumed.
Poincare/macroscopic extension and SPHMC4.1 BL covariance bound.	Derive one real smooth sequence with common outer compact support and simultaneous actual ordinary-volume L2 function/gradient/Laplacian limits for v=chiu, g=chiG+ugradientchi, F=chir+2inner(gradientchi,G)+u*laplacianchi. Same original D before epsilon/f, same u before ALL cutoffs. No supplied graph-density/approximation/mixedHessian/core certificate, no classical rough derivatives, no weighted-domain/operator-core/globalcutoff/Bochner/BL/Poincare/jointmeasurablechoice/main/composition claim. Reflected/RGO quarter Hessian and fourfold energy kept distinct; TV never transfers unbounded cost.	unresolved	Fixed compact ordinary-volume graph approximation does not establish weighted generator domain/core, global cutoff removal/Bochner, epsilon0, source full4.1 or either main/composition.

Derive one real smooth sequence with common outer compact support and simultaneous actual ordinary-volume L2 function/gradient/Laplacian limits for v=chi*u, g=chi*G+u*gradientchi, F=chi*r+2inner(gradientchi,G)+u*laplacianchi. Same original D before epsilon/f, same u before ALL cutoffs. No supplied graph-density/approximation/mixedHessian/core certificate, no classical rough derivatives, no weighted-domain/operator-core/globalcutoff/Bochner/BL/Poincare/jointmeasurablechoice/main/composition claim. Reflected/RGO quarter Hessian and fourfold energy kept distinct; TV never transfers unbounded cost.

Encoder–denoiser: accepted · equivalent-after-elaboration

Detected semantic differences

assumptions: The current whole module imports one canonical local-C2 Laplacian product theorem. Its actual cutoff application specializes the globally smooth Schwartz factors to ContDiffAt R 2 at each x. This changes proof infrastructure without adding any public input or conclusion. — cutoff_schwartz_graph.hqF calls LaplacianProduct.laplacian_mul with (theta.smooth 2).contDiffAt and ((r n).smooth 2).contDiffAt.
scopes: The authored source/restatement is an analytic prerequisite, not a quoted PBPS/SPHMC theorem. Exact compact ordinary-volume graph convergence does not discharge weighted core or source main results. — Source original_text and candidate source scope; public statement and actual consumer quantifier order. No old source verdict was reused.

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 one real smooth sequence with common outer compact support and simultaneous actual ordinary-volume L2 function/gradient/Laplacian limits for v=chi*u, g=chi*G+u*gradientchi, F=chi*r+2inner(gradientchi,G)+u*laplacianchi. Same original D before epsilon/f, same u before ALL cutoffs. No supplied graph-density/approximation/mixedHessian/core certificate, no classical rough derivatives, no weighted-domain/operator-core/globalcutoff/Bochner/BL/Poincare/jointmeasurablechoice/main/composition claim. Reflected/RGO quarter Hessian and fourfold energy kept distinct; TV never transfers unbounded cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

SchwartzMap.denseRange_toLpCLM
Lp.fourierTransformₗᵢ
Lp.toTemperedDistribution_smul_eq
Lp.ker_toTemperedDistributionCLM_eq_bot
ContinuousLinearMap.holderL
SchwartzMap.fourierMultiplierCLM
besselPotential_neg_apply_eq_iff
ae_eq_of_integral_contDiff_smul_eq
ContinuousLinearMap.compLpL
ContDiffBump.eventuallyEq_one_of_mem_ball

Mathematical sources

PBPS AppendixC.1 authored analytic prerequisite — Derive one real smooth sequence with common outer compact support and simultaneous actual ordinary-volume L2 function/gradient/Laplacian limits for v=chi*u, g=chi*G+u*gradientchi, F=chi*r+2inner(gradientchi,G)+u*laplacianchi. Same original D before epsilon/f, same u before ALL cutoffs. No supplied graph-density/approximation/mixedHessian/core certificate, no classical rough derivatives, no weighted-domain/operator-core/globalcutoff/Bochner/BL/Poincare/jointmeasurablechoice/main/composition claim. Reflected/RGO quarter Hessian and fourfold energy kept distinct; TV never transfers 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: one smooth function/gradient/Laplacian sequence

Complete source statement (Samplinglib restatement)

Actual compact weak Poisson: one smooth function/gradient/Laplacian sequence

Read the formalized proofs

Actual compact weak Poisson: one smooth function/gradient/Laplacian sequence

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Derive the actual Bessel-L2 witness from the original compact PDE

2. Construct chosen norm-controlled continuous L2 spectral maps

3. Use one Schwartz approximation of w for every graph component

4. Identify the original real gradient, not a newly chosen derivative

5. Construct one fixed outer plateau and all bounded coefficient maps

6. Apply actual product rules to the same sequence

7. Return actual compact graph convergence and stop before weighted core

Lean verification

Source assumptions versus formal assumptions

Detected semantic differences

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?