A unique weak resolvent from a closed Hilbert graph
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent.weak_resolvent · theorem · Teaching coverage
Statement
Let H,K be real Hilbert spaces and A a partial real-linear operator with closed graph. For each epsilon>0 and f in H, there is a unique domain element u such that epsilon inner(u,v)+inner(Au,Av)=inner(f,v) for every v in the domain. It satisfies the exact energy identity epsilon norm(u)^2+norm(Au)^2=inner(f,u), the ambient bound norm(u)<=epsilon^-1 norm(f), and the energy bound <=epsilon^-1 norm(f)^2. No density, boundedness, Poincare or prior solvability is assumed.
All objects and hypotheses
- H and K are complete real inner-product spaces; they may be infinite dimensional.
- A is a partial real-linear map with a linear-subspace domain, and its graph is closed in H times K. The domain is not assumed dense or all of H, and A is not assumed bounded.
- Epsilon is strictly positive and f is an arbitrary H element. Domain-element norms in the statement are ambient H norms, not graph norms.
- This is an abstract Hilbert weak-form prerequisite inspired by the Poisson/Sobolev discussion in Kolesnikov-Milman sections2.4-2.5. It is not that source compact-manifold Poisson existence/regularity theorem, nor PBPS conditional Poincare.
Mathematical proof
1. Place the scaled graph in a Hilbert product
Set s=sqrt(epsilon)>0. On H direct-sum K with its L2 product norm use T(a,b)=(s^-1 a,b). Define G as the inverse image under T of the graph of A. T is continuous linear, so G is a closed subspace and therefore complete. This avoids assuming the unbounded operator is continuous.
Corresponding Lean step
The local hex proof uses WithLp.fstL/sndL, Submodule.comap, hA.preimage T.continuous and hG.completeSpace_coe.
2. Project and recover a genuine domain element
Project z=(s^-1 f,0) orthogonally onto G. Membership of p in G gives an actual u in the domain with u=s^-1 p_1 and Au=p_2. Since s is nonzero, p_1=s u. No totalized inverse or arbitrary differential representative is used.
Corresponding Lean step
starProjection_apply_mem and LinearPMap.mem_graph_iff provide u; scalar cancellation establishes hu'.
3. Orthogonality is exactly the weak equation
For every domain v, the vector w=(s v,Av) lies in G. Orthogonality of z-p to w gives inner(s^-1 f-s u,s v)-inner(Au,Av)=0. Expanding both inner products and using s^2=epsilon yields the weak equation for every test in the closed domain.
Corresponding Lean step
Submodule.starProjection_inner_eq_zero, the L2 product inner product and explicit nonzero-s scalar simplification close the local existence proof.
4. Derive the exact energy and explicit bounds
Use v=u in the weak equation. Cauchy-Schwarz bounds its right side by norm(f) norm(u). When norm(u)=0 the norm bound is immediate; otherwise divide its positive value to obtain epsilon norm(u)<=norm(f). Substitute this estimate back into the energy identity. The constants are explicit and deteriorate as epsilon approaches zero.
Corresponding Lean step
he is the self-test identity; hn handles the zero/nonzero norm branches, hb divides by positive epsilon, heb combines Cauchy-Schwarz and hb.
5. Prove uniqueness by testing the difference
If w also solves the same equation, subtract the two equations tested at d=w-u. Domain linearity and A(w-u)=Aw-Au give epsilon norm(d)^2+norm(Ad)^2=0. Positivity of epsilon forces the ambient norm of d to vanish, hence the two domain elements are equal.
Corresponding Lean step
The last quantified clause assumes only the weak equation for w, not its norm/energy bounds; Subtype.ext concludes equality from ambient norm zero.
Lean statement · weak_resolvent
Existence, exact energy, ambient H norm bound, energy bound, and uniqueness among all weak solutions on A.domain.
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 weak_resolvent {H K : Type*}
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
[NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K]
(A : H →ₗ.[ℝ] K) (hA : A.IsClosed) (ε : ℝ) (hε : 0 < ε) (f : H) :
∃ u : A.domain,
(∀ v : A.domain, ε * ⟪(u : H), (v : H)⟫ + ⟪A u, A v⟫ = ⟪f, (v : H)⟫) ∧
ε * ‖(u : H)‖^2 + ‖A u‖^2 = ⟪f, (u : H)⟫ ∧
‖(u : H)‖ ≤ ε⁻¹ * ‖f‖ ∧
ε * ‖(u : H)‖^2 + ‖A u‖^2 ≤ ε⁻¹ * ‖f‖^2 ∧
∀ w : A.domain,
(∀ v : A.domain, ε * ⟪(w : H), (v : H)⟫ + ⟪A w, A v⟫ = ⟪f, (v : H)⟫) → w = uLean proof · weak_resolvent
The scaled-graph existence proof is local to the single public theorem; the complete folded proof includes it and all 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 weak_resolvent {H K : Type*}
[NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
[NormedAddCommGroup K] [InnerProductSpace ℝ K] [CompleteSpace K]
(A : H →ₗ.[ℝ] K) (hA : A.IsClosed) (ε : ℝ) (hε : 0 < ε) (f : H) :
∃ u : A.domain,
(∀ v : A.domain, ε * ⟪(u : H), (v : H)⟫ + ⟪A u, A v⟫ = ⟪f, (v : H)⟫) ∧
ε * ‖(u : H)‖^2 + ‖A u‖^2 = ⟪f, (u : H)⟫ ∧
‖(u : H)‖ ≤ ε⁻¹ * ‖f‖ ∧
ε * ‖(u : H)‖^2 + ‖A u‖^2 ≤ ε⁻¹ * ‖f‖^2 ∧
∀ w : A.domain,
(∀ v : A.domain, ε * ⟪(w : H), (v : H)⟫ + ⟪A w, A v⟫ = ⟪f, (v : H)⟫) → w = u := by
have hex : ∃ u : A.domain, ∀ v : A.domain,
ε * ⟪(u : H), (v : H)⟫ + ⟪A u, A v⟫ = ⟪f, (v : H)⟫ := by
let s := Real.sqrt ε
have hs : 0 < s := Real.sqrt_pos.2 hε
have hs0 : s ≠ 0 := ne_of_gt hs
have hss : s * s = ε := Real.mul_self_sqrt hε.le
let T : WithLp 2 (H × K) →L[ℝ] H × K :=
(s⁻¹ • (WithLp.fstL 2 ℝ H K)).prod (WithLp.sndL 2 ℝ H K)
let G : Submodule ℝ (WithLp 2 (H × K)) := A.graph.comap T.toLinearMap
have hG : IsClosed (G : Set (WithLp 2 (H × K))) := hA.preimage T.continuous
let : CompleteSpace G := hG.completeSpace_coe
let z : WithLp 2 (H × K) := WithLp.toLp 2 (s⁻¹ • f, 0)
let p := G.starProjection z
have hp : T p ∈ A.graph := G.starProjection_apply_mem z
obtain ⟨u,hu,hAu⟩ := A.mem_graph_iff.mp hp
have hu' : s • (u : H) = p.fst := by
rw [hu]
change s • (s⁻¹ • p.fst) = p.fst
simp [smul_smul, hs0]
refine ⟨u, ?_⟩
intro v
let w : WithLp 2 (H × K) := WithLp.toLp 2 (s • (v : H), A v)
have hw : w ∈ G := by
change T w ∈ A.graph
apply A.mem_graph_iff.mpr
refine ⟨v, ?_, ?_⟩
· change (v : H) = s⁻¹ • (s • (v : H))
simp [smul_smul, hs0]
· rfl
have ho := G.starProjection_inner_eq_zero z w hw
change ⟪s⁻¹ • f - p.fst, s • (v : H)⟫ + ⟪(0 : K) - p.snd, A v⟫ = 0 at ho
have hAu' : A u = p.snd := hAu
rw [← hu', ← hAu'] at ho
simp only [inner_sub_left, real_inner_smul_left, real_inner_smul_right, zero_sub,
inner_neg_left] at ho
simp only [← mul_assoc, mul_inv_cancel₀ hs0, hss, one_mul] at ho
linarith
obtain ⟨u,hu⟩ := hex
have he : ε * ‖(u : H)‖^2 + ‖A u‖^2 = ⟪f, (u : H)⟫ := by
simpa only [real_inner_self_eq_norm_sq] using hu u
have hn : ε * ‖(u : H)‖ ≤ ‖f‖ := by
have hcs := real_inner_le_norm f (u : H)
by_cases hz : ‖(u : H)‖ = 0
· simp [hz]
· have hp : 0 < ‖(u : H)‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz)
nlinarith [sq_nonneg ‖A u‖]
have hb : ‖(u : H)‖ ≤ ε⁻¹ * ‖f‖ := by
have hn' : ‖(u : H)‖ ≤ ‖f‖ / ε := (le_div_iff₀ hε).2 (by simpa [mul_comm] using hn)
simpa [div_eq_mul_inv, mul_comm] using hn'
have heb : ε * ‖(u : H)‖^2 + ‖A u‖^2 ≤ ε⁻¹ * ‖f‖^2 := by
rw [he]
calc
⟪f, (u : H)⟫ ≤ ‖f‖ * ‖(u : H)‖ := real_inner_le_norm _ _
_ ≤ ‖f‖ * (ε⁻¹ * ‖f‖) := mul_le_mul_of_nonneg_left hb (norm_nonneg _)
_ = _ := by ring
refine ⟨u,hu,he,hb,heb,?_⟩
intro w hw
let d : A.domain := w-u
have hd : ε * ⟪(d : H), (d : H)⟫ + ⟪A d, A d⟫ = 0 := by
have heq := sub_eq_zero.mpr ((hw d).trans (hu d).symm)
have hAd : A d = A w - A u := A.toFun.map_sub w u
rw [hAd, inner_sub_left]
change ε * ⟪(w : H) - (u : H), (d : H)⟫ + _ = 0
rw [inner_sub_left]
rw [hAd] at heq
nlinarith
rw [real_inner_self_eq_norm_sq, real_inner_self_eq_norm_sq] at hd
have hz : ‖(d : H)‖ = 0 := by
by_contra hz
have hp : 0 < ‖(d : H)‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz)
have hpos := mul_pos hε (sq_pos_of_pos hp)
nlinarith [sq_nonneg ‖A d‖]
apply Subtype.ext
exact sub_eq_zero.mp (norm_eq_zero.mp hz)
end AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolventScope 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.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- WithLp.fstL
- WithLp.sndL
- Submodule.comap
- IsClosed.completeSpace_coe
- Submodule.starProjection_apply_mem
- Submodule.starProjection_inner_eq_zero
- LinearPMap.mem_graph_iff
- real_inner_le_norm
Mathematical sources
- Kolesnikov and Milman, sections2.4-2.5 — Poisson/Sobolev background; this directly proved abstract weak-form prerequisite does not claim compact-manifold classical regularity.
- Chen, Chewi, Lu and Zhang, PBPS Appendix C.1 — Actual conditional Poincare route requires further regularity/core and limiting arguments.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.