AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventC1

Samplinglib mathematical lesson

The actual weak resolvent admits C1 compact weighted tests

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventC1.weak_resolvent_c1 · theorem · Teaching coverage

Read this first

Mathematical statement

For C1 W and genuine integrability of exp(-W) volume, let mu=volume.tilted(-W). For every same closable exact compact smooth gradient D, epsilon>0 and scalar L2(mu) input f, construct u in D.closure.domain satisfying the variational equation for every domain test. Its actual closed gradient is the ordinary weak gradient, with locally volume-integrable representatives and full C1 compact directional identities. For every C1 compact psi, all three weighted volume products are integrable and epsilon integral exp(-W)u psi + integral exp(-W)<D.closure u,gradient psi> = integral exp(-W)f psi.

\[\varepsilon\int e^{-W}u\psi\,dx+\int e^{-W}\langle\overline Du,\nabla\psi\rangle\,dx=\int e^{-W}f\psi\,dx\quad(\psi\in C_c^1(E)).\]

Lean statement · weak_resolvent_c1

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_c1 {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 ℝ 1 ψ → 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

Proof roadmap

1Construct the same genuine variational solution
Positive epsilon and the actual closed partial operator give the true weak solution on D.closure.domain. The same D precedes epsilon and input; no Poisson solvability or Poincare premise is inserted.
2Retain the ordinary weak gradient and representatives
The existing exact graph/distributional producer gives local volume integrability and every C1 compact directional weak-gradient identity for the very same u and D.closure u.
3Embed each actual C1 compact test in this domain
Use the newly proved joint domain producer, yielding true MemLp classes p=[psi],q=[gradient psi] and their pair in this same closure graph. Extract the domain element v with D.closure v=q.
4Derive integrability before integral algebra
Actual L2 inner integrability gives the three mu-products. The proved tilted-law integrability equivalence transfers them to exp(-W)-weighted volume. No integral of an unproved nonintegrable expression is rearranged.
5Remove only the true positive normalization
Rewrite the actual L2 inner products with their mu-a.e. representatives and true tilted integrals. Cancel the reciprocal of the genuine positive partition to obtain the weighted volume equation for every C1 compact psi.
6Permit legitimate inverseweight tests without higher-regularity claims
For smooth compact phi, exp(W)phi is still compact and C1 when W is C1, so the new class is the needed legitimate input. This theorem does not itself establish the ordinary Laplacian, local H2, global Bochner or BL.

Full assumptions and notation

All objects and hypotheses

E has the same finite-dimensional real Hilbert/Borel/full-space structure, including dimension zero. W is C1 and exp(-W) is genuinely integrable for volume. The law mu is exactly volume.tilted(-W), whose probability normalization is derived.
D is the same closable partial gradient with exact compact smooth representative graph. epsilon is positive and forcing f is a genuine scalar L2(mu) class. No weak solution, H1 membership of a test, differentiability of u, coercivity or Poincare certificate is supplied.
All quantifiers/representatives/measures are retained: the weak equation tests every original closure-domain element; ordinary weak derivatives use volume and every C1 compact scalar test/direction; the weighted equation now uses every C1 compact scalar test, with all three products L1 for volume.

Mathematical proof

1. Construct the same genuine variational solution

Positive epsilon and the actual closed partial operator give the true weak solution on D.closure.domain. The same D precedes epsilon and input; no Poisson solvability or Poincare premise is inserted.

\[\varepsilon\langle u,v\rangle_2+\langle\overline Du,\overline Dv\rangle_2=\langle f,v\rangle_2.\]

Corresponding Lean step

ClosedGraphResolvent.weak_resolvent

2. Retain the ordinary weak gradient and representatives

The existing exact graph/distributional producer gives local volume integrability and every C1 compact directional weak-gradient identity for the very same u and D.closure u.

\[\int\chi\langle\overline Du,a\rangle dx=-\int uD\chi[a]dx.\]

Corresponding Lean step

WeightedGradientDistribution.closed_gradient_distributional

3. Embed each actual C1 compact test in this domain

Use the newly proved joint domain producer, yielding true MemLp classes p=[psi],q=[gradient psi] and their pair in this same closure graph. Extract the domain element v with D.closure v=q.

\[(p,q)=([\psi],[\nabla\psi])\in\operatorname{graph}\overline D.\]

Corresponding Lean step

CompactC1GradientDomain.compact_c1_in_closed_gradient; mem_graph_iff

4. Derive integrability before integral algebra

Actual L2 inner integrability gives the three mu-products. The proved tilted-law integrability equivalence transfers them to exp(-W)-weighted volume. No integral of an unproved nonintegrable expression is rearranged.

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

Corresponding Lean step

L2.integrable_inner; integrable_tilted_iff

5. Remove only the true positive normalization

Rewrite the actual L2 inner products with their mu-a.e. representatives and true tilted integrals. Cancel the reciprocal of the genuine positive partition to obtain the weighted volume equation for every C1 compact psi.

\[\varepsilon\int e^{-W}u\psi+\int e^{-W}\langle\overline Du,\nabla\psi\rangle=\int e^{-W}f\psi.\]

Corresponding Lean step

L2.inner_def; integral_tilted; integral_exp_pos

6. Permit legitimate inverseweight tests without higher-regularity claims

For smooth compact phi, exp(W)phi is still compact and C1 when W is C1, so the new class is the needed legitimate input. This theorem does not itself establish the ordinary Laplacian, local H2, global Bochner or BL.

\[e^W\phi\in C_c^1;\quad\text{higher operator-domain conclusions remain separate}.\]

Corresponding Lean step

weak_resolvent_c1

Lean verification

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

Lean proof · weak_resolvent_c1

Construct the same genuine variational solution; Retain the ordinary weak gradient and representatives; Embed each actual C1 compact test in this domain; Derive integrability before integral algebra; Remove only the true positive normalization; Permit legitimate inverseweight tests without higher-regularity claims

Download module (.lean)

theorem weak_resolvent_c1 {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 ℝ 1 ψ → 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,_⟩ := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent.weak_resolvent D.closure hD.closure_isClosed ε hε f
  obtain ⟨huL,hGL,hderiv⟩ := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.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
  obtain ⟨hp,hg,hpqc⟩ := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactC1GradientDomain.compact_c1_in_closed_gradient μ D hD hgraph hψ hc
  let p : Lp ℝ 2 μ := hp.toLp ψ
  let q : Lp E 2 μ := hg.toLp (gradient ψ)
  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
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventC1

Exact module and namespace context

Scope and omitted-condition boundaries

Same actual compact-gradient graph closure admits C1 compact function/gradient pairs; actual positive-epsilon weak resolvent has all C1 compact weighted volume tests and genuine ordinary weak gradient. Actual PBPS reflected conditional R/S law and original fixed D precede epsilon/input. No local H2, global operator-core/Bochner, conditional Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1, PBPS hypocoercivity or either complete main/composition. TV never transfers unbounded expected cost.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

L2.integrable_inner
integrable_tilted_iff
integral_tilted
integral_exp_pos
LinearPMap.mem_graph_iff

Mathematical sources

PBPS Appendix C.1 omitted analytic domain prerequisite — Same actual compact-gradient graph closure admits C1 compact function/gradient pairs; actual positive-epsilon weak resolvent has all C1 compact weighted volume tests and genuine ordinary weak gradient. Actual PBPS reflected conditional R/S law and original fixed D precede epsilon/input. No local H2, global operator-core/Bochner, conditional Poincare/BL, centered epsilon limit, noncompact constant/linear domains, measurable y-selection, SPHMC Hessian lower/full4.1, PBPS hypocoercivity or either complete 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.

WeightedResolventC1: mathematical reading route

The actual weak resolvent admits C1 compact weighted tests

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Construct the same genuine variational solution

2. Retain the ordinary weak gradient and representatives

3. Embed each actual C1 compact test in this domain

4. Derive integrability before integral algebra

5. Remove only the true positive normalization

6. Permit legitimate inverseweight tests without higher-regularity claims

Lean verification

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources