Mathlib.Analysis.Inner­Product­Space.Pos­Def

PosDef — Mathlib-shaped helpers: Sqrt.

Sqrt 6 core · 9 supporting This file constructs the positive square root of a positive operator on a finite-dimensional real inner-product space by diagonalizing the operator in an orthonormal eigenbasis. ★ posSqrt_mul_self★ posSqrtCLM_comp_self

Positive square roots of finite-dimensional positive operators

This file constructs the positive square root of a positive operator on a finite-dimensional real inner-product space by diagonalizing the operator in an orthonormal eigenbasis. The main linear-map construction is posSqrt, with posSqrt_mul_self, posSqrt_isSymmetric, and posSqrt_isPositive proving that it is the positive square root. The file also packages the same map as a continuous linear map posSqrtCLM, proves it is self-adjoint, and proves the corresponding continuous square law posSqrtCLM_comp_self.

def eigBasis reviewed
LinearMap.IsPositive

An orthonormal eigenbasis of T, obtained from the symmetry of a positive operator.

Definition (Lean source)
parameters
E :
Type u_1
E →ₗ[ℝ] E
shared
hT :
T.IsPositive
shared
def
eigBasis hT :
OrthonormalBasis (Fin (finrank ℝ E)) ℝ E
given by
hT.isSymmetric.eigenvectorBasis rfl
LinearMap.IsPositive.eigBasis · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:39
def eigVals reviewed
LinearMap.IsPositive

The real eigenvalues of T, indexed compatibly with eigBasis.

Definition (Lean source)
parameters
E :
Type u_1
E →ₗ[ℝ] E
shared
hT :
T.IsPositive
shared
def
eigVals hT :
Fin (finrank ℝ E) → ℝ
given by
hT.isSymmetric.eigenvalues rfl
LinearMap.IsPositive.eigVals · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:43
def posSqrt reviewed
LinearMap.IsPositive

The positive square root of T: the linear operator that acts as √(eigenvalue) on each vector of the chosen orthonormal eigenbasis.

Definition (Lean source)
parameters
E :
Type u_1
E →ₗ[ℝ] E
shared
hT :
T.IsPositive
shared
def
posSqrt hT :
E →ₗ[ℝ] E
given by
(hT.eigBasis).toBasis.constr ℝ (fun i => sqrt (hT.eigVals i) • hT.eigBasis i)
LinearMap.IsPositive.posSqrt · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:64
theorem posSqrt_mul_self reviewed
LinearMap.IsPositive

Composing the positive square root of T with itself recovers T.

Formal statement
hypotheses
E :
Type u_1
E →ₗ[ℝ] E
shared
hT :
T.IsPositive
shared
conclusion
hT.posSqrt ∘ₗ hT.posSqrt = T
Proof (Lean source)
theorem posSqrt_mul_self : hT.posSqrt ∘ₗ hT.posSqrt = T := by refine (hT.eigBasis).toBasis.ext fun i => ?_ simp only [OrthonormalBasis.coe_toBasis, coe_comp, Function.comp_apply, hT.posSqrt_apply_eigBasis i, map_smul, smul_smul, Real.mul_self_sqrt (hT.eigVals_nonneg i), hT.apply_eigBasis i]
LinearMap.IsPositive.posSqrt_mul_self · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:75 · uses posSqrt
def posSqrtCLM reviewed
LinearMap.IsPositive

posSqrt packaged as a continuous linear map (finite-dimensional domain).

Definition (Lean source)
parameters
E :
Type u_1
E →ₗ[ℝ] E
shared
hT :
T.IsPositive
shared
def
posSqrtCLM hT :
E →L[ℝ] E
given by
hT.posSqrt.toContinuousLinearMap
LinearMap.IsPositive.posSqrtCLM · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:114
theorem posSqrtCLM_comp_self reviewed
LinearMap.IsPositive

Composing the continuous positive square root of T with itself recovers T, packaged as a continuous linear map.

