Davis--Kahan 1970: the four Section 2 theorems

The namespace is RotationOfEigenvectors, after the paper's title. Everything below is ordinary Mathlib vocabulary; the only non-Mathlib names are the source objects defined here.

Two conventions, stated once. There is no functional calculus anywhere: a unitarily invariant norm sees only the singular-value sequence, so every angle quantity is either an explicit block of orthogonal projections or a sequence of trigonometric functions of singular values. And ‖tan Θ‖ is evaluated on the tangent sequence, with each tangent theorem concluding that the tangent has no pole rather than assuming it away.

1. Singular values

noncomputable def RotationOfEigenvectors.singularValue {𝕜 : Type u} [NontriviallyNormedField 𝕜] {E : Type v} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type w} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : ℝ

The n-th singular value of a bounded operator, zero-based: the operator-norm distance from T to the operators of rank at most n. a₀ T = ‖T‖, and for a compact operator this is the usual decreasing sequence.

Equations

• RotationOfEigenvectors.singularValue T n = ⨅ (R : { R : E →L[𝕜] F // (↑R).rank ≤ ↑n }), ‖T - ↑R‖

2. The symmetric-norming presentation of the source norm quantifier

The paper quantifies over arbitrary normalized unitarily invariant norms. This Challenge uses the canonical dimension-coherent symmetric-norming presentation: a two-sided unitarily invariant seminorm on n × n complex matrices in every dimension, normalized on rank one and unchanged by appending a zero singular value, extended to operators through approximation singular values.

This Lean type is not literally the entire source norm class in infinite dimension. The included formalization proves, via the strong Fan-dominance criterion used by Davis and Kahan, that the inequalities quantified over all such symmetric norming functions are equivalent to the corresponding universal unitarily invariant norm estimates. In particular the formal development also covers Fan-dominant norms not generated by a symmetric gauge. The distinction is recorded explicitly in formalization.yaml; it is a presentation choice, not a claim that the two norm types are definitionally identical.

noncomputable def RotationOfEigenvectors.diagOp {n : ℕ} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (b : OrthonormalBasis (Fin n) ℂ E) (x : Fin n → ℝ) : E →ₗ[ℂ] E

The operator with real diagonal x in an orthonormal basis.

Equations

• RotationOfEigenvectors.diagOp b x = ∑ i : Fin n, ↑(x i) • ↑(((InnerProductSpace.rankOne ℂ) (b i)) (b i))

structure RotationOfEigenvectors.UISeminorm (E : Type v) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] : Type v

A two-sided unitarily invariant seminorm on the operators of a finite-dimensional complex inner product space.

• toFun : (E →ₗ[ℂ] E) → ℝ

  The underlying function on operators.

• add_le (A B : E →ₗ[ℂ] E) : self.toFun (A + B) ≤ self.toFun A + self.toFun B

  Subadditivity.

• smul (a : ℂ) (A : E →ₗ[ℂ] E) : self.toFun (a • A) = ‖a‖ * self.toFun A

  Absolute homogeneity.

• invariant (U V : E ≃ₗᵢ[ℂ] E) (A : E →ₗ[ℂ] E) : self.toFun (↑U.toLinearEquiv ∘ₗ A ∘ₗ ↑V.toLinearEquiv) = self.toFun A

  Two-sided unitary invariance -- the defining property.

noncomputable def RotationOfEigenvectors.UISeminorm.gauge {n : ℕ} {E : Type v} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (N : UISeminorm E) (b : OrthonormalBasis (Fin n) ℂ E) (x : Fin n → ℝ) : ℝ

The symmetric gauge: the seminorm's value on the diagonal operator.

Equations

• N.gauge b x = N.toFun (RotationOfEigenvectors.diagOp b x)

def RotationOfEigenvectors.zeroPad {n : ℕ} (x : Fin n → ℝ) : Fin (n + 1) → ℝ

Append one trailing zero to a finite vector of singular values.

Equations

• RotationOfEigenvectors.zeroPad x i = Fin.lastCases 0 x i

structure RotationOfEigenvectors.SymmetricNormingFunction : Type

A dimension-coherent normalized symmetric norming function.

This is the Challenge's canonical presentation of the source norm quantifier. The source's broader unitary-invariant-norm class is related to it by the formalized Fan-dominance equivalence described above.

• finiteNorm (n : ℕ) : UISeminorm (EuclideanSpace ℂ (Fin n))

  A unitarily invariant seminorm in each finite dimension.

• normalized : ((self.finiteNorm 1).gauge (EuclideanSpace.basisFun (Fin 1) ℂ) fun (x : Fin 1) => 1) = 1

  Normalisation on a single unit singular value.

• zero_pad {n : ℕ} (x : Fin n → ℝ) : (self.finiteNorm (n + 1)).gauge (EuclideanSpace.basisFun (Fin (n + 1)) ℂ) (zeroPad x) = (self.finiteNorm n).gauge (EuclideanSpace.basisFun (Fin n) ℂ) x

  Appending a zero singular value does not change the value.

noncomputable def RotationOfEigenvectors.SymmetricNormingFunction.evalSeq (N : SymmetricNormingFunction) (s : ℕ → ℝ) : ENNReal

The extended symmetric-norming value of a scalar sequence: the supremum over its finite prefixes. A norm of tan Θ is evaluated on the sequence tan θ₁, tan θ₂, ….

Equations

• N.evalSeq s = ⨆ (n : ℕ), ENNReal.ofReal ((N.finiteNorm n).gauge (EuclideanSpace.basisFun (Fin n) ℂ) fun (i : Fin n) => s ↑i)

def RotationOfEigenvectors.SymmetricNormingFunction.SeqFinite (N : SymmetricNormingFunction) (s : ℕ → ℝ) : Prop

The sequence lies in the norm's ideal.

Equations

• N.SeqFinite s = (N.evalSeq s ≠ ⊤)

noncomputable def RotationOfEigenvectors.SymmetricNormingFunction.seqNorm (N : SymmetricNormingFunction) (s : ℕ → ℝ) : ℝ

The real-valued norm of a sequence, meaningful on the ideal.

Equations

• N.seqNorm s = (N.evalSeq s).toReal

noncomputable def RotationOfEigenvectors.SymmetricNormingFunction.eval {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : SymmetricNormingFunction) (T : E →L[𝕜] F) : ENNReal

The symmetric-norming extended value on an operator: its value on the singular-value sequence, and ⊤ exactly off the associated ideal.

Equations

• N.eval T = N.evalSeq fun (n : ℕ) => RotationOfEigenvectors.singularValue T n

def RotationOfEigenvectors.SymmetricNormingFunction.Finite {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : SymmetricNormingFunction) (T : E →L[𝕜] F) : Prop

The operator lies in the norm's ideal.

Equations

• N.Finite T = (N.eval T ≠ ⊤)

noncomputable def RotationOfEigenvectors.SymmetricNormingFunction.norm {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : SymmetricNormingFunction) (T : E →L[𝕜] F) : ℝ

The real-valued norm, meaningful on the ideal.

Equations

• N.norm T = (N.eval T).toReal

theorem RotationOfEigenvectors.instCompleteSpaceOfHasOrthogonalProjection {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (W : Submodule 𝕜 E) [W.HasOrthogonalProjection] : CompleteSpace ↥W

A subspace with an orthogonal projection is closed, hence complete.

3. The paper's block data

Section 1 fixes a self-adjoint A, a bounded self-adjoint perturbation H, and two reducing decompositions: E₀ spans the trial subspace with block A₀, and F₀, F₁ span the exact subspaces of A + H with complementary block Λ₁. The residual is R = (A + H) E₀ − E₀ A₀. Neither decomposition is assumed spectral.

def RotationOfEigenvectors.IsIsometric {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) : Prop

A coordinate map is an isometry onto its range.

Equations

• RotationOfEigenvectors.IsIsometric T = ∀ (x : E), ‖T x‖ = ‖x‖

structure RotationOfEigenvectors.IsTrialResidual {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (A₀ : F →ₗ.[𝕜] F) (E₀ R : F →L[𝕜] E) : Prop

The trial-coordinate half of the setup: E₀ is an isometric coordinate map for the trial subspace and R the residual A E₀ − E₀ A₀; A₀ is a partial map, so it may be unbounded.

• isometry : IsIsometric E₀

  The trial coordinate map is isometric.

• mapsDomain (x : ↥A₀.domain) : E₀ ↑x ∈ A.domain

  It carries the trial domain into the ambient domain.

• residualEquation (x : ↥A₀.domain) : ↑A ⟨E₀ ↑x, ⋯⟩ - E₀ (↑A₀ x) = R ↑x

  R is the residual there.

structure RotationOfEigenvectors.IsExactDecomposition {𝕜 : Type u} [RCLike 𝕜] {E G K : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (A : E →ₗ.[𝕜] E) (Λ₁ : G →ₗ.[𝕜] G) (F₀ : K →L[𝕜] E) (F₁ : G →L[𝕜] E) : Prop

The exact-coordinate half: F₀ and F₁ are complementary exhaustive isometries and F₁ intertwines A with the complementary block Λ₁.

• desiredIsometry : IsIsometric F₀

  The desired coordinate map is isometric.

• complementIsometry : IsIsometric F₁

  The complementary coordinate map is isometric.

• orthogonal : ContinuousLinearMap.adjoint F₀ ∘SL F₁ = 0

  The two ranges are orthogonal.

• complete : F₀ ∘SL ContinuousLinearMap.adjoint F₀ + F₁ ∘SL ContinuousLinearMap.adjoint F₁ = ContinuousLinearMap.id 𝕜 E

  Together they exhaust the space.

• mapsDomain (y : ↥Λ₁.domain) : F₁ ↑y ∈ A.domain

  F₁ carries the block domain into the ambient domain.

• intertwines (y : ↥Λ₁.domain) : ↑A ⟨F₁ ↑y, ⋯⟩ = F₁ (↑Λ₁ y)

  and intertwines the two operators there.

structure RotationOfEigenvectors.TrialBlock {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Type v

The trial data of a subspace, in the source's own shape (1.8): a trial operator A₀ on the subspace, possibly unbounded, and a bounded residual R with A z = A₀ z + R z on the trial domain. The compression is a partial map because the Appendix to Section 6 allows the tangent theorem's A₀ to be unbounded.

• compression : ↥U →ₗ.[𝕜] ↥U

  The trial block A₀, a partial map on the trial subspace.

• compression_selfAdjoint : IsSelfAdjoint self.compression

  A₀ is self-adjoint.

• residual : ↥U →L[𝕜] E

  The bounded residual R.

• mem_domain (z : ↥self.compression.domain) : ↑↑z ∈ A.domain

  Trial vectors in the compression's domain lie in the ambient domain.

• action_eq (z : ↥self.compression.domain) : ↑A ⟨↑↑z, ⋯⟩ = ↑(↑self.compression z) + self.residual ↑z

  and there A z = A₀ z + R z, which is (1.8).

structure RotationOfEigenvectors.BoundedTrialBlock {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Type v

The trial data of a subspace with a bounded compression, in the source's shape (1.8): a bounded self-adjoint A₀ on a trial subspace inside dom A, and a bounded residual R with A z = A₀ z + R z there.

The Appendix to Section 6 relaxes the sine family -- the sin Θ theorem, Proposition 6.1 and Theorem 6.1 -- to allow one of A₀, Λ₁ to be unbounded, and reserves "both may be unbounded" for the tangent theorem. Here the unwanted exact block is the unbounded one.

• compression : ↥U →L[𝕜] ↥U

  The trial block A₀, bounded on the trial subspace.

• compression_selfAdjoint : IsSelfAdjoint self.compression

  A₀ is self-adjoint.

• residual : ↥U →L[𝕜] E

  The bounded residual R.

• mem_domain (z : ↥U) : ↑z ∈ A.domain

  The trial subspace lies inside the ambient domain.

• action_eq (z : ↥U) : ↑A ⟨↑z, ⋯⟩ = ↑(self.compression z) + self.residual z

  and there A z = A₀ z + R z, which is (1.8).

structure RotationOfEigenvectors.RitzData {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] extends RotationOfEigenvectors.TrialBlock A U : Type v

Rayleigh--Ritz trial data: trial data whose residual is orthogonal to the trial subspace. This is the source's H₀ = 0 in the form (1.8) takes when A₀ = E₀^*(A+H)E₀, the extra hypothesis the tan Θ theorem imposes and the sin Θ and sin 2Θ theorems do not.

• compression : ↥U →ₗ.[𝕜] ↥U
• compression_selfAdjoint : IsSelfAdjoint self.compression
• residual : ↥U →L[𝕜] E
• mem_domain (z : ↥self.compression.domain) : ↑↑z ∈ A.domain
• action_eq (z : ↥self.compression.domain) : ↑A ⟨↑↑z, ⋯⟩ = ↑(↑self.compression z) + self.residual ↑z
• residual_orthogonal (z z' : ↥U) : inner 𝕜 (self.residual z) ↑z' = 0

  The residual is orthogonal to the trial subspace.

4. The source separation

def RotationOfEigenvectors.realResolventSet {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : Set ℝ

The real resolvent set: the shifted operator has a bounded two-sided inverse.

Equations

• RotationOfEigenvectors.realResolventSet A = {lam : ℝ | ∃ (R : E →L[𝕜] E), (∀ (x : ↥A.domain), R (↑A x - ↑lam • ↑x) = ↑x) ∧ ∀ (y : E), ∃ (h : R y ∈ A.domain), ↑A ⟨R y, h⟩ - ↑lam • R y = y}

def RotationOfEigenvectors.realSpectrum {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : Set ℝ

The real spectrum.

Equations

• RotationOfEigenvectors.realSpectrum A = (RotationOfEigenvectors.realResolventSet A)ᶜ

def RotationOfEigenvectors.SemiboundedBelow {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : ℝ) : Prop

The quadratic form of A is at least c on its domain.

Equations

• RotationOfEigenvectors.SemiboundedBelow A c = ∀ (x : ↥A.domain), c * ‖↑x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (↑A x) ↑x)

def RotationOfEigenvectors.SemiboundedAbove {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : ℝ) : Prop

The quadratic form of A is at most c on its domain.

Equations

• RotationOfEigenvectors.SemiboundedAbove A c = ∀ (x : ↥A.domain), RCLike.re (inner 𝕜 (↑A x) ↑x) ≤ c * ‖↑x‖ ^ 2

inductive RotationOfEigenvectors.SylvesterGap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (δ : ℝ) : Prop

The source separation of two blocks by a gap of width δ. intervalExterior is the printed interval/exterior condition, symmetric in the two blocks; the two ordered constructors are the half-infinite configurations the source explicitly permits, in which both blocks may have unbounded spectrum.

• intervalExterior {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {δ β α : ℝ} (hβα : β ≤ α) (hgap : realSpectrum A ⊆ Set.Icc β α ∧ realSpectrum B ⊆ {x : ℝ | x ≤ β - δ ∨ α + δ ≤ x} ∨ realSpectrum B ⊆ Set.Icc β α ∧ realSpectrum A ⊆ {x : ℝ | x ≤ β - δ ∨ α + δ ≤ x}) : SylvesterGap A B δ
• leftAboveRightBelow {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {δ : ℝ} (c : ℝ) (hA : SemiboundedBelow A (c + δ)) (hB : SemiboundedAbove B c) : SylvesterGap A B δ
• leftBelowRightAbove {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {δ : ℝ} (c : ℝ) (hA : SemiboundedAbove A c) (hB : SemiboundedBelow B (c + δ)) : SylvesterGap A B δ

inductive RotationOfEigenvectors.SinTwoThetaGap {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (δ : ℝ) : Prop

The oriented separation printed in the sin 2Θ theorem. The first block is the source's Λ₀ and the second is Λ₁: for a finite interval, Λ₀ lies inside [β, α] while Λ₁ lies outside the enlarged open interval (β - δ, α + δ). The second constructor is exactly the lower half-line extension stated immediately after the four Section 2 theorems. This is intentionally narrower than SylvesterGap, whose interval constructor is symmetric and is appropriate for the printed sin Θ theorem.

• intervalExterior {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {δ β α : ℝ} (hβα : β ≤ α) (hA : realSpectrum A ⊆ Set.Icc β α) (hB : realSpectrum B ⊆ {x : ℝ | x ≤ β - δ ∨ α + δ ≤ x}) : SinTwoThetaGap A B δ
• leftBelowRightAbove {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {δ : ℝ} (c : ℝ) (hA : SemiboundedAbove A c) (hB : SemiboundedBelow B (c + δ)) : SinTwoThetaGap A B δ

5. Reducing subspaces and their blocks

Section 1 says in as many words that neither P nor Q is assumed to be a spectral projector: what the theorems assume is that the decomposition reduces the operator and that its two blocks are separated.

def RotationOfEigenvectors.Reduces {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Prop

A subspace reduces a partial map when both projections preserve its domain and both summands are invariant.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RotationOfEigenvectors.block {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (h : Reduces A U) : ↥U →ₗ.[𝕜] ↥U

The block of A on a reducing subspace.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def RotationOfEigenvectors.addBounded {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : E →ₗ.[𝕜] E

Adding a bounded operator to a partial map, on the same domain.

Equations

• RotationOfEigenvectors.addBounded A V = { domain := A.domain, toFun := A.toFun + (↑V).domRestrict A.domain }

theorem RotationOfEigenvectors.Reduces.orthogonal {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h : Reduces A U) : Reduces A Uᗮ

The orthogonal complement of a reducing subspace also reduces the operator, so the ambient separation hypothesis can name both blocks.

6. The angle quantities

The sines are explicit operators; the tangents are sequences, ‖tan Θ‖ being the norm's value on tan θ₁, tan θ₂, ….

noncomputable def RotationOfEigenvectors.directedSine {𝕜 : Type u} [RCLike 𝕜] {E F K : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (E₀ : F →L[𝕜] E) (F₀ : K →L[𝕜] E) : F →L[𝕜] E

sin Θ₀ in coordinates: the part of the trial coordinate map that misses the exact subspace, the source's Q^⊥E₀.

Equations

• RotationOfEigenvectors.directedSine E₀ F₀ = (ContinuousLinearMap.id 𝕜 E - F₀ ∘SL ContinuousLinearMap.adjoint F₀) ∘SL E₀

noncomputable def RotationOfEigenvectors.directedSineBlock {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [V.HasOrthogonalProjection] : ↥U →L[𝕜] E

sin Θ₀ for a trial subspace: Q^⊥E₀ = P_{Vᗮ}|_U.

Equations

• RotationOfEigenvectors.directedSineBlock U V = Vᗮ.starProjection ∘SL U.subtypeL

noncomputable def RotationOfEigenvectors.ambientSine {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : E →L[𝕜] E

sin Θ, the ambient sine: the projector difference, whose singular values are the sines of the principal angles, each occurring twice.

Equations

• RotationOfEigenvectors.ambientSine U V = V.starProjection - U.starProjection

noncomputable def RotationOfEigenvectors.ambientDoubleSine {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : E →L[𝕜] E

sin 2Θ, the ambient double-angle sine: the projector difference between U and its mirror image in V. Reflecting U in V doubles every principal angle.

Equations

• RotationOfEigenvectors.ambientDoubleSine U V = (Submodule.map (↑V.reflection.toLinearEquiv) U).starProjection - U.starProjection

noncomputable def RotationOfEigenvectors.directedDoubleSine {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : E →L[𝕜] E

sin 2Θ₀, the directed double-angle sine.

Equations

• RotationOfEigenvectors.directedDoubleSine U V = U.starProjection ∘SL (Submodule.map (↑V.reflection.toLinearEquiv) Uᗮ).starProjection

Tangents of an angle presented by its sine

The argument of tanSeq is always a sine: tan Θ₀ is a trigonometric function of the angle, presented here by an operator whose singular values are its sines. The residual is the right-hand side and has nothing to do with the left.

A doubled angle is presented by its own sine, never by doubling the ordered sines of the single angle. θ ↦ sin 2θ is not monotone on [0, π/2], so n ↦ sin (2 arcsin (aₙ(sin Θ))) need not be the ordered singular-value sequence of sin 2Θ -- at principal angles 75° and 30° the two sequences are in opposite order. The tan 2Θ clauses below therefore read the doubled tangent off ambientDoubleSine and directedDoubleSine, through the same monotone u ↦ tan (arcsin u) that tan Θ uses, and |tan 2θ| = tan (arcsin |sin 2θ|) supplies the source's absolute value with no branch choice.

noncomputable def RotationOfEigenvectors.tanSeq {𝕜 : Type u} [RCLike 𝕜] {X Y : Type v} [NormedAddCommGroup X] [InnerProductSpace 𝕜 X] [NormedAddCommGroup Y] [InnerProductSpace 𝕜 Y] (S : X →L[𝕜] Y) (n : ℕ) : ℝ

The sequence tan θ₀, tan θ₁, …, where sin θₙ is the n-th singular value of the sine operator S.

Equations

• RotationOfEigenvectors.tanSeq S n = Real.tan (Real.arcsin (RotationOfEigenvectors.singularValue S n))

def RotationOfEigenvectors.TangentDefined {𝕜 : Type u} [RCLike 𝕜] {X Y : Type v} [NormedAddCommGroup X] [InnerProductSpace 𝕜 X] [NormedAddCommGroup Y] [InnerProductSpace 𝕜 Y] (S : X →L[𝕜] Y) : Prop

No principal angle of S is a right angle, so every tan θₙ is a genuine tangent rather than the value Lean's field division assigns at a pole. Equivalently ‖S‖ < 1, since a₀ S = ‖S‖. Davis and Kahan derive this rather than assuming it, so it appears below as a conclusion -- for the double-angle clauses too, where S is the double-angle sine and the condition is the quarter-turn exclusion ‖sin 2Θ‖ < 1.

Equations

• RotationOfEigenvectors.TangentDefined S = ∀ (n : ℕ), Real.cos (Real.arcsin (RotationOfEigenvectors.singularValue S n)) ≠ 0