Solve the weak equation on the actual conditional gradient closure
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent.conditional_weak_resolvent · theorem · Teaching coverage
Mathematical statement
For the actual Gibbs-Gaussian augmentation, retain common Markov kernels R,S with swapped-joint disintegration and reflected pushforward. Every S_y is the normalized exp(-W_y) law with W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), C2 potential and finite positive normalizer. Choose one genuine compact-test gradient D_y on scalar/vector L2(S_y), dense and closable with the exact almost-everywhere smooth-gradient graph. For this same D_y, every epsilon>0 and scalar L2 input f has a unique weak solution u in the domain of D_y.closure with the exact energy identity and epsilon^-1 norm and energy bounds.
Lean statement · conditional_weak_resolvent
Actual common conditional kernels, normalized C2 potential, dense closable exact gradient graph, then every positive-epsilon weak solution with exact energy, bounds and uniqueness.
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 conditional_weak_resolvent {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α β : NNReal} {η : ℝ}
(hα : 0 < (α:ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ (β:ℝ)*‖v‖^2)
(hη : 0 < η) (hβη : (β:ℝ)*η ≤ 1) :
let μ := (volume : Measure E).tilted (fun x => -V x)
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
(J.map Prod.swap).IsCondKernel R ∧
(∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
0 < (∫ u, Real.exp (-W y u)) ∧
∃ D : Lp ℝ 2 (S y) →ₗ.[ℝ] Lp E 2 (S y),
Dense (D.domain : Set (Lp ℝ 2 (S y))) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
(∀ (u : Lp ℝ 2 (S y)) (v : Lp E 2 (S y)), (u,v) ∈ D.graph ↔
∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
u =ᵐ[S y] f ∧ v =ᵐ[S y] gradient f) ∧
∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 (S y),
∃ u : D.closure.domain,
(∀ v : D.closure.domain, ε * ⟪(u : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) ∧
ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 = ⟪f, (u : Lp ℝ 2 (S y))⟫ ∧
‖(u : Lp ℝ 2 (S y))‖ ≤ ε⁻¹ * ‖f‖ ∧
ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 ≤ ε⁻¹ * ‖f‖^2 ∧
∀ w : D.closure.domain,
(∀ v : D.closure.domain, ε * ⟪(w : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
⟪D.closure w, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) → w = uProof roadmap
- 1Preserve the same conditional probability and gradient
Use conditional_gradient_closable to obtain common R,S and, at each y, the actual normalized potential and one dense closable partial gradient. Retain its exact graph equivalence with smooth compact f and their genuine gradients. The operator is chosen before epsilon and f.
- 2Use the proved closed extension on the actual fiber
Take A=D_y.closure in the Hilbert spaces of scalar and vector L2(S_y). The parent theorem already proves that this closure has a closed graph. Thus the abstract theorem applies without assuming PI, domain coercivity or a classical differential equation.
- 3Retain uniqueness and constants without claiming regularity
The abstract result supplies the exact weak equation over every closed-domain test, energy identity, both explicit bounds and uniqueness on that same domain. This is an L2 domain statement. It does not justify substitution into compact-test Bochner or a pointwise PDE identity.
Full assumptions and notation
All objects and hypotheses
- E is finite-dimensional real inner-product Borel, including dimension zero, and V is C2.
- Explicit 0<alpha≤beta, genuine lower/upper Hessian quadratic-form bounds, eta>0 and beta eta≤1 are inherited from the actual kernel interface. They are not needed by the abstract closed-graph theorem.
- Mu is the actual normalized tilt by -V. J is the pushforward of independent Gibbs X and standard Gaussian Z under (X,X+sqrt(eta)Z).
- Common R,S precede every y; each D_y precedes every epsilon and f. The exact graph iff characterizes D_y, not every element of its closure.
- Integrable exp(-W_y) and its positive normalizer are proved conclusions supplied by the same actual conditional law, not additional paper assumptions. No measurability of y-to-D_y or y-to-solution is asserted.
Mathematical proof
1. Preserve the same conditional probability and gradient
Use conditional_gradient_closable to obtain common R,S and, at each y, the actual normalized potential and one dense closable partial gradient. Retain its exact graph equivalence with smooth compact f and their genuine gradients. The operator is chosen before epsilon and f.
Corresponding Lean step
hfiber supplies hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph; every one is retained in the result.
2. Use the proved closed extension on the actual fiber
Take A=D_y.closure in the Hilbert spaces of scalar and vector L2(S_y). The parent theorem already proves that this closure has a closed graph. Thus the abstract theorem applies without assuming PI, domain coercivity or a classical differential equation.
Corresponding Lean step
Instantiate ClosedGraphResolvent.weak_resolvent with D.closure and hClosed for each positive epsilon and each input f.
3. Retain uniqueness and constants without claiming regularity
The abstract result supplies the exact weak equation over every closed-domain test, energy identity, both explicit bounds and uniqueness on that same domain. This is an L2 domain statement. It does not justify substitution into compact-test Bochner or a pointwise PDE identity.
Corresponding Lean step
All clauses are returned directly for the same D and actual S_y; generator core/regularity and the epsilon-to-zero step remain separate obligations.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_weak_resolvent
The consumer uses the same parent kernels and operator; its only analytic application is the proved closed-graph 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.
theorem conditional_weak_resolvent {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α β : NNReal} {η : ℝ}
(hα : 0 < (α:ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
(hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
(fderiv ℝ (fderiv ℝ V) x v) v ≤ (β:ℝ)*‖v‖^2)
(hη : 0 < η) (hβη : (β:ℝ)*η ≤ 1) :
let μ := (volume : Measure E).tilted (fun x => -V x)
let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2)) (μ.prod (stdGaussian E))
let W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
(J.map Prod.swap).IsCondKernel R ∧
(∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
∀ y, S y = (volume : Measure E).tilted (fun u => -W y u) ∧
ContDiff ℝ 2 (W y) ∧ Integrable (fun u => Real.exp (-W y u)) ∧
0 < (∫ u, Real.exp (-W y u)) ∧
∃ D : Lp ℝ 2 (S y) →ₗ.[ℝ] Lp E 2 (S y),
Dense (D.domain : Set (Lp ℝ 2 (S y))) ∧ D.IsClosable ∧ D.closure.IsClosed ∧
(∀ (u : Lp ℝ 2 (S y)) (v : Lp E 2 (S y)), (u,v) ∈ D.graph ↔
∃ f : E → ℝ, ContDiff ℝ ∞ f ∧ HasCompactSupport f ∧
u =ᵐ[S y] f ∧ v =ᵐ[S y] gradient f) ∧
∀ (ε : ℝ), 0 < ε → ∀ f : Lp ℝ 2 (S y),
∃ u : D.closure.domain,
(∀ v : D.closure.domain, ε * ⟪(u : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
⟪D.closure u, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) ∧
ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 = ⟪f, (u : Lp ℝ 2 (S y))⟫ ∧
‖(u : Lp ℝ 2 (S y))‖ ≤ ε⁻¹ * ‖f‖ ∧
ε * ‖(u : Lp ℝ 2 (S y))‖^2 + ‖D.closure u‖^2 ≤ ε⁻¹ * ‖f‖^2 ∧
∀ w : D.closure.domain,
(∀ v : D.closure.domain, ε * ⟪(w : Lp ℝ 2 (S y)), (v : Lp ℝ 2 (S y))⟫ +
⟪D.closure w, D.closure v⟫ = ⟪f, (v : Lp ℝ 2 (S y))⟫) → w = u := by
obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
ConditionalGradient.conditional_gradient_closable hα hαβ hV hH hη hβη
dsimp only
refine ⟨R,S,hR,hS,hcond,hSR,?_⟩
intro y
obtain ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph⟩ := hfiber y
refine ⟨hSy,hW,hI,hZ,D,hDense,hClose,hClosed,hgraph,?_⟩
intro ε hε f
exact AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent.weak_resolvent D.closure hClosed ε hε f
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolventSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Euclidean d>=1. | Arbitrary finite-dimensional real inner-product Borel E, including zero dimension. | generalization | Explicit dimension-zero extension retained. |
| Appendix C.1 conditional Poincare/variance. | Actual conditional closed-gradient epsilon weak equation only. | API-limitation | Generator core/regularity, compact Bochner extension, mean-zero limit and score extension remain open. |
| Actual augmentation and conditional Gibbs law. | Same common R,S; every actual normalized C2 fiber; one exact D_y before all epsilon,f. | source-implicit | No unrelated law or arbitrary surrogate operator and no extra integrability premise. |
| Source curvature and scale hypotheses. | 0<alpha<=beta, C2, true Hessian bounds, eta>0 and beta eta<=1 retained. | same | Inherited parent restrictions, not required by the abstract weak theorem. |
Weak equation on the closed gradient domain only. No classical PDE regularity, identified maximal differential domain, D*D operator core, compact-test Bochner extension, epsilon-uniform estimate, Poincare, noncompact score variance, measurable parameter selection, process/error/cost or full-paper conclusion.
Encoder–denoiser: accepted · domain-mismatch
Detected semantic differences
- domains: Explicit finite-dimensional and zero-dimensional extension. — No positive-dimension premise; zero dimension explicitly disclosed.
- scopes: Authored weak-resolvent prerequisite, not C.1 PI/variance. — Graph iff describes D, not closure; uniqueness is of domain L2 classes, not pointwise representatives.
- assumptions: Curvature and beta eta<=1 retained parent restrictions, not abstract weak-existence premises. — hSy,hW,hI,hZ,hClosed from same parent, not added premises.
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
- Weak equation on the closed gradient domain only. No classical PDE regularity, identified maximal differential domain, D*D operator core, compact-test Bochner extension, epsilon-uniform estimate, Poincare, noncompact score variance, measurable parameter selection, process/error/cost or full-paper conclusion.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient.conditional_gradient_closableAutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent.weak_resolvent
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
- Chen, Chewi, Lu and Zhang, PBPS Appendix C.1 — Actual conditional weak-form prerequisite, not the conditional PI or variance estimate.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.