Actual scaled closed-graph resolvent norm limit

Samplinglib authored actual scaled-resolvent analytic prerequisite for omitted Poincare/BL background; not the printed source proof or a completed Poincare/BL/main theorem.

Complete source statement (Samplinglib restatement)

For every actual variational solution sequence in SAME closed D, both epsilon_n*u_n and epsilon_n*D(u_n) tend0 strongly when genuine forcing is orthogonal to the entire kernel. Explicit Hilbert/Riesz/graph/energy hypotheses only.

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 scaled closed-graph resolvent norm limit

AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ScaledClosedGraphResolvent.scaled_resolvent_sequence_tendsto_zero · theorem · Teaching coverage

Read this first

Mathematical statement

\[\varepsilon_n\langle u_n,v\rangle+\langle Du_n,Dv\rangle=\langle f,v\rangle,\quad f\perp\ker D,\quad\varepsilon_n>0,\ \varepsilon_n\to0\Longrightarrow\varepsilon_nu_n\to0,\ \varepsilon_nDu_n\to0.\]

Lean statement · scaled_resolvent_sequence_tendsto_zero

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 scaled_resolvent_sequence_tendsto_zero
    [TopologicalSpace.SeparableSpace H]
    (D : H →ₗ.[ℝ] K) (hD : D.IsClosed) (f : H)
    (ε : ℕ → ℝ) (hε : ∀ n, 0 < ε n) (hε0 : Tendsto ε atTop (𝓝 0))
    (u : ℕ → D.domain)
    (hv : ∀ n, ∀ v : D.domain,
      ε n*inner ℝ (u n : H) (v : H)+inner ℝ (D (u n)) (D v)=inner ℝ f (v : H))
    (hk : ∀ v : D.domain, D v=0 → inner ℝ f (v : H)=0) :
    Tendsto (fun n => ε n • (u n : H)) atTop (𝓝 0) ∧
    Tendsto (fun n => ε n • D (u n)) atTop (𝓝 0)

Exact module and namespace context

Proof roadmap

1Scale in the SAME actual linear domain
Put r_n=epsilon_n*u_n in the genuine domain. The actual self variational test gives energy; scaling and true partial linearity give the residual and gradient energy estimates, also when f=0.
2Derive actual scaled gradient strongzero
Squeeze true squared norms by epsilon_n*normf^2, pass through sqrt and the genuine norm-tendsto criterion. No unscaled gradient or solution limit is assumed.
3Extract a genuine weak subsequence
For each bounded subsequence, map its actual vectors through the Riesz isometry into WeakDual. Explicit separability gives genuine sequential Banach-Alaoglu. Pull the limit back by inverse Riesz and prove every inner evaluation limit.
4Use the correct Hilbert product graph
Ordinary H*K has max norm. Comap the SAME D.graph to WithLp2 through its actual linear equivalence; continuous ofLp gives true closedness. Double orthogonal equals this actual closed submodule.
5Admit the actual weak-strong graph limit
Pair each (r_n,Dr_n) with every vector in G-perp. Weak first component and strongly-zero second component preserve all zero pairings. Double orthogonal and mem_graph_iff produce an actual domain witness equal to v with Dv=0.
6Force residual normzero along that subsequence
The actual forcing/kernel orthogonality gives <f,v≥0. Energy normr^2≤<f,r>, weak evaluation and square-root squeeze therefore give strong residualzero. This uses no Poincare or unscaled uniform bound.
7Promote to whole-sequence convergence
Apply the true subsequence-tendsto criterion to every index sequence tendingatTop. Each has a further actual weak subsequence and the same strongzero limit, yielding the whole residual limit and retaining the scaled-gradient limit.

Full assumptions and notation

All objects and hypotheses

Real complete Hilbert H,K; H genuinely separable, SAME actual closed partial-linear D before f and all solution data. Positive epsilon_n tending0; actual domain u_n satisfies ALL genuine variational tests epsilon_n<un,v>+<Dun,Dv≥<f,v>.
Forcing f is orthogonal to EVERY v in SAME domain with Dv=0. No supplied weak clusters/closedgraph-limit certificate, Poincare, unscaled uniform solution bound, finite-dimensional H or K, or dense/range premise.

