Actual compact weak Poisson: complex Schwartz, TD and Sobolev

Mathematical statement

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.

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)

Proof roadmap

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

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

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

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

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

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