Samplinglib mathematical lesson

The actual weighted weak resolvent satisfies an ordinary distribution Laplace equation

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.OrdinaryWeakResolvent.weak_resolvent_laplacian · theorem · Teaching coverage

Read this first

Mathematical statement

For actual mu=volume.tilted(-W), the same exact closable compact smooth gradient D, every epsilon>0 and genuine L2(mu) forcing f, construct u in D.closure.domain satisfying the all-domain variational equation. Its actual G=D.closure u is the ordinary weak gradient, with locally volume-integrable u/G and every C1 compact directional identity and both integrable products. Put k=epsilon u+inner(gradient W,G)-f. Prove locally integrable squared norm of k and actual u/G/k in L2(volume.restrict K) for every compact K. For every C2 compact phi, both u Delta phi and k phi are integrable for volume and integral u Delta phi = integral k phi. This is a distribution identity, not a classical Laplacian of arbitrary u.

\[\mu=Z_W^{-1}e^{-W}dx,\quad G=\overline Du,\quad k=\varepsilon u+\langle\nabla W,G\rangle-f;\quad u,G,k\in L^2_{\rm loc}(dx),\quad\int u\Delta\phi\,dx=\int k\phi\,dx\ (\phi\in C_c^2).\]

Lean statement · weak_resolvent_laplacian

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 weak_resolvent_laplacian (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) →
      ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 μ,
      ∃ u : D.closure.domain,
        (∀ v : D.closure.domain,
          ε * ⟪(u : Lp ℝ 2 μ), (v : Lp ℝ 2 μ)⟫ +
            ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 μ)⟫) ∧
        LocallyIntegrable (fun x => (u : Lp ℝ 2 μ) x) ∧
        LocallyIntegrable (fun x => D.closure u x) ∧
        (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (D.closure u x) v) ∧
          Integrable (fun x => (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (D.closure u x) v) =
            - ∫ x, (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
        LocallyIntegrable (fun x => ‖ε * (u : Lp ℝ 2 μ) x +
          inner ℝ (gradient W x) (D.closure u x) - f x‖ ^ 2) ∧
        (∀ K : Set E, IsCompact K →
          MemLp (fun x => (u : Lp ℝ 2 μ) x) 2 (volume.restrict K) ∧
          MemLp (fun x => D.closure u x) 2 (volume.restrict K) ∧
          MemLp (fun x => ε * (u : Lp ℝ 2 μ) x +
            inner ℝ (gradient W x) (D.closure u x) - f x) 2 (volume.restrict K)) ∧
        ∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
          Integrable (fun x => (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) ∧
          Integrable (fun x => (ε * (u : Lp ℝ 2 μ) x +
            inner ℝ (gradient W x) (D.closure u x) - f x) * φ x) ∧
          (∫ x, (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) =
            ∫ x, (ε * (u : Lp ℝ 2 μ) x +
              inner ℝ (gradient W x) (D.closure u x) - f x) * φ x

Exact module and namespace context

Proof roadmap

1Retain the same genuine weak solution and ordinary weak gradient
Apply the canonical C1 resolvent to the actual normalized law and original closable graph. It supplies u in the same closure domain, its all-domain variational equation, ordinary locally integrable representatives, and every C1 compact directional weak-gradient identity. No Poisson/Poincare or final-PDE premise is inserted.
2Derive actual compact-volume L2 and the drift bound
The true weighted L2 classes u/G/f each transfer to volume L2 on every compact K by the existing local producer. Continuous grad W is bounded on K by a constant M_K. Its actual a.e. measurable drift product obeys abs(inner(grad W,G))≤M_K norm G on the restricted measure. MemLp domination and addition give actual k compact L2; the squared-norm criterion gives locally integrable norm(k)^2. M_K depends on K and is not a global drift bound.
3Use a legitimate inverseweight test and genuine product rule
For C2 compact phi, psi=exp(W)phi is still compact and C1 when W is only C1. Differentiate the actual product by Frechet/Riesz calculus. True exponential cancellation converts its weighted gradient term into phi inner(grad W,G)+inner(G,grad phi); multiplying by exp(W) does not remove compact support.
4Derive the weak Laplacian by finite-basis summation
For each orthonormal basis vector b_i, chi_i=Dphi[b_i] is C1 compact. Apply the genuine ordinary weak-gradient identity in direction b_i. The actual second Frechet derivative identifies Delta phi with sum_i Dchi_i[b_i], and Riesz/orthonormal expansion identifies inner(G,grad phi) with sum_i chi_i inner(G,b_i). Each term is integrable before exchanging the finite sum and integral. Empty basis sums cover dimension zero.
5Justify every ordinary integral before combining the equations
Local integrability of u/f and continuous-drift product, together with compact continuous phi, proves the individual ordinary u phi, drift phi and f phi products L1. The preceding finite-basis step proves the gradient and Laplace products L1. Use the actual weighted C1 equation at psi and cancel only the true pointwise exp(-W)exp(W)=1. Legal integral addition/subtraction yields integral k phi=-integral inner(G,grad phi).
6Conclude only the ordinary distribution equation and local-L2 edge
Combine the two justified identities for the same u/G/f, and retain all earlier variational and weak-gradient conclusions. No total Lean laplacian applied to an arbitrary L2 representative is substituted for weak regularity. Local H2, global generator core/Bochner and centered epsilon limits require further true analytic adapters.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with Borel measurable structure and canonical full-space volume, including dimension zero. W is C1 and exp(-W) is genuinely integrable for volume; mu is exactly volume.tilted(-W).
D is the same real-linear partial gradient on actual L2(mu), closable with original graph exactly compact smooth scalar representatives and their genuine gradients, identified mu-a.e. Epsilon is positive and forcing f is a genuine scalar L2(mu) class. Neither a weak solution, test-domain membership, ordinary PDE nor local-L2 certificate is supplied.
All ordinary weak derivatives, compact restrictions and distribution test integrals use volume; the variational identity uses actual L2(mu). The actual closed gradient G=D.closure u and the same u serve every test/compact. C2 compact tests suffice; no regularity of the selected L2 representative u is assumed.

Mathematical proof

1. Retain the same genuine weak solution and ordinary weak gradient

Apply the canonical C1 resolvent to the actual normalized law and original closable graph. It supplies u in the same closure domain, its all-domain variational equation, ordinary locally integrable representatives, and every C1 compact directional weak-gradient identity. No Poisson/Poincare or final-PDE premise is inserted.

\[\varepsilon\langle u,v\rangle_{L^2(\mu)}+\langle G,\overline Dv\rangle_{L^2(\mu)}=\langle f,v\rangle_{L^2(\mu)},\quad G=\overline Du.\]

Corresponding Lean step

WeightedResolventC1.weak_resolvent_c1

2. Derive actual compact-volume L2 and the drift bound

The true weighted L2 classes u/G/f each transfer to volume L2 on every compact K by the existing local producer. Continuous grad W is bounded on K by a constant M_K. Its actual a.e. measurable drift product obeys abs(inner(grad W,G))≤M_K norm G on the restricted measure. MemLp domination and addition give actual k compact L2; the squared-norm criterion gives locally integrable norm(k)^2. M_K depends on K and is not a global drift bound.

\[u,G,f\in L^2(K,dx),\quad|\langle\nabla W,G\rangle|\le M_K\|G\|,\quad k\in L^2(K,dx).\]

Corresponding Lean step

WeightedLocalL2.lp_locallyMemLp_volume; lp_inner_continuous_local_l2; MemLp.of_le_mul; memLp_two_iff_integrable_sq_norm

3. Use a legitimate inverseweight test and genuine product rule

For C2 compact phi, psi=exp(W)phi is still compact and C1 when W is only C1. Differentiate the actual product by Frechet/Riesz calculus. True exponential cancellation converts its weighted gradient term into phi inner(grad W,G)+inner(G,grad phi); multiplying by exp(W) does not remove compact support.

\[\psi=e^W\phi\in C_c^1,\quad e^{-W}\langle G,\nabla\psi\rangle=\phi\langle\nabla W,G\rangle+\langle G,\nabla\phi\rangle.\]

Corresponding Lean step

inverseweight_gradient; hW.exp.mul hphi; HasCompactSupport.mul_left

4. Derive the weak Laplacian by finite-basis summation

For each orthonormal basis vector b_i, chi_i=Dphi[b_i] is C1 compact. Apply the genuine ordinary weak-gradient identity in direction b_i. The actual second Frechet derivative identifies Delta phi with sum_i Dchi_i[b_i], and Riesz/orthonormal expansion identifies inner(G,grad phi) with sum_i chi_i inner(G,b_i). Each term is integrable before exchanging the finite sum and integral. Empty basis sums cover dimension zero.

\[\int u\Delta\phi\,dx=\sum_i\int uD\chi_i[b_i]dx=-\sum_i\int\chi_i\langle G,b_i\rangle dx=-\int\langle G,\nabla\phi\rangle dx.\]

Corresponding Lean step

ordinary_weak_laplacian; stdOrthonormalBasis; iteratedFDeriv_two_apply; integral_finsetSum

5. Justify every ordinary integral before combining the equations

Local integrability of u/f and continuous-drift product, together with compact continuous phi, proves the individual ordinary u phi, drift phi and f phi products L1. The preceding finite-basis step proves the gradient and Laplace products L1. Use the actual weighted C1 equation at psi and cancel only the true pointwise exp(-W)exp(W)=1. Legal integral addition/subtraction yields integral k phi=-integral inner(G,grad phi).

\[\varepsilon\int u\phi+\int\phi\langle\nabla W,G\rangle+\int\langle G,\nabla\phi\rangle=\int f\phi,\quad\int k\phi=-\int\langle G,\nabla\phi\rangle.\]

Corresponding Lean step

hweighted; locally_integrable_inner; integrable_smul_right_of_hasCompactSupport; integral_add; integral_sub

6. Conclude only the ordinary distribution equation and local-L2 edge

Combine the two justified identities for the same u/G/f, and retain all earlier variational and weak-gradient conclusions. No total Lean laplacian applied to an arbitrary L2 representative is substituted for weak regularity. Local H2, global generator core/Bochner and centered epsilon limits require further true analytic adapters.

\[\forall\phi\in C_c^2,\quad\int u\Delta\phi\,dx=\int k\phi\,dx;\quad H^2,\text{ core},\mathrm{BL}\text{ remain open}.\]

Corresponding Lean step

weak_resolvent_laplacian

Lean verification

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

Lean proof · weak_resolvent_laplacian

Retain the same genuine weak solution and ordinary weak gradient; Derive actual compact-volume L2 and the drift bound; Use a legitimate inverseweight test and genuine product rule; Derive the weak Laplacian by finite-basis summation; Justify every ordinary integral before combining the equations; Conclude only the ordinary distribution equation and local-L2 edge

Download module (.lean)

theorem weak_resolvent_laplacian (W : E → ℝ) (hW : ContDiff ℝ 1 W)
    (hI : Integrable (fun x => Real.exp (-W x))) :
    let μ := (volume : Measure E).tilted (fun x => -W x)
    ∀ (D : Lp ℝ 2 μ →ₗ.[ℝ] Lp E 2 μ), D.IsClosable →
      (∀ (a : Lp ℝ 2 μ) (H : Lp E 2 μ), (a,H) ∈ D.graph ↔
        ∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
          a =ᵐ[μ] φ ∧ H =ᵐ[μ] gradient φ) →
      ∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 μ,
      ∃ u : D.closure.domain,
        (∀ v : D.closure.domain,
          ε * ⟪(u : Lp ℝ 2 μ), (v : Lp ℝ 2 μ)⟫ +
            ⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 μ)⟫) ∧
        LocallyIntegrable (fun x => (u : Lp ℝ 2 μ) x) ∧
        LocallyIntegrable (fun x => D.closure u x) ∧
        (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ v : E,
          Integrable (fun x => ψ x * inner ℝ (D.closure u x) v) ∧
          Integrable (fun x => (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
          (∫ x, ψ x * inner ℝ (D.closure u x) v) =
            - ∫ x, (u : Lp ℝ 2 μ) x * fderiv ℝ ψ x v) ∧
        LocallyIntegrable (fun x => ‖ε * (u : Lp ℝ 2 μ) x +
          inner ℝ (gradient W x) (D.closure u x) - f x‖ ^ 2) ∧
        (∀ K : Set E, IsCompact K →
          MemLp (fun x => (u : Lp ℝ 2 μ) x) 2 (volume.restrict K) ∧
          MemLp (fun x => D.closure u x) 2 (volume.restrict K) ∧
          MemLp (fun x => ε * (u : Lp ℝ 2 μ) x +
            inner ℝ (gradient W x) (D.closure u x) - f x) 2 (volume.restrict K)) ∧
        ∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
          Integrable (fun x => (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) ∧
          Integrable (fun x => (ε * (u : Lp ℝ 2 μ) x +
            inner ℝ (gradient W x) (D.closure u x) - f x) * φ x) ∧
          (∫ x, (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) =
            ∫ x, (ε * (u : Lp ℝ 2 μ) x +
              inner ℝ (gradient W x) (D.closure u x) - f x) * φ x := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  dsimp only
  intro D hD hgraph ε hε f
  obtain ⟨u,hu,huL,hGL,hderiv,hweighted⟩ :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventC1.weak_resolvent_c1 W hW hI D hD hgraph ε hε f
  have hgrad : Continuous (gradient W) :=
    (toDual ℝ E).symm.continuous.comp (hW.continuous_fderiv one_ne_zero)
  let r := fun x => ε * (u : Lp ℝ 2 μ) x + inner ℝ (gradient W x) (D.closure u x) - f x
  have hlocal (K : Set E) (hK : IsCompact K) :
      MemLp (fun x => (u : Lp ℝ 2 μ) x) 2 (volume.restrict K) ∧
      MemLp (fun x => D.closure u x) 2 (volume.restrict K) ∧
      MemLp r 2 (volume.restrict K) := by
    have hU := (AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2.lp_locallyMemLp_volume W hW.continuous hI (u : Lp ℝ 2 μ)).2 K hK
    have hG := (AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2.lp_locallyMemLp_volume W hW.continuous hI (D.closure u)).2 K hK
    have hF := (AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2.lp_locallyMemLp_volume W hW.continuous hI f).2 K hK
    have hB := lp_inner_continuous_local_l2 W hW.continuous hI (D.closure u) (gradient W) hgrad K hK
    refine ⟨hU,hG,?_⟩
    convert ((hU.const_smul ε).add hB).sub hF using 1
    funext x
    rfl
  have hr2 : LocallyIntegrable (fun x => ‖r x‖^2) := by
    rw [locallyIntegrable_iff]
    intro K hK
    have hr := (hlocal K hK).2.2
    exact (memLp_two_iff_integrable_sq_norm hr.aestronglyMeasurable).mp hr
  have hfL : LocallyIntegrable (fun x => f x) := by
    rw [locallyIntegrable_iff]
    intro K hK
    let : IsFiniteMeasure (volume.restrict K) := isFiniteMeasure_restrict.mpr hK.measure_lt_top.ne
    have hF := (AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2.lp_locallyMemLp_volume W hW.continuous hI f).2 K hK
    exact hF.integrable (by norm_num)
  have hBLoc : LocallyIntegrable (fun x => inner ℝ (gradient W x) (D.closure u x)) := by
    simpa only [real_inner_comm] using locally_integrable_inner _ _ hGL hgrad
  have hrLoc : LocallyIntegrable r := by
    convert ((huL.smul ε).add hBLoc).sub hfL using 1
    funext x
    rfl
  refine ⟨u,hu,huL,hGL,hderiv,hr2,hlocal,?_⟩
  intro φ hφ hc
  have hφ1 : ContDiff ℝ 1 φ := hφ.of_le (by norm_num)
  obtain ⟨hLapI,hGi,hLap⟩ := ordinary_weak_laplacian _ _ hderiv φ hφ hc
  have hRi : Integrable (fun x => r x * φ x) := by
    simpa only [smul_eq_mul] using hrLoc.integrable_smul_right_of_hasCompactSupport hφ1.continuous hc
  refine ⟨hLapI,hRi,?_⟩
  let ψ := fun x => Real.exp (W x) * φ x
  have hψ : ContDiff ℝ 1 ψ := hW.exp.mul hφ1
  have hψc : HasCompactSupport ψ := hc.mul_left
  have hw := (hweighted ψ hψ hψc).2.2.2
  have hcancel (x : E) : Real.exp (-W x) * Real.exp (W x) = 1 := by
    rw [← Real.exp_add]; simp
  have hfirst (a : E → ℝ) (x : E) : Real.exp (-W x) * (a x * ψ x) = a x * φ x := by
    dsimp [ψ]
    calc
      _ = (Real.exp (-W x) * Real.exp (W x)) * (a x * φ x) := by ring
      _ = _ := by rw [hcancel,one_mul]
  have hsecond (x : E) : Real.exp (-W x) * inner ℝ (D.closure u x) (gradient ψ x) =
      φ x * inner ℝ (gradient W x) (D.closure u x) + inner ℝ (D.closure u x) (gradient φ x) :=
    inverseweight_gradient W φ hW hφ1 x (D.closure u x)
  simp only [hfirst,hsecond] at hw
  have hUi : Integrable (fun x => (u : Lp ℝ 2 μ) x * φ x) := by
    simpa only [smul_eq_mul] using huL.integrable_smul_right_of_hasCompactSupport hφ1.continuous hc
  have hBi : Integrable (fun x => φ x * inner ℝ (gradient W x) (D.closure u x)) := by
    simpa only [smul_eq_mul] using hBLoc.integrable_smul_left_of_hasCompactSupport hφ1.continuous hc
  have hFi : Integrable (fun x => f x * φ x) := by
    simpa only [smul_eq_mul] using hfL.integrable_smul_right_of_hasCompactSupport hφ1.continuous hc
  rw [integral_add hBi hGi] at hw
  have he : (∫ x, r x * φ x) =
      ε * (∫ x, (u : Lp ℝ 2 μ) x * φ x) +
      (∫ x, φ x * inner ℝ (gradient W x) (D.closure u x)) - ∫ x, f x * φ x := by
    have hp : (fun x => r x * φ x) = (fun x =>
      ε * ((u : Lp ℝ 2 μ) x * φ x) + φ x * inner ℝ (gradient W x) (D.closure u x) - f x * φ x) := by
      funext x; dsimp [r]; ring
    have hsum : Integrable (fun x => ε * ((u : Lp ℝ 2 μ) x * φ x) + φ x * inner ℝ (gradient W x) (D.closure u x)) := by
      convert (hUi.const_mul ε).add hBi using 1 <;> rfl
    have hsumEq : (∫ x, ε * ((u : Lp ℝ 2 μ) x * φ x) + φ x * inner ℝ (gradient W x) (D.closure u x)) =
        ε * (∫ x, (u : Lp ℝ 2 μ) x * φ x) + ∫ x, φ x * inner ℝ (gradient W x) (D.closure u x) := by
      calc
        _ = (∫ x, ε * ((u : Lp ℝ 2 μ) x * φ x)) + ∫ x, φ x * inner ℝ (gradient W x) (D.closure u x) :=
          integral_add (hUi.const_mul ε) hBi
        _ = _ := by rw [integral_const_mul]
    rw [hp]
    calc
      _ = (∫ x, ε * ((u : Lp ℝ 2 μ) x * φ x) + φ x * inner ℝ (gradient W x) (D.closure u x)) - ∫ x, f x * φ x :=
        integral_sub hsum hFi
      _ = _ := by rw [hsumEq]
  change (∫ x, (u : Lp ℝ 2 μ) x * Laplacian.laplacian φ x) = ∫ x, r x * φ x
  rw [he]
  linarith [hLap,hw]

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.OrdinaryWeakResolvent

Exact module and namespace context

Scope and omitted-condition boundaries

Same actual D/u/G and forcing yield ordinary volume distribution Delta u=epsilon u+inner(gradient W,G)-f, all C2 compact tests with genuine L1 products, and genuine local L2 of u/G/right-hand side. Full existing variational and ordinary weak-gradient identities retained. Actual PBPS R/S/reflected law and fixed fiber D before epsilon/input. No local H2, global generator core/Bochner, Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1 or complete paper/main/composition. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

HasFDerivAt.exp
HasFDerivAt.mul
stdOrthonormalBasis
InnerProductSpace.laplacian_eq_iteratedFDeriv_stdOrthonormalBasis
iteratedFDeriv_two_apply
MemLp.of_le_mul
locallyIntegrable_iff
integral_finsetSum
integral_add
integral_sub

Mathematical sources

PBPS AppendixC.1 omitted analytic prerequisite — Same actual D/u/G and forcing yield ordinary volume distribution Delta u=epsilon u+inner(gradient W,G)-f, all C2 compact tests with genuine L1 products, and genuine local L2 of u/G/right-hand side. Full existing variational and ordinary weak-gradient identities retained. Actual PBPS R/S/reflected law and fixed fiber D before epsilon/input. No local H2, global generator core/Bochner, Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1 or complete paper/main/composition. TV never transfers unbounded expected 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.