Documentation

TauCeti.Analysis.InnerProductSpace.QuadraticForm.Bounds

Quadratic-form bounds on subspaces #

Scalar-generic lower and upper bounds for the real part of the quadratic form of a bounded operator, restricted to a subspace. These predicates are useful well beyond Davis--Kahan perturbation theory.

Provenance #

Form-bound predicates extend the ContinuousLinearMap API and support dot notation on bounded operators.

source
def ContinuousLinearMap.LowerFormBoundOn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) (c : ℝ) :
Prop

Lower quadratic-form bound on a subspace.

Instances For
    source
    def ContinuousLinearMap.UpperFormBoundOn {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) (c : ℝ) :
    Prop

    Upper quadratic-form bound on a subspace.

    Instances For
      source
      theorem ContinuousLinearMap.lowerFormBoundOn_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) (c : ℝ) :
      A.LowerFormBoundOn U c ↔ ∀ x ∈ U, c * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x)

      The characteristic inequality defining a lower form bound.

      source
      theorem ContinuousLinearMap.upperFormBoundOn_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →L[𝕜] E) (U : Submodule 𝕜 E) (c : ℝ) :
      A.UpperFormBoundOn U c ↔ ∀ x ∈ U, RCLike.re (inner 𝕜 (A x) x) ≤ c * ‖x‖ ^ 2

      The characteristic inequality defining an upper form bound.

      Basic theory #

      The two ways a form bound weakens -- in the constant and in the subspace -- and the identification of the degenerate case with Mathlib's IsPositive. A consumer holding a bound on U at constant c and needing one on a subspace of U, or at a worse constant, should not have to reprove it from the definition.

      source
      theorem ContinuousLinearMap.LowerFormBoundOn.mono_const {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →L[𝕜] E} {U : Submodule 𝕜 E} {c c' : ℝ} (h : A.LowerFormBoundOn U c) (hc : c' ≤ c) :
      A.LowerFormBoundOn U c'

      A lower form bound weakens as the constant decreases.

      source
      theorem ContinuousLinearMap.LowerFormBoundOn.mono_subspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →L[𝕜] E} {U U' : Submodule 𝕜 E} {c : ℝ} (h : A.LowerFormBoundOn U c) (hU : U' ≤ U) :
      A.LowerFormBoundOn U' c

      A lower form bound restricts to a smaller subspace.

      source
      theorem ContinuousLinearMap.UpperFormBoundOn.mono_const {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →L[𝕜] E} {U : Submodule 𝕜 E} {c c' : ℝ} (h : A.UpperFormBoundOn U c) (hc : c ≤ c') :
      A.UpperFormBoundOn U c'

      An upper form bound weakens as the constant increases.

      source
      theorem ContinuousLinearMap.UpperFormBoundOn.mono_subspace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →L[𝕜] E} {U U' : Submodule 𝕜 E} {c : ℝ} (h : A.UpperFormBoundOn U c) (hU : U' ≤ U) :
      A.UpperFormBoundOn U' c

      An upper form bound restricts to a smaller subspace.

      source
      theorem ContinuousLinearMap.IsPositive.lowerFormBoundOn_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →L[𝕜] E} (hA : A.IsPositive) :
      A.LowerFormBoundOn ⊤ 0

      Positivity implies the zero lower form bound on the whole space.

      source
      theorem ContinuousLinearMap.isPositive_of_lowerFormBoundOn_top {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →L[𝕜] E} (hsym : (↑A).IsSymmetric) (h : A.LowerFormBoundOn ⊤ 0) :
      A.IsPositive

      The converse: symmetry plus the zero lower bound on ⊤ is positivity. Together with IsPositive.lowerFormBoundOn_top this pins LowerFormBoundOn _ ⊤ 0 as a generalization of Mathlib's predicate rather than a competitor to it.

      source
      @[simp]
      theorem ContinuousLinearMap.re_inner_algebraMap_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (c : ℝ) (x : E) :
      RCLike.re (inner 𝕜 (((algebraMap ℝ (E →L[𝕜] E)) c) x) x) = c * ‖x‖ ^ 2

      The real quadratic form of a real scalar operator is the scalar times the squared norm.