Mathematical proof

1. Scale in the SAME actual linear domain

Put r_n=epsilon_n*u_n in the genuine domain. The actual self variational test gives energy; scaling and true partial linearity give the residual and gradient energy estimates, also when f=0.

\[\|r_n\|^2+\varepsilon_n\|Du_n\|^2=\langle f,r_n\rangle,\quad\|r_n\|\le\|f\|,\quad\|Dr_n\|^2\le\varepsilon_n\|f\|^2.\]

Corresponding Lean step

scaled_energy_bounds; LinearPMap.map_smul

2. Derive actual scaled gradient strongzero

Squeeze true squared norms by epsilon_n*normf^2, pass through sqrt and the genuine norm-tendsto criterion. No unscaled gradient or solution limit is assumed.

\[Dr_n=\varepsilon_nDu_n\to0\text{ strongly in }K.\]

Corresponding Lean step

squeeze_zero; Real.continuous_sqrt; scaled_resolvent_sequence_tendsto_zero

3. Extract a genuine weak subsequence

For each bounded subsequence, map its actual vectors through the Riesz isometry into WeakDual. Explicit separability gives genuine sequential Banach-Alaoglu. Pull the limit back by inverse Riesz and prove every inner evaluation limit.

\[\langle r_{n_j},a\rangle\to\langle v,a\rangle\quad\forall a\in H.\]

Corresponding Lean step

bounded_weak_subsequence; WeakDual.isSeqCompact_closedBall; InnerProductSpace.toDual_symm_apply

4. Use the correct Hilbert product graph

Ordinary H*K has max norm. Comap the SAME D.graph to WithLp2 through its actual linear equivalence; continuous ofLp gives true closedness. Double orthogonal equals this actual closed submodule.

\[G=\operatorname{ofLp}^{-1}(\operatorname{graph}D)\subset H\oplus_2K,\quad G^{\perp\perp}=G.\]

Corresponding Lean step

weak_strong_closed_graph; WithLp.prod_continuous_ofLp; Submodule.orthogonal_orthogonal_eq_closure

5. Admit the actual weak-strong graph limit

Pair each (r_n,Dr_n) with every vector in G-perp. Weak first component and strongly-zero second component preserve all zero pairings. Double orthogonal and mem_graph_iff produce an actual domain witness equal to v with Dv=0.

\[(v,0)\in G\Longrightarrow v\in\operatorname{dom}D,\ Dv=0.\]

Corresponding Lean step

WithLp.prod_inner_apply; LinearPMap.mem_graph_iff; weak_strong_closed_graph

6. Force residual normzero along that subsequence

The actual forcing/kernel orthogonality gives <f,v≥0. Energy normr^2≤<f,r>, weak evaluation and square-root squeeze therefore give strong residualzero. This uses no Poincare or unscaled uniform bound.

\[0\le\|r_{n_j}\|^2\le\langle f,r_{n_j}\rangle\to\langle f,v\rangle=0.\]

Corresponding Lean step

bounded_kernel_orthogonal_sequence_tendsto_zero; real_inner_comm; squeeze_zero

7. Promote to whole-sequence convergence

Apply the true subsequence-tendsto criterion to every index sequence tendingatTop. Each has a further actual weak subsequence and the same strongzero limit, yielding the whole residual limit and retaining the scaled-gradient limit.

\[\varepsilon_nu_n\to0,\quad\varepsilon_nDu_n\to0.\]

Corresponding Lean step

Filter.tendsto_of_subseq_tendsto; scaled_resolvent_sequence_tendsto_zero

Lean verification

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

Lean proof · scaled_resolvent_sequence_tendsto_zero

Scale in the SAME actual linear domain; Derive actual scaled gradient strongzero; Extract a genuine weak subsequence; Use the correct Hilbert product graph; Admit the actual weak-strong graph limit; Force residual normzero along that subsequence; Promote to whole-sequence convergence

Download module (.lean)

