Actual scaled closed-graph resolvent norm limit
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ScaledClosedGraphResolvent.scaled_resolvent_sequence_tendsto_zero · theorem · Teaching coverage
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.
Lean statement · scaled_resolvent_sequence_tendsto_zero
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.
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 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)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.
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.
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.
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.
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.
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.
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.
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
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 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.ScaledClosedGraphResolventScope 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.