Coercive bounded operators

A uniformly coercive real part of the quadratic form makes a bounded operator on a real or complex Hilbert space invertible. Self-adjointness is not needed. The inverse follows from Mathlib’s operator invertibility criterion for a uniform lower bound on the norm of the quadratic form. For complex operators the same argument applied to a scalar shift bounds the real part of every spectral value below by the coercivity constant.

These facts supply the invertibility and spectral half-plane steps in Lyapunov arguments comparing positive spectral subspaces.

For an operator on a real inner product space, the quadratic form ⟪T v, v⟫ is bounded by ‖T‖ ‖v‖² (ContinuousLinearMap.abs_inner_apply_le), and the form ⟪S (A v), v⟫ of S against A by ‖S‖ ‖A‖ ‖v‖² (ContinuousLinearMap.abs_inner_apply_apply_le). Two consequences bound the change of this form under a perturbation of A (ContinuousLinearMap.inner_apply_apply_sub_le) and bound below the form ⟪S (A v), v⟫ - ½ ⟪D v, v⟫ that appears when integrating against a family of quadratic forms (ContinuousLinearMap.neg_mul_norm_sq_le_inner_sub).

In a real inner product space we also record the quadratic perturbation estimates for a coercive symmetric operator A: the increment of F - ⟪·, y + A z⟫ is that of a quadratic centred at x + z up to the second-order error of F (LinearMap.IsSymmetric.increment_sub_quadratic_eq), and a coercive quadratic of this form dominates its perturbation on a sphere (LinearMap.lt_on_sphere_of_abs_increment_le).

A real coercive quadratic form also loses at most the size of a perturbation of the operator (sub_norm_mul_norm_sq_le_inner) and stays nonnegative under a small perturbation and scalar shift (inner_add_smul_id_nonneg_of_norm_sub_le), which gives the convexity of perturbed barrier functions, for instance in the Monge–Ampère viscosity argument.

Provenance

Adapted from ForTauCeti/Analysis/InnerProductSpace/CoerciveUnit.lean (Jon Crall and Claude Fable 5) and DavisKahan/InfiniteDimensional/TanTwoTheta/QuarterAcuteFormGap.lean (Jon Crall, OpenAI GPT-5.6 Thinking, Claude Opus 5), in the Kitware DKPS formalization, Apache-2.0, copyright 2026 Kitware, Inc. The invertibility proof here applies Mathlib's ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map directly.

theorem ContinuousLinearMap.mul_norm_le_norm_apply_of_coercive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (N : E →L[𝕜] E) {c : ℝ} (hcoer : ∀ (z : E), c * ‖z‖ ^ 2 ≤ RCLike.re (inner 𝕜 (N z) z)) (z : E) : c * ‖z‖ ≤ ‖N z‖

A quadratic-form lower bound yields the corresponding norm lower bound.