theorem scaled_resolvent_sequence_tendsto_zero
    [TopologicalSpace.SeparableSpace H]
    (D : H →ₗ.[ℝ] K) (hD : D.IsClosed) (f : H)
    (ε : ℕ → ℝ) (hε : ∀ n, 0 < ε n) (hε0 : Tendsto ε atTop (𝓝 0))
    (u : ℕ → D.domain)
    (hv : ∀ n, ∀ v : D.domain,
      ε n*inner ℝ (u n : H) (v : H)+inner ℝ (D (u n)) (D v)=inner ℝ f (v : H))
    (hk : ∀ v : D.domain, D v=0 → inner ℝ f (v : H)=0) :
    Tendsto (fun n => ε n • (u n : H)) atTop (𝓝 0) ∧
    Tendsto (fun n => ε n • D (u n)) atTop (𝓝 0) := by
  let r : ℕ → D.domain := fun n => ε n • u n
  have he (n : ℕ) : ε n*‖(u n : H)‖^2+‖D (u n)‖^2=inner ℝ f (u n : H) := by
    simpa only [real_inner_self_eq_norm_sq] using hv n (u n)
  have hb (n : ℕ) := scaled_energy_bounds (ε n) (hε n) f (u n) (D (u n)) (he n)
  have hDsq : Tendsto (fun n => ‖D (r n)‖^2) atTop (𝓝 0) := by
    apply squeeze_zero (fun n => sq_nonneg _) (fun n => ?_)
      (by simpa only [zero_mul] using hε0.mul_const (‖f‖^2))
    simpa only [r,D.map_smul] using (hb n).2.2
  have hDz : Tendsto (fun n => D (r n)) atTop (𝓝 0) := by
    apply tendsto_zero_iff_norm_tendsto_zero.mpr
    simpa only [Function.comp_def,Real.sqrt_sq (norm_nonneg _),Real.sqrt_zero] using
      Real.continuous_sqrt.continuousAt.tendsto.comp hDsq
  exact ⟨bounded_kernel_orthogonal_sequence_tendsto_zero D hD r f
    (fun n => (hb n).1) hDz (fun n => (hb n).2.1) hk,by
      simpa only [r,D.map_smul] using hDz⟩


end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ScaledClosedGraphResolvent

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Actual PBPS reflected C2 conditional law/background Poincare.	Real complete Hilbert H,K; H genuinely separable, SAME actual closed partial-linear D before f and all solution data. Positive epsilon_n tending0; actual domain u_n satisfies ALL genuine variational tests epsilon_n<un,v>+<Dun,Dv>=<f,v>. Forcing f is orthogonal to EVERY v in SAME domain with Dv=0. No supplied weak clusters/closedgraph-limit certificate, Poincare, unscaled uniform solution bound, finite-dimensional H or K, or dense/range premise.	generalization	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.	For every actual variational solution sequence in SAME closed D, both epsilon_nu_n and epsilon_nD(u_n) tend0 strongly when genuine forcing is orthogonal to the entire kernel. Explicit Hilbert/Riesz/graph/energy hypotheses only.	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 epsilonu_n->0 and epsilonD(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

Mathlib API called (external library)

InnerProductSpace.toDual
InnerProductSpace.toDual_symm_apply
WeakDual.isSeqCompact_closedBall
WithLp.prod_continuous_ofLp
WithLp.prod_inner_apply
Submodule.orthogonal_orthogonal_eq_closure
LinearPMap.mem_graph_iff
Filter.tendsto_of_subseq_tendsto

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.

Actual scaled closed-graph resolvent norm limit

Complete source statement (Samplinglib restatement)

Actual scaled closed-graph resolvent norm limit

Read the formalized proofs

Actual scaled closed-graph resolvent norm limit

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Scale in the SAME actual linear domain

2. Derive actual scaled gradient strongzero

3. Extract a genuine weak subsequence

4. Use the correct Hilbert product graph

5. Admit the actual weak-strong graph limit

6. Force residual normzero along that subsequence

7. Promote to whole-sequence convergence

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?