ASTIS mathematical exposition

The closed-gradient resolvent is a genuine weak PDE solution

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolvent.weak_resolvent_distributional · theorem · Teaching coverage

Statement

There exists u in the domain of the same closed gradient such that ε⟨u,v⟩L²(μ)+⟨G,D.closure v⟩L²(μ)=⟨f,v⟩L²(μ) for every domain test v, with G=D.closure u. The representatives u and G are locally volume-integrable and satisfy the ordinary weak gradient identity against every C1 compact scalar test and constant direction, including both integrable test products. For every smooth compact ψ, each of e^(−W)uψ, e^(−W)⟨G,∇ψ⟩ and e^(−W)fψ is volume-integrable and satisfies the displayed equation. This is εe^(−W)u−div(e^(−W)G)=e^(−W)f in the distributional sense, not a classical second-order equation.

\[\varepsilon\!\int e^{-W}u\psi\,dx+\int e^{-W}\langle G,\nabla\psi\rangle\,dx=\int e^{-W}f\psi\,dx,\qquad G=\overline D u.\]

All objects and hypotheses

E is any finite-dimensional real inner-product space with a Borel measurable structure, including dimension zero. W:E→R is C1, exp(-W) is volume-integrable, and μ is its normalized exponential tilt.
D is a given closable partial real-linear operator from scalar L²(μ) to vector L²(μ). Its graph is exactly the pairs represented μ-almost everywhere by (φ,∇φ) for smooth compact φ; WeightedGradient constructs such an operator.
ε is positive and f is an arbitrary scalar L²(μ) forcing. The theorem constructs one u in this same D.closure.domain and uses G=D.closure u everywhere. No weak equation, differentiability of u, or higher regularity is assumed.
The ordinary gradient identity uses all C1 compact tests and constant directions. The resolvent PDE uses smooth compact scalar tests ψ, embedded in the original gradient graph. Coercions select L2 representatives; all asserted integrabilities specify μ or volume.

Mathematical proof

1. Construct the actual same-domain solution

The existing closed-graph resolvent theorem applies to D.closure, whose closedness follows from closability of D. For positive ε it supplies a domain element u and an equation against every element of that domain. This step constructs a solution; it does not postulate the weak equation. All later uses refer to this one witness.

\[\exists u\in\operatorname{Dom}(\overline D),\quad\varepsilon\langle u,v\rangle_\mu+\langle\overline D u,\overline D v\rangle_\mu=\langle f,v\rangle_\mu\quad(\forall v\in\operatorname{Dom}(\overline D)).\]

Corresponding Lean step

ClosedGraphResolvent.weak_resolvent D.closure hD.closure_isClosed ε hε f

2. Identify its ordinary weak gradient

Apply the previously compiled distributional-gradient theorem to (u,G), where G=D.closure u and the pair belongs to that exact closure graph. It yields local volume integrability and the directional weak identity, with both integrable products. It never differentiates u pointwise.

\[u,G\in L^1_{\mathrm{loc}}(dx),\qquad\int\chi\langle G,a\rangle\,dx=-\int uD_a\chi\,dx\quad(\chi\in C_c^1,\ a\in E).\]

Corresponding Lean step

WeightedGradientDistribution.closed_gradient_distributional; D.closure.mem_graph u

3. Embed a genuine smooth compact test

For ψ smooth and compactly supported, both ψ and ∇ψ are continuous and compactly supported, hence in L²(μ). Choose their Lp classes p and q. The exact original graph places (p,q) in D.graph and graph closure places it in D.closure.graph. Thus there is a domain test v whose scalar class is p and whose image is q. No inverse-weighted test is presumed smooth.

\[p=[\psi]_\mu,\quad q=[\nabla\psi]_\mu,\qquad(p,q)\in\operatorname{graph}(D)\subseteq\operatorname{graph}(\overline D).\]

Corresponding Lean step

hgCont,hgComp,hp,hg,hpq,hpqc; MemLp.toLp; LinearPMap.mem_graph_iff

4. Expand three integrable L2 pairings

Test the abstract equation at this v. The L2 inner-product integrability theorem proves each product integrable for μ. Almost-everywhere representative equalities replace p by ψ and q by ∇ψ, both in the integrability proofs and in the integral formula. The scalar inner product is ordinary real multiplication.

\[\varepsilon\int u\psi\,d\mu+\int\langle G,\nabla\psi\rangle\,d\mu=\int f\psi\,d\mu.\]

