Davis--Kahan 1970: Palomar solution bridge

The public vocabulary used by Comparator is elaborated in Palomar.DKSectionTwo.SolutionPrelude, which imports Mathlib alone and is an exact copy of the Challenge's definition prefix. Keeping that vocabulary out of the larger Davis--Kahan import environment makes its exported constants identical to the Challenge constants. This module then adds only the bridge to the compiled formalization and the five proofs.

7. Bridge to the compiled Davis--Kahan development

The Challenge intentionally uses Mathlib-only vocabulary. The Solution keeps that public vocabulary unchanged and translates it once into the production Section 2 API. In particular, the tangent proofs use the scalar-generic RCLike endpoints directly; there is no local real/complex proof split.

theorem RotationOfEigenvectors.singularValue_eq_approximationNumber {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (T : E →L[𝕜] F) (n : ℕ) : singularValue T n = T.approximationNumber n

The Challenge's singular values are the development's approximation numbers.

noncomputable def RotationOfEigenvectors.UISeminorm.toTauCeti {G : Type v} [NormedAddCommGroup G] [InnerProductSpace ℂ G] [FiniteDimensional ℂ G] (N : UISeminorm G) : TauCeti.UnitarilyInvariantSeminorm ℂ G G

Convert the Mathlib-only finite-dimensional UI seminorm to the production rectangular UI-seminorm structure.

Equations

• N.toTauCeti = { toSeminorm := Seminorm.of N.toFun ⋯ ⋯, unitary_invariant' := ⋯ }

theorem RotationOfEigenvectors.diagOp_eq {n : ℕ} {G : Type v} [NormedAddCommGroup G] [InnerProductSpace ℂ G] (b : OrthonormalBasis (Fin n) ℂ G) (x : Fin n → ℝ) : diagOp b x = TauCeti.diagOp b x

The diagonal operators used by the two finite gauges coincide.

theorem RotationOfEigenvectors.UISeminorm.gauge_eq {n : ℕ} {G : Type v} [NormedAddCommGroup G] [InnerProductSpace ℂ G] [FiniteDimensional ℂ G] (N : UISeminorm G) (b : OrthonormalBasis (Fin n) ℂ G) (x : Fin n → ℝ) : N.gauge b x = N.toTauCeti.gauge b x

Hence the finite gauges coincide.

noncomputable def RotationOfEigenvectors.SymmetricNormingFunction.toSourceNorm (N : SymmetricNormingFunction) : TauCeti.DavisKahan.ExactSinTheta.SymmetricNormingFunction

The Challenge symmetric norming function as the production source norm.

Equations

• N.toSourceNorm = { finiteNorm := fun (n : ℕ) => (N.finiteNorm n).toTauCeti, normalized := ⋯, zero_pad := ⋯ }

theorem RotationOfEigenvectors.SymmetricNormingFunction.evalSeq_eq_of_approximationNumber {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : SymmetricNormingFunction) (s : ℕ → ℝ) (T : E →L[𝕜] F) (h : ∀ (n : ℕ), T.approximationNumber n = s n) : N.evalSeq s = N.toSourceNorm.extendedGauge T

A sequence represented as the approximation-number sequence of an operator has the same extended norm in the Challenge and production vocabularies.

theorem RotationOfEigenvectors.SymmetricNormingFunction.eval_eq {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : SymmetricNormingFunction) (T : E →L[𝕜] F) : N.eval T = N.toSourceNorm.extendedGauge T

Operator evaluation agrees with production evaluation.

theorem RotationOfEigenvectors.SymmetricNormingFunction.finite_iff {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : SymmetricNormingFunction) (T : E →L[𝕜] F) : N.Finite T ↔ N.toSourceNorm.Mem T

Ideal membership is the same proposition on both sides of the bridge.

theorem RotationOfEigenvectors.SymmetricNormingFunction.norm_eq {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (N : SymmetricNormingFunction) (T : E →L[𝕜] F) : N.norm T = N.toSourceNorm.gauge T

The real-valued operator norms agree.

theorem RotationOfEigenvectors.tangentDefined_of_approximationNumber_lt_one {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (S : E →L[𝕜] F) (h : ∀ (n : ℕ), S.approximationNumber n < 1) : TangentDefined S

Pole exclusion from the approximation-number bound.

theorem RotationOfEigenvectors.isTrialResidual_iff {𝕜 : 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) : IsTrialResidual A A₀ E₀ R ↔ TauCeti.DavisKahan1970.IsTrialResidual A A₀ E₀ R

theorem RotationOfEigenvectors.isExactDecomposition_iff {𝕜 : 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) : IsExactDecomposition A Λ₁ F₀ F₁ ↔ TauCeti.DavisKahan1970.IsExactSpectralDecomposition A Λ₁ F₀ F₁

theorem RotationOfEigenvectors.realResolventSet_eq {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : realResolventSet A = TauCeti.LinearPMap.realResolventSet A

theorem RotationOfEigenvectors.realSpectrum_eq {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) : realSpectrum A = TauCeti.LinearPMap.realSpectrum A

theorem RotationOfEigenvectors.semiboundedBelow_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : ℝ) : SemiboundedBelow A c ↔ TauCeti.LinearPMap.SemiboundedBelow A c

theorem RotationOfEigenvectors.semiboundedAbove_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (c : ℝ) : SemiboundedAbove A c ↔ TauCeti.LinearPMap.SemiboundedAbove A c

theorem RotationOfEigenvectors.sylvesterGap_iff {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (A : E →ₗ.[𝕜] E) (B : F →ₗ.[𝕜] F) (δ : ℝ) : SylvesterGap A B δ ↔ TauCeti.DavisKahan.Sylvester.FormBoundedSylvesterGap A B δ

theorem RotationOfEigenvectors.SinTwoThetaGap.toSylvesterGap {𝕜 : Type u} [RCLike 𝕜] {E F : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →ₗ.[𝕜] E} {B : F →ₗ.[𝕜] F} {δ : ℝ} : SinTwoThetaGap A B δ → SylvesterGap A B δ

Forget the source-facing orientation of the sin 2Θ gap when entering the more general internal Sylvester-gap API.

theorem RotationOfEigenvectors.reduces_iff {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] : Reduces A U ↔ TauCeti.LinearPMap.ReducesSubspace A U

theorem RotationOfEigenvectors.block_eq {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (U : Submodule 𝕜 E) [U.HasOrthogonalProjection] (h : Reduces A U) : block A U h = TauCeti.LinearPMap.reducingRestriction A U ⋯

theorem RotationOfEigenvectors.addBounded_eq {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (A : E →ₗ.[𝕜] E) (V : E →L[𝕜] E) : addBounded A V = TauCeti.LinearPMap.addBounded A V

def RotationOfEigenvectors.RitzData.toUnboundedRitzPair {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (D : RitzData A U) : TauCeti.DavisKahan.UnboundedRitzPair A U

A Challenge Ritz bundle as the production unbounded Ritz pair.

Equations

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

theorem RotationOfEigenvectors.isOddFor_of_offDiagonal {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {H : E →L[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h₀ : U.starProjection ∘SL H ∘SL U.starProjection = 0) (h₁ : Uᗮ.starProjection ∘SL H ∘SL Uᗮ.starProjection = 0) : TauCeti.IsOddFor U H

theorem RotationOfEigenvectors.reflectionIntertwines_of_reduces {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {H : E →L[𝕜] E} {V : Submodule 𝕜 E} [V.HasOrthogonalProjection] (hV : Reduces (addBounded A H) V) : TauCeti.DavisKahan.ReflectionIntertwines A H V

A reducing subspace of the bounded perturbation supplies the reflection intertwining data used by the ambient double-angle theorem.

theorem RotationOfEigenvectors.formBound_upper_of_semiboundedAbove {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Reduces A U) {α : ℝ} (hupper : SemiboundedAbove (block A U hU) α) (x : ↥A.domain) : ↑x ∈ U → RCLike.re (inner 𝕜 (↑A x) ↑x) ≤ α * ‖↑x‖ ^ 2

theorem RotationOfEigenvectors.formBound_lower_of_semiboundedBelow {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {A : E →ₗ.[𝕜] E} {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Reduces A U) {c : ℝ} (hlower : SemiboundedBelow (block A Uᗮ ⋯) c) (x : ↥A.domain) : ↑x ∈ Uᗮ → c * ‖↑x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (↑A x) ↑x)

theorem RotationOfEigenvectors.directedDoubleSine_eq {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (U V : Submodule 𝕜 E) [U.HasOrthogonalProjection] [V.HasOrthogonalProjection] : directedDoubleSine U V = TauCeti.DavisKahan.sinTwoThetaIdealBlock U V

8. The four theorem families of Section 2

The Palomar surface has five source-facing clauses. Three membership-and-bound variants expose the sine conclusions without assuming angle membership, alongside the five retained compatibility declarations. The two whole-space tangent bounds are consequences in the source proof and are not repeated here; the two sin 2Θ clauses remain separate.

theorem RotationOfEigenvectors.sinTheta_mem_and_bound {𝕜 : Type u} [RCLike 𝕜] {E F G K : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (N : SymmetricNormingFunction) {A : E →ₗ.[𝕜] E} {A₀ : F →ₗ.[𝕜] F} {Λ₁ : G →ₗ.[𝕜] G} {E₀ : F →L[𝕜] E} {F₀ : K →L[𝕜] E} {F₁ : G →L[𝕜] E} {R : F →L[𝕜] E} (hA : IsSelfAdjoint A) (hA₀ : IsSelfAdjoint A₀) (hΛ₁ : IsSelfAdjoint Λ₁) (hres : IsTrialResidual A A₀ E₀ R) (hdec : IsExactDecomposition A Λ₁ F₀ F₁) {δ : ℝ} (hδ : 0 < δ) (hgap : SylvesterGap A₀ Λ₁ δ) (hR : N.Finite R) : N.Finite (directedSine E₀ F₀) ∧ δ * N.norm (directedSine E₀ F₀) ≤ N.norm R

Residual ideal membership gives sine-angle membership and its gap bound.

theorem RotationOfEigenvectors.sinTheta {𝕜 : Type u} [RCLike 𝕜] {E F G K : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [CompleteSpace G] [NormedAddCommGroup K] [InnerProductSpace 𝕜 K] [CompleteSpace K] (N : SymmetricNormingFunction) {A : E →ₗ.[𝕜] E} {A₀ : F →ₗ.[𝕜] F} {Λ₁ : G →ₗ.[𝕜] G} {E₀ : F →L[𝕜] E} {F₀ : K →L[𝕜] E} {F₁ : G →L[𝕜] E} {R : F →L[𝕜] E} (hA : IsSelfAdjoint A) (hA₀ : IsSelfAdjoint A₀) (hΛ₁ : IsSelfAdjoint Λ₁) (hres : IsTrialResidual A A₀ E₀ R) (hdec : IsExactDecomposition A Λ₁ F₀ F₁) {δ : ℝ} (hδ : 0 < δ) (hgap : SylvesterGap A₀ Λ₁ δ) (_hSin : N.Finite (directedSine E₀ F₀)) (hR : N.Finite R) : δ * N.norm (directedSine E₀ F₀) ≤ N.norm R

The sin Θ theorem, at the source where-defined norm boundary.

theorem RotationOfEigenvectors.tanTheta {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (N : SymmetricNormingFunction) {A : E →ₗ.[𝕜] E} (_hA : IsSelfAdjoint A) {V : Submodule 𝕜 E} [V.HasOrthogonalProjection] (hV : Reduces A V) {α δ : ℝ} (hδ : 0 < δ) (hunwanted : SemiboundedBelow (block A Vᗮ ⋯) (α + δ)) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (D : RitzData A U) (hupper : SemiboundedAbove D.compression α) (hR : N.Finite D.residual) : TangentDefined (directedSineBlock U V) ∧ N.SeqFinite (tanSeq (directedSineBlock U V)) ∧ δ * N.seqNorm (tanSeq (directedSineBlock U V)) ≤ N.norm D.residual

The tan Θ theorem, in its stronger residual form, for Rayleigh--Ritz trial data. The residual is orthogonal to the trial subspace, as required by RitzData.residual_orthogonal.

theorem RotationOfEigenvectors.sinTwoTheta_directed_mem_and_bound {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (N : SymmetricNormingFunction) {A T : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) (hT : IsSelfAdjoint T) (hdom : T.domain = A.domain) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Reduces A U) {V : Submodule 𝕜 E} [V.HasOrthogonalProjection] (hV : Reduces T V) (R : ↥U →L[𝕜] E) (hres : ∀ (u : ↥U) (hu : ↑u ∈ T.domain), ↑T ⟨↑u, hu⟩ = ↑A ⟨↑u, ⋯⟩ + R u) {δ : ℝ} (hδ : 0 < δ) (hgap : SinTwoThetaGap (block T V hV) (block T Vᗮ ⋯) δ) (hR : N.Finite R) : N.Finite (directedDoubleSine V U) ∧ δ * N.norm (directedDoubleSine V U) ≤ 2 * N.norm R

Residual ideal membership gives directed double-angle membership and its gap bound.

theorem RotationOfEigenvectors.sinTwoTheta_directed {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (N : SymmetricNormingFunction) {A T : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) (hT : IsSelfAdjoint T) (hdom : T.domain = A.domain) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Reduces A U) {V : Submodule 𝕜 E} [V.HasOrthogonalProjection] (hV : Reduces T V) (R : ↥U →L[𝕜] E) (hres : ∀ (u : ↥U) (hu : ↑u ∈ T.domain), ↑T ⟨↑u, hu⟩ = ↑A ⟨↑u, ⋯⟩ + R u) {δ : ℝ} (hδ : 0 < δ) (hgap : SinTwoThetaGap (block T V hV) (block T Vᗮ ⋯) δ) (_hAngle : N.Finite (directedDoubleSine V U)) (hR : N.Finite R) : δ * N.norm (directedDoubleSine V U) ≤ 2 * N.norm R

The residual clause of the sin 2Θ theorem, at the source common-domain scope.

theorem RotationOfEigenvectors.sinTwoTheta_ambient_mem_and_bound {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (N : SymmetricNormingFunction) {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Reduces A U) (H : E →L[𝕜] E) (hH : IsSelfAdjoint H) {V : Submodule 𝕜 E} [V.HasOrthogonalProjection] (hV : Reduces (addBounded A H) V) {δ : ℝ} (hδ : 0 < δ) (hgap : SinTwoThetaGap (block (addBounded A H) V hV) (block (addBounded A H) Vᗮ ⋯) δ) (hHmem : N.Finite H) : N.Finite (ambientDoubleSine U V) ∧ δ * N.norm (ambientDoubleSine U V) ≤ 2 * N.norm H

Perturbation ideal membership gives ambient double-angle membership and its gap bound.

theorem RotationOfEigenvectors.sinTwoTheta_ambient {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (N : SymmetricNormingFunction) {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Reduces A U) (H : E →L[𝕜] E) (hH : IsSelfAdjoint H) {V : Submodule 𝕜 E} [V.HasOrthogonalProjection] (hV : Reduces (addBounded A H) V) {δ : ℝ} (hδ : 0 < δ) (hgap : SinTwoThetaGap (block (addBounded A H) V hV) (block (addBounded A H) Vᗮ ⋯) δ) (_hAngle : N.Finite (ambientDoubleSine U V)) (hHmem : N.Finite H) : δ * N.norm (ambientDoubleSine U V) ≤ 2 * N.norm H

The whole-space clause of the sin 2Θ theorem, with the printed operator roles.

theorem RotationOfEigenvectors.tanTwoTheta {𝕜 : Type u} [RCLike 𝕜] {E : Type v} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (N : SymmetricNormingFunction) {A : E →ₗ.[𝕜] E} (hA : IsSelfAdjoint A) {U : Submodule 𝕜 E} [U.HasOrthogonalProjection] (hU : Reduces A U) (H : E →L[𝕜] E) (_hH : IsSelfAdjoint H) (hoffdiag₀ : U.starProjection ∘SL H ∘SL U.starProjection = 0) (hoffdiag₁ : Uᗮ.starProjection ∘SL H ∘SL Uᗮ.starProjection = 0) {α δ : ℝ} (hδ : 0 < δ) (hlow : SemiboundedAbove (block A U hU) α) (hhigh : SemiboundedBelow (block A Uᗮ ⋯) (α + δ)) {V : Submodule 𝕜 E} [V.HasOrthogonalProjection] (hV : Reduces (addBounded A H) V) (hRmem : N.Finite (Uᗮ.starProjection ∘SL H ∘SL U.starProjection)) : TangentDefined (directedDoubleSine U V) ∧ N.SeqFinite (tanSeq (directedDoubleSine U V)) ∧ δ * N.seqNorm (tanSeq (directedDoubleSine U V)) ≤ 2 * N.norm (Uᗮ.starProjection ∘SL H ∘SL U.starProjection)

The tan 2Θ theorem, in its stronger residual form.