Actual compact localization of the same weighted weak resolvent

Samplinglib explicit same-solution compact localization prerequisite to Chen, Chewi, Lu and Zhang AppendixC.1; not a quoted numbered theorem or complete LemmaC.1/Poincare result.

Complete source statement (Samplinglib restatement)

For the exact normalized Gibbs mu, original closable D fixed before epsilon/forcing, construct the actual resolvent u in D.closure.domain. Retain the actual all-domain variational equation, ordinary locally integrable u/G, all C1 compact directional weak-gradient tests, squared local integrability of r=epsilon*u+inner(grad W,G)-f, compact-volume L2 of u/G/r and every C2 original distribution test. For every C2 compact chi define v=chi*u, Gchi=chi*G+u*grad chi, Fchi=chi*r+2 inner(grad chi,G)+u Delta chi. Prove genuine global-volume L2 of v/Gchi/Fchi and each topological support contained in tsupport chi. For every C1 compact psi/direction a both weak-gradient products are L1 with integral psi inner(Gchi,a)=-integral v Dpsi[a]. For every C2 compact phi both PDE products are L1 with integral v Delta phi=integral Fchi phi. The same u is chosen before all cutoffs; only smooth test/cutoff functions have classical derivatives.

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 localization of the same weighted weak resolvent

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.LocalizedWeakResolvent.localized_weak_resolvent · theorem · Teaching coverage

Read this first

Mathematical statement

\[G=\overline Du,\ r=\varepsilon u+\langle\nabla W,G\rangle-f;\quad v=\chi u,\ G_\chi=\chi G+u\nabla\chi,\ F_\chi=\chi r+2\langle\nabla\chi,G\rangle+u\Delta\chi;\quad v,G_\chi,F_\chi\in L^2(dx),\quad\nabla v=G_\chi,\ \Delta v=F_\chi\quad\text{weakly}.\]

Lean statement · localized_weak_resolvent

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 localized_weak_resolvent (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) ∧
        ∀ χ : E → ℝ, ContDiff ℝ 2 χ → HasCompactSupport χ →
    let v := fun x => χ x * (u : Lp ℝ 2 μ) x
    let Gχ := fun x => χ x • D.closure u x + (u : Lp ℝ 2 μ) x • gradient χ x
    let Fχ := fun x => χ x * (ε * (u : Lp ℝ 2 μ) x + inner ℝ (gradient W x) (D.closure u x) - f x) + 2 * inner ℝ (gradient χ x) (D.closure u x) +
      (u : Lp ℝ 2 μ) x * Laplacian.laplacian χ x
    MemLp v 2 volume ∧ MemLp Gχ 2 volume ∧ MemLp Fχ 2 volume ∧
    tsupport v ⊆ tsupport χ ∧ tsupport Gχ ⊆ tsupport χ ∧ tsupport Fχ ⊆ tsupport χ ∧
    (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => ψ x * inner ℝ (Gχ x) a) ∧
      Integrable (fun x => v x * fderiv ℝ ψ x a) ∧
      (∫ x, ψ x * inner ℝ (Gχ x) a) = -∫ x, v x * fderiv ℝ ψ x a) ∧
    ∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
      Integrable (fun x => v x * Laplacian.laplacian φ x) ∧
      Integrable (fun x => Fχ x * φ x) ∧
      (∫ x, v x * Laplacian.laplacian φ x) = ∫ x, Fχ x * φ x

Exact module and namespace context

Proof roadmap

