Sharp quadratic corrector bound on a real Hilbert space
AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorBound.quadratic_corrector_bound_of_square_identity · theorem · Teaching coverage
Mathematical statement
Let H be any complete real inner-product space, including the zero space. Let K,D:H→H be bounded real-linear selfadjoint operators with I+K²=D². Let c≥0 and ‖D‖≤c. Then for every u,v∈H, |(‖u‖²−‖v‖²)/2−⟨Ku,v⟩|≤(c/2)(‖u‖²+‖v‖²). No finite-dimensionality, nontriviality, c≥1, positivity of K or D, or commutation is assumed. This ASTIS auxiliary Hilbert-space lemma supplies the sharp two-component estimate in the PBPS B23 proof; its actual consumer internally produces K,D,c and all hypotheses.
Lean statement · quadratic_corrector_bound_of_square_identity
Let H be any complete real inner-product space, including the zero space. Let K,D:H→H be bounded real-linear selfadjoint operators with I+K²=D². Let c≥0 and ‖D‖≤c. Then for every u,v∈H, |(‖u‖²−‖v‖²)/2−⟨Ku,v⟩|≤(c/2)(‖u‖²+‖v‖²). No finite-dimensionality, nontriviality, c≥1, positivity of K or D, or commutation is assumed. This ASTIS auxiliary Hilbert-space lemma supplies the sharp two-component estimate in the PBPS B23 proof; its actual consumer internally produces K,D,c and all hypotheses.
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 quadratic_corrector_bound_of_square_identity
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
(K D : H →L[ℝ] H) (hK : IsSelfAdjoint K) (hD : IsSelfAdjoint D)
(hSquare : (1 : H →L[ℝ] H)+K*K=D*D)
(c : ℝ) (hc : 0 ≤ c) (hNorm : ‖D‖ ≤ c) (u v : H) :
|(1/2 : ℝ)*(‖u‖^2-‖v‖^2)-inner ℝ (K u) v| ≤
(c/2)*(‖u‖^2+‖v‖^2)Proof roadmap
- 1Turn the operator square into a norm identity
Evaluate I+K²=D² against x. Selfadjointness moves the outer K and D across the inner product.
- 2Cancel the two block cross terms
Use the sum of the two squared component norms. Symmetry cancels the mixed terms; this is the Hilbert sum energy, without a product max-norm assertion.
- 3Bound the quadratic form and block energy
Set S=‖u‖²+‖v‖² and T=‖u-Kv‖²+‖Ku+v‖²=‖Du‖²+‖Dv‖² throughout this five-step proof. Triangle inequality and the inner-product bound control E. The operator norm controls each D component.
- 4Apply two-component Cauchy-Schwarz
The scalar inequality follows from a single nonnegative square. Combine with the block energy bound, keeping S nonnegative.
- 5Take the nonnegative square root and divide by two
Both |E| and cS are nonnegative, so their square inequality gives |E|≤cS. The corrector is E/2.
Full assumptions and notation
All objects and hypotheses
- Complete real inner-product space H; bounded selfadjoint real operators K,D; I+K²=D²; c≥0 and ‖D‖≤c. Zero H is legal.
Mathematical proof
1. Turn the operator square into a norm identity
Evaluate I+K²=D² against x. Selfadjointness moves the outer K and D across the inner product.
Corresponding Lean step
have hEnergy (x : H) : ‖x‖^2+‖K x‖^2=‖D x‖^2 := by
have h := congrArg (fun A : H →L[ℝ] H => inner ℝ (A x) x) hSquare
simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.one_apply,
ContinuousLinearMap.mul_apply, inner_add_left] at h
have hk : inner ℝ (K (K x)) x=inner ℝ (K x) (K x) :=
hK.isSymmetric (K x) x
have hd : inner ℝ (D (D x)) x=inner ℝ (D x) (D x) :=
hD.isSymmetric (D x) x
rw [hk, hd] at h
simpa only [real_inner_self_eq_norm_sq] using h
Literal compiled BODY span; exact preceding locals remain in scope.
2. Cancel the two block cross terms
Use the sum of the two squared component norms. Symmetry cancels the mixed terms; this is the Hilbert sum energy, without a product max-norm assertion.
Corresponding Lean step
have hSym : inner ℝ u (K v)=inner ℝ (K u) v :=
(hK.isSymmetric u v).symm
have hBlock : ‖u-K v‖^2+‖K u+v‖^2=‖D u‖^2+‖D v‖^2 := by
rw [norm_sub_sq_real, norm_add_sq_real, hSym]
nlinarith only [hEnergy u, hEnergy v]
have hForm : inner ℝ (u-K v) u-inner ℝ (K u+v) v =
‖u‖^2-‖v‖^2-2*inner ℝ (K u) v := by
have hSwap : inner ℝ (K v) u=inner ℝ (K u) v :=
(hK.isSymmetric v u).trans (real_inner_comm v (K u)).symm
rw [inner_sub_left, inner_add_left, hSwap, real_inner_self_eq_norm_sq,
real_inner_self_eq_norm_sq]
ring
Literal compiled BODY span; exact preceding locals remain in scope.
3. Bound the quadratic form and block energy
Set S=‖u‖²+‖v‖² and T=‖u-Kv‖²+‖Ku+v‖²=‖Du‖²+‖Dv‖² throughout this five-step proof. Triangle inequality and the inner-product bound control E. The operator norm controls each D component.
Corresponding Lean step
have hAbs : |‖u‖^2-‖v‖^2-2*inner ℝ (K u) v| ≤
‖u-K v‖*‖u‖+‖K u+v‖*‖v‖ := by
rw [← hForm]
exact (abs_sub _ _).trans (add_le_add
(abs_real_inner_le_norm _ _) (abs_real_inner_le_norm _ _))
have hDx (x : H) : ‖D x‖^2 ≤ c^2*‖x‖^2 := by
have hb : ‖D x‖ ≤ c*‖x‖ :=
(D.le_opNorm x).trans (mul_le_mul_of_nonneg_right hNorm (norm_nonneg x))
have hs := (sq_le_sq₀ (norm_nonneg (D x)) (mul_nonneg hc (norm_nonneg x))).2 hb
nlinarith only [hs]
have hBlockBound : ‖u-K v‖^2+‖K u+v‖^2 ≤ c^2*(‖u‖^2+‖v‖^2) := by
rw [hBlock]
nlinarith only [hDx u, hDx v]
Literal compiled BODY span; exact preceding locals remain in scope.
4. Apply two-component Cauchy-Schwarz
The scalar inequality follows from a single nonnegative square. Combine with the block energy bound, keeping S nonnegative.
Corresponding Lean step
have hCS : (‖u-K v‖*‖u‖+‖K u+v‖*‖v‖)^2 ≤
(‖u‖^2+‖v‖^2)*(‖u-K v‖^2+‖K u+v‖^2) := by
nlinarith only [sq_nonneg (‖u-K v‖*‖v‖-‖K u+v‖*‖u‖)]
have hSquared : |‖u‖^2-‖v‖^2-2*inner ℝ (K u) v|^2 ≤
(c*(‖u‖^2+‖v‖^2))^2 := by
calc
_ ≤ (‖u-K v‖*‖u‖+‖K u+v‖*‖v‖)^2 :=
(sq_le_sq₀ (abs_nonneg _) (by positivity)).2 hAbs
_ ≤ (‖u‖^2+‖v‖^2)*(‖u-K v‖^2+‖K u+v‖^2) := hCS
_ ≤ (‖u‖^2+‖v‖^2)*(c^2*(‖u‖^2+‖v‖^2)) :=
mul_le_mul_of_nonneg_left hBlockBound (by positivity)
_ = _ := by ring
Literal compiled BODY span; exact preceding locals remain in scope.
5. Take the nonnegative square root and divide by two
Both |E| and cS are nonnegative, so their square inequality gives |E|≤cS. The corrector is E/2.
Corresponding Lean step
have hBound := (sq_le_sq₀ (abs_nonneg
(‖u‖^2-‖v‖^2-2*inner ℝ (K u) v)) (by positivity)).1 hSquared
have hHalf : (1/2 : ℝ)*(‖u‖^2-‖v‖^2)-inner ℝ (K u) v =
(1/2 : ℝ)*(‖u‖^2-‖v‖^2-2*inner ℝ (K u) v) := by ring
rw [hHalf, abs_mul, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1/2)]
nlinarith only [hBound]
Literal compiled BODY span; exact preceding locals remain in scope.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · quadratic_corrector_bound_of_square_identity
Turn the operator square into a norm identity; Cancel the two block cross terms; Bound the quadratic form and block energy; Apply two-component Cauchy-Schwarz; Take the nonnegative square root and divide by two
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 quadratic_corrector_bound_of_square_identity
{H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H]
(K D : H →L[ℝ] H) (hK : IsSelfAdjoint K) (hD : IsSelfAdjoint D)
(hSquare : (1 : H →L[ℝ] H)+K*K=D*D)
(c : ℝ) (hc : 0 ≤ c) (hNorm : ‖D‖ ≤ c) (u v : H) :
|(1/2 : ℝ)*(‖u‖^2-‖v‖^2)-inner ℝ (K u) v| ≤
(c/2)*(‖u‖^2+‖v‖^2)
:= by
have hEnergy (x : H) : ‖x‖^2+‖K x‖^2=‖D x‖^2 := by
have h := congrArg (fun A : H →L[ℝ] H => inner ℝ (A x) x) hSquare
simp only [ContinuousLinearMap.add_apply, ContinuousLinearMap.one_apply,
ContinuousLinearMap.mul_apply, inner_add_left] at h
have hk : inner ℝ (K (K x)) x=inner ℝ (K x) (K x) :=
hK.isSymmetric (K x) x
have hd : inner ℝ (D (D x)) x=inner ℝ (D x) (D x) :=
hD.isSymmetric (D x) x
rw [hk, hd] at h
simpa only [real_inner_self_eq_norm_sq] using h
have hSym : inner ℝ u (K v)=inner ℝ (K u) v :=
(hK.isSymmetric u v).symm
have hBlock : ‖u-K v‖^2+‖K u+v‖^2=‖D u‖^2+‖D v‖^2 := by
rw [norm_sub_sq_real, norm_add_sq_real, hSym]
nlinarith only [hEnergy u, hEnergy v]
have hForm : inner ℝ (u-K v) u-inner ℝ (K u+v) v =
‖u‖^2-‖v‖^2-2*inner ℝ (K u) v := by
have hSwap : inner ℝ (K v) u=inner ℝ (K u) v :=
(hK.isSymmetric v u).trans (real_inner_comm v (K u)).symm
rw [inner_sub_left, inner_add_left, hSwap, real_inner_self_eq_norm_sq,
real_inner_self_eq_norm_sq]
ring
have hAbs : |‖u‖^2-‖v‖^2-2*inner ℝ (K u) v| ≤
‖u-K v‖*‖u‖+‖K u+v‖*‖v‖ := by
rw [← hForm]
exact (abs_sub _ _).trans (add_le_add
(abs_real_inner_le_norm _ _) (abs_real_inner_le_norm _ _))
have hDx (x : H) : ‖D x‖^2 ≤ c^2*‖x‖^2 := by
have hb : ‖D x‖ ≤ c*‖x‖ :=
(D.le_opNorm x).trans (mul_le_mul_of_nonneg_right hNorm (norm_nonneg x))
have hs := (sq_le_sq₀ (norm_nonneg (D x)) (mul_nonneg hc (norm_nonneg x))).2 hb
nlinarith only [hs]
have hBlockBound : ‖u-K v‖^2+‖K u+v‖^2 ≤ c^2*(‖u‖^2+‖v‖^2) := by
rw [hBlock]
nlinarith only [hDx u, hDx v]
have hCS : (‖u-K v‖*‖u‖+‖K u+v‖*‖v‖)^2 ≤
(‖u‖^2+‖v‖^2)*(‖u-K v‖^2+‖K u+v‖^2) := by
nlinarith only [sq_nonneg (‖u-K v‖*‖v‖-‖K u+v‖*‖u‖)]
have hSquared : |‖u‖^2-‖v‖^2-2*inner ℝ (K u) v|^2 ≤
(c*(‖u‖^2+‖v‖^2))^2 := by
calc
_ ≤ (‖u-K v‖*‖u‖+‖K u+v‖*‖v‖)^2 :=
(sq_le_sq₀ (abs_nonneg _) (by positivity)).2 hAbs
_ ≤ (‖u‖^2+‖v‖^2)*(‖u-K v‖^2+‖K u+v‖^2) := hCS
_ ≤ (‖u‖^2+‖v‖^2)*(c^2*(‖u‖^2+‖v‖^2)) :=
mul_le_mul_of_nonneg_left hBlockBound (by positivity)
_ = _ := by ring
have hBound := (sq_le_sq₀ (abs_nonneg
(‖u‖^2-‖v‖^2-2*inner ℝ (K u) v)) (by positivity)).1 hSquared
have hHalf : (1/2 : ℝ)*(‖u‖^2-‖v‖^2)-inner ℝ (K u) v =
(1/2 : ℝ)*(‖u‖^2-‖v‖^2-2*inner ℝ (K u) v) := by ring
rw [hHalf, abs_mul, abs_of_nonneg (by norm_num : (0 : ℝ) ≤ 1/2)]
nlinarith only [hBound]
end
end AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorBound
#print axioms AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorBound.quadratic_corrector_bound_of_square_identityScope and omitted-condition boundaries
- ASTIS sharp quadratic-form auxiliary on an arbitrary complete real Hilbert space; explicit selfadjoint square identity and norm bound. Actual PBPS inputs and these internal hypotheses are supplied by the actual production consumer. No full dynamics, mixing or cost result.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- IsSelfAdjoint.isSymmetric
- norm_add_sq_real
- norm_sub_sq_real
- abs_real_inner_le_norm
- ContinuousLinearMap.le_opNorm
- sq_le_sq₀
Mathematical sources
- PBPS2609.06905v1 AppendixB3 LemmaB.3 and B19/B20/B22/B23/B24; exact sharp two-component Hilbert energy bound and actual centered PBPS consumer. — ASTIS sharp quadratic-form auxiliary on an arbitrary complete real Hilbert space; explicit selfadjoint square identity and norm bound. Actual PBPS inputs and these internal hypotheses are supplied by the actual production consumer. No full dynamics, mixing or cost result.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.