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

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.

\[\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

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.