1Choose the same real solution before every cutoff
Use the canonical ordinary resolvent producer for the exact Gibbs law and original D. Retain its all-domain variational identity, ordinary gradient/PDE and actual compact-volume L2 of u/G/r. Choose this u once, before quantifying over chi; no cutoff-specific replacement solution or supplied final localized equation is introduced.
2Derive derivative support and global L2
The actual Frechet derivative support is contained in tsupport chi; its second derivative and finite-basis Laplacian vanish outside that set too. C2 makes grad chi and Delta chi continuous. Bound their norms only on K=tsupport chi. Actual restricted a.e. measurability and MemLp domination yield the localized scalar/vector/drift L2 on K, then the proven indicator equality and memLp_indicator_iff_restrict give global-volume L2. All three topological supports lie in K. This step does not infer global L1 from global L2.
3Prove the first weak product rule with legal terms
Test the original ordinary weak gradient at chi*psi. Actual Frechet multiplication gives D(chi psi)=chi Dpsi+psi Dchi. Each separate product is L1, using the parent compact-test integrability and the continuous compact multiplier in L infinity. Riesz identifies Dchi[a]=inner(grad chi,a). After legal integral addition, cancel the u psi Dchi term to obtain the localized gradient identity.
4Compute the actual second test product and cross identity
Differentiate the first product again; true C2 second derivatives and finite orthonormal-basis trace give Delta(chi phi)=chi Delta phi+2 inner(grad chi,grad phi)+phi Delta chi. For each b_i test the original weak gradient at phi Dchi[b_i], genuinely C1 compact. Every summand and individual split is L1 using local integrability and continuous compact coefficients before finite sum/integral exchange. Empty sums retain dimension zero.
5Derive the localized PDE with the exact coefficient2
Use the original PDE at chi*phi and the preceding product formula. Prove L1 of chi*u*Delta phi, chi*r*phi, the cross term and u*phi*Delta chi individually. Borel normalization merely identifies the given Borel measurable structure with the canonical one; function algebra is normalized without changing the measure. Legal integral splitting and the cross identity yield the positive coefficient2 and positive u Delta chi term in Fchi, with both final tested products integrable.
6Retain only the proven compact-localization boundary
Return the same parent witnesses and all original identities, together with every cutoff result. The ordinary gradient of v is not asserted to equal D.closure applied to v: no membership of v in that weighted closure-domain is proved here. The compact-to-Schwartz/tempered adapter, local H2, global weighted core/Bochner and functional inequalities still need their own producers.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real Hilbert space with Borel measurable structure and canonical full-space volume, including dimension zero. W is C1, exp(-W) is integrable, and mu is exactly volume.tilted(-W).
D is the original closable partial gradient on L2(mu), with graph exactly compact smooth scalar representatives and their genuine gradients modulo mu-a.e. D is fixed before epsilon>0 and forcing f in L2(mu). The genuine solution u/G/r and all local volume facts are derived, not supplied.
For every C2 real cutoff chi with compact topological support, the same u chosen before all chi yields explicit v=chi*u, Gchi=chi*G+u*grad chi and Fchi=chi*r+2 inner(grad chi,G)+u Delta chi. Neither sign, normalized mass, compact derivative bounds nor localized PDE/H2 certificate is assumed. All localized L2 and test integrals use volume; variational identities use L2(mu).

Mathematical proof

1. Choose the same real solution before every cutoff

Use the canonical ordinary resolvent producer for the exact Gibbs law and original D. Retain its all-domain variational identity, ordinary gradient/PDE and actual compact-volume L2 of u/G/r. Choose this u once, before quantifying over chi; no cutoff-specific replacement solution or supplied final localized equation is introduced.

\[\exists u\in\operatorname{dom}\overline D\ \forall\chi\in C_c^2,\quad G=\overline Du,\quad r=\varepsilon u+\langle\nabla W,G\rangle-f.\]

Corresponding Lean step

OrdinaryWeakResolvent.weak_resolvent_laplacian; localized_weak_resolvent

2. Derive derivative support and global L2

The actual Frechet derivative support is contained in tsupport chi; its second derivative and finite-basis Laplacian vanish outside that set too. C2 makes grad chi and Delta chi continuous. Bound their norms only on K=tsupport chi. Actual restricted a.e. measurability and MemLp domination yield the localized scalar/vector/drift L2 on K, then the proven indicator equality and memLp_indicator_iff_restrict give global-volume L2. All three topological supports lie in K. This step does not infer global L1 from global L2.

