Actual reflected conditional centered residual limit
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCenteredResolventLimit.conditional_centered_resolvent_sequence · theorem · Teaching coverage
Mathematical statement
Construct true common Gaussian/disintegrating/reflected J/R/S and one original dense closable D_y before ALL centered forcing/epsilon sequences. Construct true same-domain variational solutions on actual S_y with strong epsilon_n*u_n zero limit, retaining source curvature/eta cap/partition/order.
Lean statement · conditional_centered_resolvent_sequence
Construct true common Gaussian/disintegrating/reflected J/R/S and one original dense closable D_y before ALL centered forcing/epsilon sequences. Construct true same-domain variational solutions on actual S_y with strong epsilon_n*u_n zero limit, retaining source curvature/eta cap/partition/order.
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_centered_resolvent_sequence
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α β : NNReal} {η : ℝ}
(hα : 0 < (α:ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
(hH : ∀ x a : E, (α:ℝ)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
fderiv ℝ (fderiv ℝ V) x a a ≤ (β:ℝ)*‖a‖^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 ∧
(∀ (a : Lp ℝ 2 (S y)) (G : Lp E 2 (S y)), (a,G) ∈ D.graph ↔
∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
a =ᵐ[S y] φ ∧ G =ᵐ[S y] gradient φ) ∧
∀ f : Lp ℝ 2 (S y), (∫ x, f x ∂S y)=0 →
∀ (ε : ℕ → ℝ), (∀ n, 0 < ε n) → Tendsto ε atTop (𝓝 0) →
∃ u : ℕ → D.closure.domain,
(∀ n, ∀ v : D.closure.domain,
ε n*inner ℝ (u n : Lp ℝ 2 (S y)) (v : Lp ℝ 2 (S y))+
inner ℝ (D.closure (u n)) (D.closure v)=inner ℝ f (v : Lp ℝ 2 (S y))) ∧
Tendsto (fun n => ε n • (u n : Lp ℝ 2 (S y))) atTop (𝓝 0)Proof roadmap
- 1Keep the actual common law and original domain order
Accepted ConditionalScoreClosedDomain constructs common Gaussian J/R/S, disintegration/reflection, true C2 W_y/positive partition and original dense/closable/exact D_y before every centered forcing or epsilon query. Source curvature/eta cap retained.
- 2Transfer by literal actual density only
Use exact S_y=volume.tilted(-W_y) to rewrite the shared Gibbs prerequisite onto this SAME conditional law and SAME D_y. No auxiliary R2=R or alternate-operator identification is used.
- 3Produce real conditional solutions and normzero
For every true centered L2 forcing and every positive epsilon sequence→0, the shared actual producer gives same-domain u_n, all variational equations and the strong scaled residual limit. This supplies a later actual centered-domain Poincare node; that node/score variance/BL/main remain open.
Full assumptions and notation
All objects and hypotheses
- Source V C2, NNReal0<alpha≤beta and actual allpoint/allvector alphaI≤HessV≤betaI; eta>0,beta*eta≤1. Full finite-dimensional real Hilbert/Borel E including0.
- Actual common Gaussian J=(x,x+sqrteta*xi)#(mu*Gamma), Markov/disintegrating R and actual reflected S_y=(2x-y)#R_y. W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), exact normalized reflected density and positive integrable partition. SAME original dense closable compact-smooth gradient D_y chosen BEFORE ALL meanzero L2 forcing f and epsilon sequences.
- Mean-zero forcing is with respect to actual S_y; real variational solutions and scaled residual limit are constructed fiberwise. No identification of auxiliary conditional versions, jointly measurable solution selector, or normalized score derivative.
Mathematical proof
1. Keep the actual common law and original domain order
Accepted ConditionalScoreClosedDomain constructs common Gaussian J/R/S, disintegration/reflection, true C2 W_y/positive partition and original dense/closable/exact D_y before every centered forcing or epsilon query. Source curvature/eta cap retained.
Corresponding Lean step
ConditionalScoreClosedDomain.conditional_score_closed_gradient_domain
2. Transfer by literal actual density only
Use exact S_y=volume.tilted(-W_y) to rewrite the shared Gibbs prerequisite onto this SAME conditional law and SAME D_y. No auxiliary R2=R or alternate-operator identification is used.
Corresponding Lean step
CenteredGibbsResolventLimit.gibbs_centered_resolvent_sequence; conditional_centered_resolvent_sequence
3. Produce real conditional solutions and normzero
For every true centered L2 forcing and every positive epsilon sequence→0, the shared actual producer gives same-domain u_n, all variational equations and the strong scaled residual limit. This supplies a later actual centered-domain Poincare node; that node/score variance/BL/main remain open.
Corresponding Lean step
conditional_centered_resolvent_sequence; Tests.ScaledResolventLimit.actual_nonquadratic_centered_resolvent
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · conditional_centered_resolvent_sequence
Keep the actual common law and original domain order; Transfer by literal actual density only; Produce real conditional solutions and normzero
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_centered_resolvent_sequence
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
[FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
{V : E → ℝ} {α β : NNReal} {η : ℝ}
(hα : 0 < (α:ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
(hH : ∀ x a : E, (α:ℝ)*‖a‖^2 ≤ fderiv ℝ (fderiv ℝ V) x a a ∧
fderiv ℝ (fderiv ℝ V) x a a ≤ (β:ℝ)*‖a‖^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 ∧
(∀ (a : Lp ℝ 2 (S y)) (G : Lp E 2 (S y)), (a,G) ∈ D.graph ↔
∃ φ : E → ℝ, ContDiff ℝ ∞ φ ∧ HasCompactSupport φ ∧
a =ᵐ[S y] φ ∧ G =ᵐ[S y] gradient φ) ∧
∀ f : Lp ℝ 2 (S y), (∫ x, f x ∂S y)=0 →
∀ (ε : ℕ → ℝ), (∀ n, 0 < ε n) → Tendsto ε atTop (𝓝 0) →
∃ u : ℕ → D.closure.domain,
(∀ n, ∀ v : D.closure.domain,
ε n*inner ℝ (u n : Lp ℝ 2 (S y)) (v : Lp ℝ 2 (S y))+
inner ℝ (D.closure (u n)) (D.closure v)=inner ℝ f (v : Lp ℝ 2 (S y))) ∧
Tendsto (fun n => ε n • (u n : Lp ℝ 2 (S y))) atTop (𝓝 0) := by
obtain ⟨R,S,hR,hS,hcond,hSR,hfiber⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreClosedDomain.conditional_score_closed_gradient_domain
hα hαβ hV hH hη hβη
dsimp only
refine ⟨R,S,hR,hS,hcond,hSR,?_⟩
intro y
obtain ⟨hSy,hW,hI,hZ,D,hd,hD,hDc,hgraph,_⟩ := hfiber y
refine ⟨hSy,hW,hI,hZ,D,hd,hD,hDc,hgraph,?_⟩
have hg := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredGibbsResolventLimit.gibbs_centered_resolvent_sequence _ (hW.of_le (by norm_num)) hI
rw [← hSy] at hg
intro f hf ε hε hε0
obtain ⟨_,u,hu,ht⟩ := hg D hD hgraph f hf ε hε hε0
exact ⟨u,fun n => (hu n).1,ht⟩
end AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCenteredResolventLimitSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Actual PBPS reflected C2 conditional law/background Poincare. | Source V C2, NNReal0<alpha<=beta and actual allpoint/allvector alphaI<=HessV<=betaI; eta>0,beta*eta<=1. Full finite-dimensional real Hilbert/Borel E including0. Actual common Gaussian J=(x,x+sqrteta*xi)#(mu*Gamma), Markov/disintegrating R and actual reflected S_y=(2x-y)#R_y. W_y(u)=V((y+u)/2)+norm(u-y)^2/(8eta), exact normalized reflected density and positive integrable partition. SAME original dense closable compact-smooth gradient D_y chosen BEFORE ALL meanzero L2 forcing f and epsilon sequences. Mean-zero forcing is with respect to actual S_y; real variational solutions and scaled residual limit are constructed fiberwise. No identification of auxiliary conditional versions, jointly measurable solution selector, or normalized score derivative. | source-implicit | Explicit abstract separability/kernel orthogonality is genuinely derived from actual finite-dimensional Borel Gibbs probability/mean-zero forcing at the source consumer. |
| Source directly invokes Poincare/BL and does not construct epsilon resolvents. | Construct true common Gaussian/disintegrating/reflected J/R/S and one original dense closable D_y before ALL centered forcing/epsilon sequences. Construct true same-domain variational solutions on actual S_y with strong epsilon_n*u_n zero limit, retaining source curvature/eta cap/partition/order. | source-implicit | Authored actual variational/Riesz/WithLp2 closed-graph/centering proof of the missing residual limit; no source theorem completion. |
| Poincare/BL/score variance/range/adjoint/core/main/composition. | Fix real complete Hilbert H,K and SAME actual closed partial linear D before forcing f, positive epsilon sequence->0 and actual variational solutions u_n. H separable explicitly; actual finite-dimensional Borel Gibbs E gives genuine scalar L2 separability by countably generated finite measure, not finite-dimensional L2. Actual energy/scaled domain, Riesz WeakDual sequential compactness, WithLp2 genuine graph double-orthogonal and forcing orthogonal to EVERY kernel give strong epsilon*u_n->0 and epsilon*D(u_n)->0 without Poincare or uniform unscaled u. True C1 Gibbs W/positive exponential normalizer/actual normalized probability and SAME exact original compact-smooth closable gradient beforeALLf; genuine mean-zero L2 forcing is integrable and kernel-orthogonal via actual AEconstant. Construct actual positive-epsilon variational solutions, retaining ordinary localL1/weakC1 test integrabilities. Actual common PBPS J/R/S/reflected law/sourceC2 alpha-beta/eta cap/positive partitions and originalD_y beforeALLf/epsilon; fiberwise only. No epsilon0 solution/range/unscaled uniform bound/extra spatial moment/supplied weak-limit or graph or residual certificate/Poincare/BL/core/adjoint/jointselector/normalized conditional-score derivative/both main/composition; TV never transfers unbounded expectedcost. | unresolved | Only strong scaled-resolvent norm limit with true conditional consumer is admitted; no unscaled bound, spectralgap/range certificate or jointly measurable selector. |
Fix real complete Hilbert H,K and SAME actual closed partial linear D before forcing f, positive epsilon sequence->0 and actual variational solutions u_n. H separable explicitly; actual finite-dimensional Borel Gibbs E gives genuine scalar L2 separability by countably generated finite measure, not finite-dimensional L2. Actual energy/scaled domain, Riesz WeakDual sequential compactness, WithLp2 genuine graph double-orthogonal and forcing orthogonal to EVERY kernel give strong epsilon*u_n->0 and epsilon*D(u_n)->0 without Poincare or uniform unscaled u. True C1 Gibbs W/positive exponential normalizer/actual normalized probability and SAME exact original compact-smooth closable gradient beforeALLf; genuine mean-zero L2 forcing is integrable and kernel-orthogonal via actual AEconstant. Construct actual positive-epsilon variational solutions, retaining ordinary localL1/weakC1 test integrabilities. Actual common PBPS J/R/S/reflected law/sourceC2 alpha-beta/eta cap/positive partitions and originalD_y beforeALLf/epsilon; fiberwise only. No epsilon0 solution/range/unscaled uniform bound/extra spatial moment/supplied weak-limit or graph or residual certificate/Poincare/BL/core/adjoint/jointselector/normalized conditional-score derivative/both main/composition; TV never transfers unbounded expectedcost.
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
- Fix real complete Hilbert H,K and SAME actual closed partial linear D before forcing f, positive epsilon sequence→0 and actual variational solutions u_n. H separable explicitly; actual finite-dimensional Borel Gibbs E gives genuine scalar L2 separability by countably generated finite measure, not finite-dimensional L2. Actual energy/scaled domain, Riesz WeakDual sequential compactness, WithLp2 genuine graph double-orthogonal and forcing orthogonal to EVERY kernel give strong epsilon*u_n→0 and epsilon*D(u_n)→0 without Poincare or uniform unscaled u. True C1 Gibbs W/positive exponential normalizer/actual normalized probability and SAME exact original compact-smooth closable gradient beforeALLf; genuine mean-zero L2 forcing is integrable and kernel-orthogonal via actual AEconstant. Construct actual positive-epsilon variational solutions, retaining ordinary localL1/weakC1 test integrabilities. Actual common PBPS J/R/S/reflected law/sourceC2 alpha-beta/eta cap/positive partitions and originalD_y beforeALLf/epsilon; fiberwise only. No epsilon0 solution/range/unscaled uniform bound/extra spatial moment/supplied weak-limit or graph or residual certificate/Poincare/BL/core/adjoint/jointselector/normalized conditional-score derivative/both main/composition; TV never transfers unbounded expectedcost.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredGibbsResolventLimit.gibbs_centered_resolvent_sequenceAutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreClosedDomain.conditional_score_closed_gradient_domain
Mathlib API called (external library)
No direct Mathlib call recorded; see the Samplinglib parents.
Mathematical sources
- PBPS AppC1 omitted-background analytic prerequisite — Fix real complete Hilbert H,K and SAME actual closed partial linear D before forcing f, positive epsilon sequence->0 and actual variational solutions u_n. H separable explicitly; actual finite-dimensional Borel Gibbs E gives genuine scalar L2 separability by countably generated finite measure, not finite-dimensional L2. Actual energy/scaled domain, Riesz WeakDual sequential compactness, WithLp2 genuine graph double-orthogonal and forcing orthogonal to EVERY kernel give strong epsilon*u_n->0 and epsilon*D(u_n)->0 without Poincare or uniform unscaled u. True C1 Gibbs W/positive exponential normalizer/actual normalized probability and SAME exact original compact-smooth closable gradient beforeALLf; genuine mean-zero L2 forcing is integrable and kernel-orthogonal via actual AEconstant. Construct actual positive-epsilon variational solutions, retaining ordinary localL1/weakC1 test integrabilities. Actual common PBPS J/R/S/reflected law/sourceC2 alpha-beta/eta cap/positive partitions and originalD_y beforeALLf/epsilon; fiberwise only. No epsilon0 solution/range/unscaled uniform bound/extra spatial moment/supplied weak-limit or graph or residual certificate/Poincare/BL/core/adjoint/jointselector/normalized conditional-score derivative/both main/composition; TV never transfers unbounded expectedcost.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.