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

Mathematical statement

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.

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

Proof roadmap

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

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

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

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

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

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

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