\[\operatorname{tsupp}(v),\operatorname{tsupp}(G_\chi),\operatorname{tsupp}(F_\chi)\subseteq K;\quad v,G_\chi,F_\chi\in L^2(dx).\]

Corresponding Lean step

compact_smul_memLp; compact_smul_right_memLp; compact_inner_memLp; cutoff_rhs_memLp; cutoff_supports

3. Prove the first weak product rule with legal terms

Test the original ordinary weak gradient at chi*psi. Actual Frechet multiplication gives D(chi psi)=chi Dpsi+psi Dchi. Each separate product is L1, using the parent compact-test integrability and the continuous compact multiplier in L infinity. Riesz identifies Dchi[a]=inner(grad chi,a). After legal integral addition, cancel the u psi Dchi term to obtain the localized gradient identity.

\[\int\psi\langle G_\chi,a\rangle=-\int\chi uD\psi[a],\quad G_\chi=\chi G+u\nabla\chi.\]

Corresponding Lean step

first_product; cutoff_weak_gradient; Integrable.mul_of_top_right; integral_add

4. Compute the actual second test product and cross identity

Differentiate the first product again; true C2 second derivatives and finite orthonormal-basis trace give Delta(chi phi)=chi Delta phi+2 inner(grad chi,grad phi)+phi Delta chi. For each b_i test the original weak gradient at phi Dchi[b_i], genuinely C1 compact. Every summand and individual split is L1 using local integrability and continuous compact coefficients before finite sum/integral exchange. Empty sums retain dimension zero.

\[\int\phi\langle\nabla\chi,G\rangle=-\int u\langle\nabla\chi,\nabla\phi\rangle-\int u\phi\Delta\chi.\]

Corresponding Lean step

directional_second; second_product; laplacian_trace; laplacian_product; cutoff_cross_identity; integral_finsetSum

5. Derive the localized PDE with the exact coefficient2

Use the original PDE at chi*phi and the preceding product formula. Prove L1 of chi*u*Delta phi, chi*r*phi, the cross term and u*phi*Delta chi individually. Borel normalization merely identifies the given Borel measurable structure with the canonical one; function algebra is normalized without changing the measure. Legal integral splitting and the cross identity yield the positive coefficient2 and positive u Delta chi term in Fchi, with both final tested products integrable.

\[\int v\Delta\phi=\int(\chi r+2\langle\nabla\chi,G\rangle+u\Delta\chi)\phi,\quad\phi\in C_c^2.\]

Corresponding Lean step

cutoff_weak_pde; localize_weak_poisson; integral_add; integral_const_mul

6. Retain only the proven compact-localization boundary

Return the same parent witnesses and all original identities, together with every cutoff result. The ordinary gradient of v is not asserted to equal D.closure applied to v: no membership of v in that weighted closure-domain is proved here. The compact-to-Schwartz/tempered adapter, local H2, global weighted core/Bochner and functional inequalities still need their own producers.

\[\text{compact localization/global }L^2\quad\ne\quad H^2,\text{ weighted core or BL}.\]

Corresponding Lean step

localized_weak_resolvent

Lean verification

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

Lean proof · localized_weak_resolvent

Choose the same real solution before every cutoff; Derive derivative support and global L2; Prove the first weak product rule with legal terms; Compute the actual second test product and cross identity; Derive the localized PDE with the exact coefficient2; Retain only the proven compact-localization boundary

Download module (.lean)