theorem ContinuousLinearMap.isUnit_of_coercive {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (N : E →L[𝕜] E) {c : ℝ} (hc : 0 < c) (hcoer : ∀ (z : E), c * ‖z‖ ^ 2 ≤ RCLike.re (inner 𝕜 (N z) z)) : IsUnit N

A bounded operator with a uniformly coercive real quadratic form is a unit.

theorem ContinuousLinearMap.conj_add_star_of_lyapunov {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B C W R Rinv : E →L[𝕜] E) (hR : IsSelfAdjoint R) (hRinv : IsSelfAdjoint Rinv) (hRR : R * R = C) (hRinvR : Rinv * R = 1) (hRRinv : R * Rinv = 1) (hlyap : C * W + star W * C = B + B) : R * W * Rinv + star (R * W * Rinv) = Rinv * B * Rinv + Rinv * B * Rinv

Conjugating a Lyapunov identity by an inverse self-adjoint square root gives the Hermitian part of the similar operator.

theorem ContinuousLinearMap.coercive_conj_of_lyapunov {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (B C W R Rinv : E →L[𝕜] E) (hR : IsSelfAdjoint R) (hRinv : IsSelfAdjoint Rinv) (hRR : R * R = C) (hRinvR : Rinv * R = 1) (hRRinv : R * Rinv = 1) (hlyap : C * W + star W * C = B + B) {δ : ℝ} (hδ : 0 ≤ δ) (hBcoer : B.LowerFormBoundOn ⊤ δ) (x : E) : δ / (1 + ‖R‖ ^ 2) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 ((R * W * Rinv) x) x)

If C = R², Rinv is the two-sided inverse of the self-adjoint R, and C W + W† C = 2 B, a quadratic-form lower bound δ for B gives the lower bound δ / (1 + ‖R‖²) for R W Rinv. No positivity of R or nontriviality of the space is required, and δ = 0 is allowed.

theorem ContinuousLinearMap.abs_inner_apply_le {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (T : F →L[ℝ] F) (v : F) : |inner ℝ (T v) v| ≤ ‖T‖ * ‖v‖ ^ 2

The quadratic form of a bounded operator T is bounded by ‖T‖ ‖v‖².

theorem ContinuousLinearMap.abs_inner_apply_apply_le {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S A : F →L[ℝ] F) (v : F) : |inner ℝ (S (A v)) v| ≤ ‖S‖ * ‖A‖ * ‖v‖ ^ 2

The quadratic form of S against A is bounded by ‖S‖ ‖A‖ ‖v‖².

theorem ContinuousLinearMap.inner_apply_apply_sub_le {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S A B : F →L[ℝ] F) (v : F) : inner ℝ (S (A v)) v - inner ℝ (S (B v)) v ≤ ‖S‖ * ‖B - A‖ * ‖v‖ ^ 2

The quadratic form of S against B differs from that against A by at most ‖S‖ ‖B - A‖ ‖v‖².

theorem ContinuousLinearMap.neg_mul_norm_sq_le_inner_sub {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (S A D : F →L[ℝ] F) (v : F) : -((‖S‖ * ‖A‖ + ‖D‖ / 2) * ‖v‖ ^ 2) ≤ inner ℝ (S (A v)) v - inner ℝ (D v) v / 2

The quadratic form ⟪S (A v), v⟫ - ½ ⟪D v, v⟫ is at least -(‖S‖ ‖A‖ + ‖D‖ / 2) ‖v‖².

theorem ContinuousLinearMap.le_re_of_mem_spectrum_of_coercive {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (N : E →L[ℂ] E) {c : ℝ} (hcoer : ∀ (x : E), c * ‖x‖ ^ 2 ≤ (inner ℂ (N x) x).re) {z : ℂ} (hz : z ∈ spectrum ℂ N) : c ≤ z.re

A uniform lower bound for the real quadratic form bounds real parts of spectral values below.

theorem ContinuousLinearMap.le_re_of_mem_spectrum_of_positive_lyapunov {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (B C W : E →L[ℂ] E) (hC : IsStrictlyPositive C) (hlyap : C * W + star W * C = B + B) {δ : ℝ} (hδ : 0 ≤ δ) (hB : B.LowerFormBoundOn ⊤ δ) {z : ℂ} (hz : z ∈ spectrum ℂ W) : δ / (1 + ‖C ^ (1 / 2)‖ ^ 2) ≤ z.re

A positive invertible Lyapunov weight transports a coercive form bound to a spectral half-plane bound, with the square-root similarity made explicit in the constant.

theorem ContinuousLinearMap.sub_norm_mul_norm_sq_le_inner {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A : F →L[ℝ] F} {κ : ℝ} (hA : ∀ (v : F), κ * ‖v‖ ^ 2 ≤ inner ℝ (A v) v) (D : F →L[ℝ] F) (v : F) : (κ - ‖D - A‖) * ‖v‖ ^ 2 ≤ inner ℝ (D v) v

A coercive quadratic form loses at most the size of the perturbation. If κ ‖v‖² ≤ ⟪A v, v⟫, then (κ - ‖D - A‖) ‖v‖² ≤ ⟪D v, v⟫.

theorem ContinuousLinearMap.inner_add_smul_id_nonneg_of_norm_sub_le {F : Type u_4} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {A D : F →L[ℝ] F} {κ t : ℝ} (hA : ∀ (v : F), κ * ‖v‖ ^ 2 ≤ inner ℝ (A v) v) (hD : ‖D - A‖ ≤ κ + t) (v : F) : 0 ≤ inner ℝ ((D + t • ContinuousLinearMap.id ℝ F) v) v

The quadratic form stays nonnegative under small perturbations. If κ ‖v‖² ≤ ⟪A v, v⟫ and ‖D - A‖ ≤ κ + t, then 0 ≤ ⟪(D + t • id) v, v⟫.

theorem LinearMap.IsSymmetric.increment_sub_quadratic_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →ₗ[ℝ] E} (hA : A.IsSymmetric) {x x' y z : E} {a b : ℝ} : a - inner ℝ x' (y + A z) - (b - inner ℝ x (y + A z)) - (inner ℝ (A (x' - x - z)) (x' - x - z) / 2 - inner ℝ (A z) z / 2) = a - b - inner ℝ y (x' - x) - inner ℝ (A (x' - x)) (x' - x) / 2

The increment of g = F - ⟪·, p⟫ for p = y + A z from x to x' is ⟪A (x' - x - z), x' - x - z⟫ / 2 - ⟪A z, z⟫ / 2, up to the error of the second-order expansion of F at x with gradient y and Hessian A: for symmetric A, the difference of the two is exactly that error, where F x' = a and F x = b.

theorem LinearMap.lt_on_sphere_of_abs_increment_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {A : E →ₗ[ℝ] E} {g : E → ℝ} {x z : E} {r s c δ : ℝ} (hc : 0 < c) (hcA : ∀ (w : E), c * ‖w‖ ^ 2 ≤ inner ℝ (A w) w) (hs : s < 1) (hr : 0 < r) (hδ : δ ≤ c * (1 - s) ^ 2 / 8) (hz : ‖z‖ ≤ s * r) (hincr : ∀ x' ∈ Metric.closedBall x r, |g x' - g x - (inner ℝ (A (x' - x - z)) (x' - x - z) / 2 - inner ℝ (A z) z / 2)| ≤ δ * ‖x' - x‖ ^ 2) (x' : E) : x' ∈ Metric.sphere x r → g (x + z) < g x'

If g has, on closedBall x r, the increment from x of a quadratic centred at x + z, up to δ ‖x' - x‖ ^ 2 with δ small relative to the coercivity constant c of A and ‖z‖ ≤ s * r for s < 1, then g on the sphere exceeds g (x + z).