Corresponding Lean step

hu v; hpe,hge; L2.integrable_inner.congr; L2.inner_def, integral_congr_ae

5. Transfer all three products to volume

For this actual normalized Gibbs tilt, integrable_tilted_iff converts each of the three μ-integrability facts to volume-integrability after multiplication by e^(−W). In particular, the displayed PDE integrals are not assigned values by a totalized fallback for nonintegrable functions.

\[u\psi,\ \langle G,\nabla\psi\rangle,\ f\psi\in L^1(\mu)\Longrightarrow e^{-W}u\psi,\ e^{-W}\langle G,\nabla\psi\rangle,\ e^{-W}f\psi\in L^1(dx).\]

Corresponding Lean step

hwu,hwG,hwf via integrable_tilted_iff hI

6. Cancel only the positive normalization

Write μ=Z⁻¹e^(−W)dx. Its finite normalization Z is strictly positive. Rewrite the three tilted integrals and cancel the common nonzero factor Z⁻¹. The plus sign on the gradient pairing is precisely the distributional minus-divergence convention. No Hessian, Laplacian or operator-core conclusion is used.

\[Z=\int e^{-W}dx>0,\qquad\varepsilon e^{-W}u-\operatorname{div}(e^{-W}G)=e^{-W}f\quad\text{in distributions}.\]

Corresponding Lean step