theorem localized_weak_resolvent (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) ∧
        ∀ χ : E → ℝ, ContDiff ℝ 2 χ → HasCompactSupport χ →
    let v := fun x => χ x * (u : Lp ℝ 2 μ) x
    let Gχ := fun x => χ x • D.closure u x + (u : Lp ℝ 2 μ) x • gradient χ x
    let Fχ := fun x => χ x * (ε * (u : Lp ℝ 2 μ) x + inner ℝ (gradient W x) (D.closure u x) - f x) + 2 * inner ℝ (gradient χ x) (D.closure u x) +
      (u : Lp ℝ 2 μ) x * Laplacian.laplacian χ x
    MemLp v 2 volume ∧ MemLp Gχ 2 volume ∧ MemLp Fχ 2 volume ∧
    tsupport v ⊆ tsupport χ ∧ tsupport Gχ ⊆ tsupport χ ∧ tsupport Fχ ⊆ tsupport χ ∧
    (∀ ψ : E → ℝ, ContDiff ℝ 1 ψ → HasCompactSupport ψ → ∀ a : E,
      Integrable (fun x => ψ x * inner ℝ (Gχ x) a) ∧
      Integrable (fun x => v x * fderiv ℝ ψ x a) ∧
      (∫ x, ψ x * inner ℝ (Gχ x) a) = -∫ x, v x * fderiv ℝ ψ x a) ∧
    ∀ φ : E → ℝ, ContDiff ℝ 2 φ → HasCompactSupport φ →
      Integrable (fun x => v x * Laplacian.laplacian φ x) ∧
      Integrable (fun x => Fχ x * φ x) ∧
      (∫ x, v x * Laplacian.laplacian φ x) = ∫ 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,hd,hr2,hl,hp⟩ :=
    AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.OrdinaryWeakResolvent.weak_resolvent_laplacian W hW hI D hD hgraph ε hε f
  refine ⟨u,hu,huL,hGL,hd,hr2,hl,hp,?_⟩
  intro χ hχ hc
  exact localize_weak_poisson (fun x => (u : Lp ℝ 2 μ) x)
    (fun x => ε * (u : Lp ℝ 2 μ) x + inner ℝ (gradient W x) (D.closure u x) - f x)
    (fun x => D.closure u x) huL hl hd hp χ hχ hc

end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.LocalizedWeakResolvent

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source Euclidean C2 positive-curvature Gibbs conditional route.	E is a finite-dimensional real Hilbert space with Borel measurable structure and canonical full-space volume, including dimension zero. W is C1, exp(-W) is integrable, and mu is exactly volume.tilted(-W). D is the original closable partial gradient on L2(mu), with graph exactly compact smooth scalar representatives and their genuine gradients modulo mu-a.e. D is fixed before epsilon>0 and forcing f in L2(mu). The genuine solution u/G/r and all local volume facts are derived, not supplied. For every C2 real cutoff chi with compact topological support, the same u chosen before all chi yields explicit v=chiu, Gchi=chiG+ugrad chi and Fchi=chir+2 inner(grad chi,G)+u Delta chi. Neither sign, normalized mass, compact derivative bounds nor localized PDE/H2 certificate is assumed. All localized L2 and test integrals use volume; variational identities use L2(mu).	generalization	Shared C1 W, C2 compact cutoffs/tests, finite Hilbert/Borel/zero dimension disclosed; actual source V C2/alpha beta/eta cap/reflected density unchanged.
AppendixC.1 compact-to-H1 analytic details omitted; compact localization not a quoted numbered theorem.	For the exact normalized Gibbs mu, original closable D fixed before epsilon/forcing, construct the actual resolvent u in D.closure.domain. Retain the actual all-domain variational equation, ordinary locally integrable u/G, all C1 compact directional weak-gradient tests, squared local integrability of r=epsilonu+inner(grad W,G)-f, compact-volume L2 of u/G/r and every C2 original distribution test. For every C2 compact chi define v=chiu, Gchi=chiG+ugrad chi, Fchi=chi*r+2 inner(grad chi,G)+u Delta chi. Prove genuine global-volume L2 of v/Gchi/Fchi and each topological support contained in tsupport chi. For every C1 compact psi/direction a both weak-gradient products are L1 with integral psi inner(Gchi,a)=-integral v Dpsi[a]. For every C2 compact phi both PDE products are L1 with integral v Delta phi=integral Fchi phi. The same u is chosen before all cutoffs; only smooth test/cutoff functions have classical derivatives.	source-implicit	Actually derive supports/global volume L2 and weak first/second cutoff products with exact cross coefficient2; no supplied localized PDE, weighted-domain membership or H2/core certificate.
Source conditional Poincare/macroscopic H1 extension; SPHMC4.1 BL bound.	Same actual original D/u/G/r, one u before all C2 compact chi: derive actual compact support/global volume L2 of chiu, chiG+ugradchi, chir+2<gradchi,G>+u*Delta chi, all C1 compact weak-gradient and C2 compact distribution PDE with every L1 term legal. No localized weighted closure-domain membership, H2, Schwartz/tempered adapter, global core/Bochner, BL/Poincare, epsilon0, noncompact domain, measurable y-selector or either main/composition. Reflected/RGO law/scale remain distinct; TV never transfers unbounded expected cost.	unresolved	This is only the actual compact-localization/global-L2 weak-PDE edge. Reflected/RGO operator adapter, H2/core/Bochner, BL/Poincare/full papers remain independent.