Formal statement
hypotheses
E :
Type u_1
E →ₗ[ℝ] E
shared
hT :
T.IsPositive
shared
conclusion
hT.posSqrtCLM ∘L hT.posSqrtCLM = T.toContinuousLinearMap
Proof (Lean source)
theorem posSqrtCLM_comp_self : hT.posSqrtCLM ∘L hT.posSqrtCLM = T.toContinuousLinearMap := by ext x change hT.posSqrt (hT.posSqrt x) = T x rw [← LinearMap.comp_apply, hT.posSqrt_mul_self]
LinearMap.IsPositive.posSqrtCLM_comp_self · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:132 · uses posSqrtCLM
9 supporting declarations (lemmas, instances)
  • apply_eigBasis theorem — Applying the operator to an eigenbasis vector scales that vector by its indexed eigenvalue.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    i :
    Fin (finrank ℝ E)
    conclusion
    T (hT.eigBasis i) = (hT.eigVals i) • hT.eigBasis i
    Proof (Lean source)
    theorem apply_eigBasis (i : Fin (finrank ℝ E)) : T (hT.eigBasis i) = (hT.eigVals i) • hT.eigBasis i := by simp only [eigBasis, eigVals] exact hT.isSymmetric.apply_eigenvectorBasis rfl i
    LinearMap.IsPositive.apply_eigBasis · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:47
  • eigVals_nonneg theorem — Eigenvalues of a positive operator are nonnegative.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    i :
    Fin (finrank ℝ E)
    conclusion
    0 ≤ hT.eigVals i
    Proof (Lean source)
    theorem eigVals_nonneg (i : Fin (finrank ℝ E)) : 0 ≤ hT.eigVals i := by have hb : ⟪hT.eigBasis i, hT.eigBasis i⟫ = 1 := by have := (hT.eigBasis).orthonormal.1 i rw [real_inner_self_eq_norm_sq, this]; norm_num have hpos := hT.2 (hT.eigBasis i) rw [hT.apply_eigBasis i, inner_smul_left] at hpos -- `hpos : 0 ≤ ⟪T (b i), b i⟫` becomes `0 ≤ μ i` simpa only [conj_trivial, hb, mul_one, RCLike.re_to_real] using hpos
    LinearMap.IsPositive.eigVals_nonneg · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:54
  • posSqrt_apply_eigBasis theorem — The positive square root sends each eigenbasis vector to the same vector scaled by the square root of its eigenvalue.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    i :
    Fin (finrank ℝ E)
    conclusion
    hT.posSqrt (hT.eigBasis i) = sqrt (hT.eigVals i) • hT.eigBasis i
    Proof (Lean source)
    theorem posSqrt_apply_eigBasis (i : Fin (finrank ℝ E)) : hT.posSqrt (hT.eigBasis i) = sqrt (hT.eigVals i) • hT.eigBasis i := by rw [posSqrt, ← OrthonormalBasis.coe_toBasis, Basis.constr_basis]
    LinearMap.IsPositive.posSqrt_apply_eigBasis · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:69
  • posSqrt_inner theorem — Inner-product form of posSqrt: a symmetric weighted sum over the eigenbasis.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    x y :
    E
    conclusion
    ⟪hT.posSqrt x, y⟫
    = ∑ i, sqrt (hT.eigVals i) * ⟪hT.eigBasis i, x⟫ * ⟪hT.eigBasis i, y⟫
    Proof (Lean source)
    theorem posSqrt_inner (x y : E) : ⟪hT.posSqrt x, y⟫ = ∑ i, sqrt (hT.eigVals i) * ⟪hT.eigBasis i, x⟫ * ⟪hT.eigBasis i, y⟫ := by have hx : hT.posSqrt x = ∑ i, (⟪hT.eigBasis i, x⟫ * sqrt (hT.eigVals i)) • hT.eigBasis i := by conv_lhs => rw [← (hT.eigBasis).sum_repr x] rw [map_sum] refine Finset.sum_congr rfl fun i _ => ?_ rw [map_smul, hT.posSqrt_apply_eigBasis i, smul_smul, OrthonormalBasis.repr_apply_apply] rw [hx, sum_inner] refine Finset.sum_congr rfl fun i _ => ?_ rw [inner_smul_left, conj_trivial] ring
    LinearMap.IsPositive.posSqrt_inner · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:82
  • posSqrt_isSymmetric theorem — posSqrt is symmetric.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    conclusion
    hT.posSqrt.IsSymmetric
    Proof (Lean source)
    theorem posSqrt_isSymmetric : hT.posSqrt.IsSymmetric := fun x y => by rw [hT.posSqrt_inner x y, show ⟪x, hT.posSqrt y⟫ = ⟪hT.posSqrt y, x⟫ from real_inner_comm _ _, hT.posSqrt_inner y x] exact Finset.sum_congr rfl fun i _ => by ring
    LinearMap.IsPositive.posSqrt_isSymmetric · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:98
  • posSqrt_isPositive theorem — posSqrt is itself a positive operator.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    conclusion
    hT.posSqrt.IsPositive
    Proof (Lean source)
    theorem posSqrt_isPositive : hT.posSqrt.IsPositive := by refine (LinearMap.isPositive_iff _).mpr ⟨hT.posSqrt_isSymmetric, fun x => ?_⟩ rw [hT.posSqrt_inner x x] refine Finset.sum_nonneg fun i _ => ?_ nlinarith [Real.sqrt_nonneg (hT.eigVals i), mul_self_nonneg ⟪hT.eigBasis i, x⟫]
    LinearMap.IsPositive.posSqrt_isPositive · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:105
  • posSqrtCLM_apply theorem — The continuous-linear-map packaging of the positive square root has the same pointwise action as the linear-map square root.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    x :
    E
    conclusion
    hT.posSqrtCLM x = hT.posSqrt x
    Proof (Lean source)
    @[simp] theorem posSqrtCLM_apply (x : E) : hT.posSqrtCLM x = hT.posSqrt x := rfl
    LinearMap.IsPositive.posSqrtCLM_apply · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:117
  • posSqrtCLM_isSelfAdjoint theorem — The continuous square root is self-adjoint.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    conclusion
    IsSelfAdjoint hT.posSqrtCLM
    Proof (Lean source)
    theorem posSqrtCLM_isSelfAdjoint : IsSelfAdjoint hT.posSqrtCLM := (LinearMap.isSelfAdjoint_toContinuousLinearMap_iff _).mpr ((LinearMap.isSymmetric_iff_isSelfAdjoint _).mp hT.posSqrt_isSymmetric)
    LinearMap.IsPositive.posSqrtCLM_isSelfAdjoint · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:122
  • posSqrtCLM_adjoint theorem — Adjoint form of self-adjointness.
    hypotheses
    E :
    Type u_1
    E →ₗ[ℝ] E
    shared
    hT :
    T.IsPositive
    shared
    conclusion
    adjoint hT.posSqrtCLM = hT.posSqrtCLM
    Proof (Lean source)
    theorem posSqrtCLM_adjoint : adjoint hT.posSqrtCLM = hT.posSqrtCLM := by rw [← ContinuousLinearMap.star_eq_adjoint]; exact hT.posSqrtCLM_isSelfAdjoint
    LinearMap.IsPositive.posSqrtCLM_adjoint · Causalean/Mathlib/Analysis/InnerProductSpace/PosDef/Sqrt.lean:127