ht, integral_tilted; mul_left_cancel₀ (inv_ne_zero (integral_exp_pos hI).ne'); ring

Lean statement · weak_resolvent_distributional

The exact quantifiers, same-operator domain and all integrabilities appear below.

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.

theorem weak_resolvent_distributional {E : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (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) ∧
        ∀ ψ : E → ℝ, ContDiff ℝ ∞ ψ → HasCompactSupport ψ →
          Integrable (fun x => Real.exp (-W x) * ((u : Lp ℝ 2 μ) x * ψ x)) ∧
          Integrable (fun x => Real.exp (-W x) * inner ℝ (D.closure u x) (gradient ψ x)) ∧
          Integrable (fun x => Real.exp (-W x) * (f x * ψ x)) ∧
          ε * (∫ x, Real.exp (-W x) * ((u : Lp ℝ 2 μ) x * ψ x)) +
            (∫ x, Real.exp (-W x) * inner ℝ (D.closure u x) (gradient ψ x)) =
            ∫ x, Real.exp (-W x) * (f x * ψ x)

Exact module and namespace context

Lean proof · weak_resolvent_distributional

Construct u once; identify its weak gradient; embed smooth compact tests; expand L2 pairings and cancel normalization.

theorem weak_resolvent_distributional {E : Type*}
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E]
    (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) ∧
        ∀ ψ : E → ℝ, ContDiff ℝ ∞ ψ → HasCompactSupport ψ →
          Integrable (fun x => Real.exp (-W x) * ((u : Lp ℝ 2 μ) x * ψ x)) ∧
          Integrable (fun x => Real.exp (-W x) * inner ℝ (D.closure u x) (gradient ψ x)) ∧
          Integrable (fun x => Real.exp (-W x) * (f x * ψ x)) ∧
          ε * (∫ x, Real.exp (-W x) * ((u : Lp ℝ 2 μ) x * ψ x)) +
            (∫ x, Real.exp (-W x) * inner ℝ (D.closure u x) (gradient ψ x)) =
            ∫ x, Real.exp (-W x) * (f x * ψ x) := by
  let μ := (volume : Measure E).tilted (fun x => -W x)
  dsimp only
  intro D hD hgraph ε hε f
  let : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hI
  obtain ⟨u,hu,_⟩ := ClosedGraphResolvent.weak_resolvent D.closure hD.closure_isClosed ε hε f
  obtain ⟨huL,hGL,hderiv⟩ := WeightedGradientDistribution.closed_gradient_distributional
    W hW hI D hD hgraph u (D.closure u) (D.closure.mem_graph u)
  refine ⟨u,hu,huL,hGL,hderiv,?_⟩
  intro ψ hψ hc
  have hgCont : Continuous (gradient ψ) :=
    (toDual ℝ E).symm.continuous.comp
      (((contDiff_infty.mp hψ 1).fderiv_right (m := 0) (by norm_num)).continuous)
  have hgComp : HasCompactSupport (gradient ψ) := by
    refine HasCompactSupport.of_support_subset_isCompact hc.isCompact ?_
    intro x hx
    by_contra hn
    exact hx (by simp [gradient, fderiv_of_notMem_tsupport ℝ hn])
  have hp : MemLp ψ 2 μ := hψ.continuous.memLp_of_hasCompactSupport hc
  have hg : MemLp (gradient ψ) 2 μ := hgCont.memLp_of_hasCompactSupport hgComp
  let p : Lp ℝ 2 μ := hp.toLp ψ
  let q : Lp E 2 μ := hg.toLp (gradient ψ)
  have hpq : (p,q) ∈ D.graph :=
    (hgraph p q).mpr ⟨ψ,hψ,hc,hp.coeFn_toLp,hg.coeFn_toLp⟩
  have hpqc : (p,q) ∈ D.closure.graph := by
    rw [← hD.graph_closure_eq_closure_graph]
    exact D.graph.le_topologicalClosure hpq
  obtain ⟨v,hv,hDv⟩ := D.closure.mem_graph_iff.mp hpqc
  have he := hu v
  rw [hv,hDv] at he
  have hpe (a : Lp ℝ 2 μ) :
      (fun x => inner ℝ (a x) (p x)) =ᵐ[μ] (fun x => a x * ψ x) := by
    filter_upwards [hp.coeFn_toLp] with x hx
    rw [show p x = ψ x from hx]
    simp [mul_comm]
  have hge :
      (fun x => inner ℝ (D.closure u x) (q x)) =ᵐ[μ]
        (fun x => inner ℝ (D.closure u x) (gradient ψ x)) := by
    filter_upwards [hg.coeFn_toLp] with x hx
    rw [show q x = gradient ψ x from hx]
  have hiu := (L2.integrable_inner (𝕜 := ℝ) (u : Lp ℝ 2 μ) p).congr (hpe u)
  have hiG := (L2.integrable_inner (𝕜 := ℝ) (D.closure u) q).congr hge
  have hif := (L2.integrable_inner (𝕜 := ℝ) f p).congr (hpe f)
  have hwu := (integrable_tilted_iff hI _).mp hiu
  have hwG := (integrable_tilted_iff hI _).mp hiG
  have hwf := (integrable_tilted_iff hI _).mp hif
  simp only [smul_eq_mul] at hwu hwG hwf
  refine ⟨hwu,hwG,hwf,?_⟩
  rw [L2.inner_def, L2.inner_def, L2.inner_def,
    integral_congr_ae (hpe u), integral_congr_ae hge,
    integral_congr_ae (hpe f)] at he
  have ht (g : E → ℝ) : (∫ x, g x ∂μ) =
      (∫ x, Real.exp (-W x))⁻¹ * ∫ x, Real.exp (-W x) * g x := by
    rw [show μ = (volume : Measure E).tilted (fun x => -W x) from rfl, integral_tilted]
    rw [← integral_const_mul]
    apply integral_congr_ae
    filter_upwards [] with x
    change (Real.exp (-W x) / (∫ z, Real.exp (-W z))) • g x = _
    simp only [smul_eq_mul, div_eq_mul_inv]
    ring
  rw [ht,ht,ht] at he
  apply mul_left_cancel₀ (inv_ne_zero (integral_exp_pos hI).ne')
  convert he using 1
  ring

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolvent

Exact module and namespace context

Scope and omitted-condition boundaries

Weighted distributional PDE existence only. No H2, converse domain characterization, D*D operator core, Poincare, measurable fiberwise solution selection, or complete paper. Separately chosen resolvent witnesses are not definitionally identified.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

LinearPMap.IsClosable.closure_isClosed
LinearPMap.IsClosable.graph_closure_eq_closure_graph
LinearPMap.mem_graph_iff
MeasureTheory.MemLp.coeFn_toLp
MeasureTheory.L2.integrable_inner
MeasureTheory.L2.inner_def
MeasureTheory.integrable_tilted_iff
MeasureTheory.integral_tilted

Mathematical sources

PBPS Appendix C.1: analytic prerequisite — Weighted distributional PDE existence only. No H2, converse domain characterization, D*D operator core, Poincare, measurable fiberwise solution selection, or complete paper. Separately chosen resolvent witnesses are not definitionally identified.
Kolesnikov–Milman §§2.4–2.5: weighted Poisson/Sobolev background — Direct Euclidean weak equation only; no automatic compact-manifold regularity transfer.

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