Same actual original D/u/G/r, one u before all C2 compact chi: derive actual compact support/global volume L2 of chi*u, chi*G+u*gradchi, chi*r+2<gradchi,G>+u*Delta chi, all C1 compact weak-gradient and C2 compact distribution PDE with every L1 term legal. No localized weighted closure-domain membership, H2, Schwartz/tempered adapter, global core/Bochner, BL/Poincare, epsilon0, noncompact domain, measurable y-selector or either main/composition. Reflected/RGO law/scale remain distinct; TV never transfers unbounded expected cost.

Encoder–denoiser: accepted · equivalent-after-elaboration

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

Same actual original D/u/G/r, one u before all C2 compact chi: derive actual compact support/global volume L2 of chi*u, chi*G+u*gradchi, chi*r+2<gradchi,G>+u*Delta chi, all C1 compact weak-gradient and C2 compact distribution PDE with every L1 term legal. No localized weighted closure-domain membership, H2, Schwartz/tempered adapter, global core/Bochner, BL/Poincare, epsilon0, noncompact domain, measurable y-selector or either main/composition. Reflected/RGO law/scale remain distinct; TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.OrdinaryWeakResolvent.weak_resolvent_laplacian

Mathlib API called (external library)

MemLp.of_le_mul
memLp_indicator_iff_restrict
tsupport_fderiv_subset
HasCompactSupport.fderiv_apply
HasFDerivAt.mul
stdOrthonormalBasis
iteratedFDeriv_two_apply
LocallyIntegrable.integrable_smul_right_of_hasCompactSupport
integral_finsetSum
integral_add
integral_const_mul

Mathematical sources

PBPS AppendixC.1 omitted analytic prerequisite — Same actual original D/u/G/r, one u before all C2 compact chi: derive actual compact support/global volume L2 of chi*u, chi*G+u*gradchi, chi*r+2<gradchi,G>+u*Delta chi, all C1 compact weak-gradient and C2 compact distribution PDE with every L1 term legal. No localized weighted closure-domain membership, H2, Schwartz/tempered adapter, global core/Bochner, BL/Poincare, epsilon0, noncompact domain, measurable y-selector or either main/composition. Reflected/RGO law/scale remain distinct; 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.

Actual compact localization of the same weighted weak resolvent

Complete source statement (Samplinglib restatement)

Actual compact localization of the same weighted weak resolvent

Read the formalized proofs

Actual compact localization of the same weighted weak resolvent

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Choose the same real solution before every cutoff

2. Derive derivative support and global L2

3. Prove the first weak product rule with legal terms

4. Compute the actual second test product and cross identity

5. Derive the localized PDE with the exact coefficient2

6. Retain only the proven compact-localization boundary

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?