The separated Sylvester bound to The Yu–Wang–Samworth overlap…

TheoremThe separated Sylvester bound#

If the real part of the quadratic form of A is at least c + g and that of B is at most c, then g ‖X‖ ≤ ‖A X - X B‖ for every bounded operator X. For g > 0, every solution of A X - X B = Y therefore satisfies ‖X‖ ≤ ‖Y‖ / g.

ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_le_re_inner_of_re_inner_le.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {A : E →L[𝕜] E}
  {B : F →L[𝕜] F} {c g : ℝ} (hA : ∀ (x : E), (c + g) * ‖x‖ ^ 2 ≤ RCLike.re (inner 𝕜 (A x) x))
  (hB : ∀ (y : F), RCLike.re (inner 𝕜 (B y) y) ≤ c * ‖y‖ ^ 2) (X : F →L[𝕜] E) :
  g * ‖X‖ ≤ ‖(A.sylvester B) X‖

Lean

Formalized in Tau Ceti as ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_le_re_inner_of_re_inner_le.

Sources

• Tau Ceti documentation: ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_le_re_inner_of_re_inner_le
• Source of ContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_le_re_inner_of_re_inner_le in TauCeti/Analysis/InnerProductSpace/Sylvester.lean

LeanContinuousLinearMap.mul_norm_le_norm_sylvester_apply_of_le_re_inner_of_re_inner_le

Uses 1

Proof usesCauchy–Schwarz for the column series

TheoremThe singular-value Hoffman–Wielandt inequality#

The singular-value Hoffman–Wielandt inequality when the domain dimension does not exceed the codomain dimension. The squared distance between the ordered singular values is at most the squared Frobenius seminorm of the difference.

LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_of_finrank_le.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] (A B : E →ₗ[𝕜] F) (hEF : Module.finrank 𝕜 E ≤ Module.finrank 𝕜 F) :
  ∑ i, (A.singularValues ↑i - B.singularValues ↑i) ^ 2 ≤
    (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E F) (A - B) ^ 2

Lean

Formalized in Tau Ceti as LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_of_finrank_le.

Other forms

The singular-value Hoffman–Wielandt inequality for arbitrary finite-dimensional maps. Formalized in Tau Ceti as LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_min.

LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_min.{u_1, u_2, u_3} {𝕜 : Type u_1}
  {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 F]
  (A B : E →ₗ[𝕜] F) :
  ∑ i, (A.singularValues ↑i - B.singularValues ↑i) ^ 2 ≤
    (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E F) (A - B) ^ 2

Sources

• Tau Ceti documentation: LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_of_finrank_le
• Source of LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_of_finrank_le in TauCeti/Analysis/InnerProductSpace/HoffmanWielandt/Singular.lean

LeanLinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_of_finrank_le · LinearMap.sum_sq_singularValues_sub_le_sq_frobenius_apply_sub_min

Uses 5 · Used by 1

Proof usesAbel's inequality, comparison form · ContinuousLinearMap.singularValue · Courant–Fischer, lower direction · Eckart–Young for Ky Fan gauges · Ky Fan's maximum principle, attainment

Used byThe singular-value Hoffman–Wielandt inequality for same-shaped rectangular matrices

TheoremThe spectral theorem for compact normal operators#

the eigenspaces of a compact normal operator on a complex Hilbert space have trivial mutual orthogonal complement.

IsStarNormal.orthogonalComplement_iSup_eigenspaces_eq_bot.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E}
  (hT : IsStarNormal T) (hc : IsCompactOperator ⇑T) : (⨆ μ, Module.End.eigenspace (↑T) μ)ᗮ = ⊥

Lean

Formalized in Tau Ceti as IsStarNormal.orthogonalComplement_iSup_eigenspaces_eq_bot.

Sources

• Tau Ceti documentation: IsStarNormal.orthogonalComplement_iSup_eigenspaces_eq_bot
• Source of IsStarNormal.orthogonalComplement_iSup_eigenspaces_eq_bot in TauCeti/Analysis/InnerProductSpace/Spectral/CompactNormal.lean

LeanIsStarNormal.orthogonalComplement_iSup_eigenspaces_eq_bot

TheoremSpectral theorem for normal operators#

The Borel calculus of the coordinate function on the spectrum is a itself, that is, a = ∫ z dP(z).

ContinuousLinearMap.borelCalculus_restrict_id.{u_1} {H : Type u_1} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] (a : H →L[ℂ] H) [IsStarNormal a] :
  a.borelCalculus
      (TauCeti.BoundedBorelFunction.ofContinuousMap
        (ContinuousMap.restrict (spectrum ℂ a) (ContinuousMap.id ℂ))) =
    a

Lean

Formalized in Tau Ceti as ContinuousLinearMap.borelCalculus_restrict_id.

Other forms

The spectral theorem for normal operators. Formalized in Tau Ceti as LinearMap.exists_orthonormalBasis_apply_eq_smul_of_isStarNormal.

LinearMap.exists_orthonormalBasis_apply_eq_smul_of_isStarNormal.{u_3, u_4} {E : Type u_3}
  [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] (T : E →ₗ[ℂ] E)
  [IsStarNormal T] {ι : Type u_4} [Fintype ι] (hι : Fintype.card ι = Module.finrank ℂ E) :
  ∃ b μ, ∀ (i : ι), T (b i) = μ i • b i

Sources

• Tau Ceti documentation: ContinuousLinearMap.borelCalculus_restrict_id
• Source of ContinuousLinearMap.borelCalculus_restrict_id in TauCeti/Analysis/InnerProductSpace/BorelCalculus/Basic.lean

LeanContinuousLinearMap.borelCalculus_restrict_id · LinearMap.exists_orthonormalBasis_apply_eq_smul_of_isStarNormal

Uses 2

Statement usesTauCeti.ProjValMeasure · TauCeti.ProjValMeasure.integral

TheoremThe spectral theorem for the solution operator#

its eigenspaces have trivial orthogonal complement in H, even when H is incomplete.

IsCoercive.orthogonalComplement_iSup_eigenspaces_formSolutionOperator_eq_bot.{u_9, u_10}
  {V : Type u_9} {H : Type u_10} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [NormedAddCommGroup H] [InnerProductSpace ℝ H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B)
  {J : V →L[ℝ] H} (hJ : IsCompactOperator ⇑J) (hsymm : ∀ (u v : V), (B u) v = (B v) u) :
  (⨆ mu, Module.End.eigenspace (↑(hB.formSolutionOperator J)) mu)ᗮ = ⊥

Lean

Formalized in Tau Ceti as IsCoercive.orthogonalComplement_iSup_eigenspaces_formSolutionOperator_eq_bot.

Sources

• Tau Ceti documentation: IsCoercive.orthogonalComplement_iSup_eigenspaces_formSolutionOperator_eq_bot
• Source of IsCoercive.orthogonalComplement_iSup_eigenspaces_formSolutionOperator_eq_bot in TauCeti/Analysis/InnerProductSpace/Variational/Spectrum.lean

LeanIsCoercive.orthogonalComplement_iSup_eigenspaces_formSolutionOperator_eq_bot

Used by 1

Used byThe spectral theorem for the Dirichlet problem

TheoremSylvester bound from a disc and the exterior of a larger disc#

If ‖A x - c x‖ ≤ r ‖x‖ for every x and (r + δ) ‖y‖ ≤ ‖B y - c y‖ for every y, then δ N(X) ≤ N(A X - X B) for every unitarily invariant seminorm N.

TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_norm_sub_smul_le_of_le_norm_sub_smul.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {c : 𝕜} {r δ : ℝ}
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) (hA : ∀ (x : E), ‖A x - c • x‖ ≤ r * ‖x‖)
  (hB : ∀ (y : F), (r + δ) * ‖y‖ ≤ ‖B y - c • y‖) (X : F →L[𝕜] E) :
  δ * N ↑X ≤ N ↑((A.sylvester B) X)

Lean

Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_norm_sub_smul_le_of_le_norm_sub_smul.

Other forms

Sylvester bound from the exterior of a disc and a smaller disc. Formalized in Tau Ceti as TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_le_norm_sub_smul_of_norm_sub_smul_le.

TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_le_norm_sub_smul_of_norm_sub_smul_le.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] {A : E →L[𝕜] E} {B : F →L[𝕜] F} {c : 𝕜} {r δ : ℝ}
  (N : TauCeti.UnitarilyInvariantSeminorm 𝕜 F E) (hA : ∀ (x : E), (r + δ) * ‖x‖ ≤ ‖A x - c • x‖)
  (hB : ∀ (y : F), ‖B y - c • y‖ ≤ r * ‖y‖) (X : F →L[𝕜] E) : δ * N ↑X ≤ N ↑((A.sylvester B) X)

Sources

• Tau Ceti documentation: TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_norm_sub_smul_le_of_le_norm_sub_smul
• Source of TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_norm_sub_smul_le_of_le_norm_sub_smul in TauCeti/Analysis/InnerProductSpace/UnitarilyInvariantSeminorm/Sylvester/Basic.lean

LeanTauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_norm_sub_smul_le_of_le_norm_sub_smul · TauCeti.UnitarilyInvariantSeminorm.mul_map_le_map_sylvester_apply_of_le_norm_sub_smul_of_norm_sub_smul_le

Uses 2

Proof usesCourant–Fischer, lower direction · Fan dominance

TheoremThe variational Fredholm alternative#

For a compact continuous linear map J, either the homogeneous perturbation of B by κ ⟪J ·, J ·⟫ has a nonzero solution, or every represented forcing has a unique solution.

IsCoercive.fredholmAlternative_formPerturbation.{u_1, u_2} {V : Type u_1} {H : Type u_2}
  [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [SeminormedAddCommGroup H]
  [InnerProductSpace ℝ H] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) {J : V →L[ℝ] H}
  (hJ : IsCompactOperator ⇑J) (kappa : ℝ) :
  (∃ u, u ≠ 0 ∧ ∀ (v : V), (B u) v - kappa * inner ℝ (J u) (J v) = 0) ∨
    ∀ (ell : StrongDual ℝ V), ∃! u, ∀ (v : V), (B u) v - kappa * inner ℝ (J u) (J v) = ell v

Lean

Formalized in Tau Ceti as IsCoercive.fredholmAlternative_formPerturbation.

Sources

• Tau Ceti documentation: IsCoercive.fredholmAlternative_formPerturbation
• Source of IsCoercive.fredholmAlternative_formPerturbation in TauCeti/Analysis/InnerProductSpace/Variational/Fredholm.lean

LeanIsCoercive.fredholmAlternative_formPerturbation

Used by 1

Used byThe Fredholm alternative in eigenvalue language

TheoremThe von Neumann trace inequality#

For symmetric T and S with eigenvalues listed in decreasing order, Re tr (T S) ≤ ∑ᵢ λᵢ(T) λᵢ(S).

LinearMap.IsSymmetric.re_trace_comp_le_sum_eigenvalues_mul_eigenvalues.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E]
  {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hS : S.IsSymmetric)
  (hn : Module.finrank 𝕜 E = n) :
  RCLike.re ((LinearMap.trace 𝕜 E) (T ∘ₗ S)) ≤ ∑ i, hT.eigenvalues hn i * hS.eigenvalues hn i

Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.re_trace_comp_le_sum_eigenvalues_mul_eigenvalues.

Sources

• Tau Ceti documentation: LinearMap.IsSymmetric.re_trace_comp_le_sum_eigenvalues_mul_eigenvalues
• Source of LinearMap.IsSymmetric.re_trace_comp_le_sum_eigenvalues_mul_eigenvalues in TauCeti/Analysis/InnerProductSpace/HoffmanWielandt/Basic.lean

LeanLinearMap.IsSymmetric.re_trace_comp_le_sum_eigenvalues_mul_eigenvalues

TheoremVon Neumann's criterion#

A symmetric partial linear map is self-adjoint if its shifts by +i and -i are surjective. Density follows from the first shift, so no independent density hypothesis is needed.

LinearPMap.isSelfAdjoint_of_surjective_addSub.{u_3} {H : Type u_3} [NormedAddCommGroup H]
  [InnerProductSpace ℂ H] [CompleteSpace H] (A : H →ₗ.[ℂ] H) (hsym : A.IsFormalAdjoint A)
  (hplus : ∀ (φ : H), ∃ ψ, ↑A ψ + Complex.I • ↑ψ = φ)
  (hminus : ∀ (φ : H), ∃ ψ, ↑A ψ - Complex.I • ↑ψ = φ) : IsSelfAdjoint A

Lean

Formalized in Tau Ceti as LinearPMap.isSelfAdjoint_of_surjective_addSub.

Sources

• Tau Ceti documentation: LinearPMap.isSelfAdjoint_of_surjective_addSub
• Source of LinearPMap.isSelfAdjoint_of_surjective_addSub in TauCeti/Analysis/InnerProductSpace/LinearPMap/SelfAdjoint.lean

LeanLinearPMap.isSelfAdjoint_of_surjective_addSub

Theoremvon Neumann's theorem#

The adjoint of a closed densely defined partial linear map between complete inner product spaces has dense domain.

LinearPMap.dense_adjoint_domain.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F]
  [InnerProductSpace 𝕜 F] [CompleteSpace F] {T : E →ₗ.[𝕜] F} (hT : Dense ↑T.domain)
  (hTc : T.IsClosed) : Dense ↑T.adjoint.domain

Lean

Formalized in Tau Ceti as LinearPMap.dense_adjoint_domain.

Sources

• Tau Ceti documentation: LinearPMap.dense_adjoint_domain
• Source of LinearPMap.dense_adjoint_domain in TauCeti/Analysis/InnerProductSpace/LinearPMap/SubmoduleAdjoint.lean

LeanLinearPMap.dense_adjoint_domain

TheoremWeyl's additive inequality, upper form#

for symmetric operators T and S and indices with i + j ≤ k, the decreasingly sorted eigenvalues satisfy λₖ(T + S) ≤ λᵢ(T) + λⱼ(S). Indices start at 0, so for k = i + j this is the classical λ_{i+j-1}(T + S) ≤ λᵢ(T) + λⱼ(S) in one-based indexing.

Horn & Johnson, Matrix Analysis 2nd ed., Theorem 4.3.1; Bhatia, Matrix Analysis, Theorem III.2.1.

LinearMap.IsSymmetric.eigenvalues_add_le.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E}
  (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {i j k : Fin n}
  (hk : ↑i + ↑j ≤ ↑k) : ⋯.eigenvalues hn k ≤ hT.eigenvalues hn i + hS.eigenvalues hn j

Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.eigenvalues_add_le.

Other forms

Weyl's additive inequality, lower form. Formalized in Tau Ceti as LinearMap.IsSymmetric.le_eigenvalues_add.

LinearMap.IsSymmetric.le_eigenvalues_add.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜]
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E}
  (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {i j k : Fin n}
  (hk : ↑k + n ≤ ↑i + ↑j + 1) : hT.eigenvalues hn i + hS.eigenvalues hn j ≤ ⋯.eigenvalues hn k

Sources

• Tau Ceti documentation: LinearMap.IsSymmetric.eigenvalues_add_le
• Source of LinearMap.IsSymmetric.eigenvalues_add_le in TauCeti/Analysis/InnerProductSpace/CourantFischer.lean

LeanLinearMap.IsSymmetric.eigenvalues_add_le · LinearMap.IsSymmetric.le_eigenvalues_add

Used by 1

Used byWeyl's additive inequality for Hermitian matrices, upper form

TheoremWeyl's inequality#

Weyl's inequality for symmetric operators on a finite-dimensional inner product space over 𝕜 = ℝ, ℂ: the k-th (decreasingly sorted) eigenvalues of T and S differ by at most the operator norm of T − S.

At LinearMap level there is no operator norm, so the bound is supplied as the pointwise hypothesis ∀ x, ‖(T − S) x‖ ≤ ε * ‖x‖; see LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le_norm for the continuous-linear-map operator-norm form.

Horn & Johnson, Matrix Analysis 2nd ed., Theorem 4.3.1; Bhatia, Matrix Analysis, Corollary III.2.6.

LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E]
  {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {ε : ℝ}
  (hε : ∀ (x : E), ‖(T - S) x‖ ≤ ε * ‖x‖) (k : Fin n) :
  |hT.eigenvalues hn k - hS.eigenvalues hn k| ≤ ε

Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le.

Other forms

Weyl's inequality. Formalized in Tau Ceti as LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le_norm.

LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le_norm.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} [FiniteDimensional 𝕜 E]
  {T S : E →L[𝕜] E} (hT : (↑T).IsSymmetric) (hS : (↑S).IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (k : Fin n) : |hT.eigenvalues hn k - hS.eigenvalues hn k| ≤ ‖T - S‖

Sources

• Tau Ceti documentation: LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le
• Source of LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le in TauCeti/Analysis/InnerProductSpace/CourantFischer.lean

LeanLinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le · LinearMap.IsSymmetric.abs_eigenvalue_sub_eigenvalue_le_norm

Uses 1 · Used by 3

Proof usesCourant–Fischer, lower direction

Used byPopulation-gap sine theorem for arbitrary ordered eigenframes · The Yu–Wang–Samworth overlap bound, Frobenius form · Weyl's perturbation bound for ordered eigenvalues of Hermitian matrices

TheoremWeyl's lemma for continuous functions#

A function continuous on the open set Ω is harmonic on Ω if and only if it is weakly harmonic there: ∫ Δφ • u ∂μ = 0 for every test function φ ∈ 𝓓(Ω).

TauCeti.harmonicOnNhd_iff_weaklyHarmonicOn.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E}
  {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {w : E → F}
  [BorelSpace E] [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F] (hu : ContinuousOn w ↑Ω) :
  InnerProductSpace.HarmonicOnNhd w ↑Ω ↔ TauCeti.WeaklyHarmonicOn μ Ω w

Lean

Formalized in Tau Ceti as TauCeti.harmonicOnNhd_iff_weaklyHarmonicOn.

Other forms

Weyl's lemma with finite-dimensional coefficients. Formalized in Tau Ceti as TauCeti.WeaklyHarmonicOn.exists_harmonicOnNhd_ae_eq.

TauCeti.WeaklyHarmonicOn.exists_harmonicOnNhd_ae_eq.{u_1, u_2} {E : Type u_1} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] {μ : MeasureTheory.Measure E}
  {Ω : TopologicalSpace.Opens E} {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {w : E → F}
  [BorelSpace E] [μ.IsAddHaarMeasure] [FiniteDimensional ℝ F]
  (hw : TauCeti.WeaklyHarmonicOn μ Ω w) :
  ∃ v, InnerProductSpace.HarmonicOnNhd v ↑Ω ∧ w =ᵐ[μ.restrict ↑Ω] v

Sources

• Tau Ceti documentation: TauCeti.harmonicOnNhd_iff_weaklyHarmonicOn
• Source of TauCeti.harmonicOnNhd_iff_weaklyHarmonicOn in TauCeti/Analysis/InnerProductSpace/Harmonic/Weyl.lean

LeanTauCeti.harmonicOnNhd_iff_weaklyHarmonicOn · TauCeti.WeaklyHarmonicOn.exists_harmonicOnNhd_ae_eq

Uses 2 · Used by 3

Proof usesThe du Bois-Reymond lemma · Green's second identity against a test function

Used byWeyl's lemma for \bar∂ · The Schwarz reflection principle · The interior Schauder estimate on small balls

TheoremYoung's inequality for real inner products#

for every weight ε > 0, 2 ⟪x, y⟫ ≤ ε ‖x‖² + ε⁻¹ ‖y‖².

TauCeti.two_mul_real_inner_le_add_mul_norm_sq.{u_1} {F : Type u_1} [SeminormedAddCommGroup F]
  [InnerProductSpace ℝ F] (x y : F) {ε : ℝ} (hε : 0 < ε) :
  2 * inner ℝ x y ≤ ε * ‖x‖ ^ 2 + ε⁻¹ * ‖y‖ ^ 2

Lean

Formalized in Tau Ceti as TauCeti.two_mul_real_inner_le_add_mul_norm_sq.

Sources

• Tau Ceti documentation: TauCeti.two_mul_real_inner_le_add_mul_norm_sq
• Source of TauCeti.two_mul_real_inner_le_add_mul_norm_sq in TauCeti/Analysis/InnerProductSpace/Young.lean

LeanTauCeti.two_mul_real_inner_le_add_mul_norm_sq

Used by 1

Used byThe Caccioppoli inequality

TheoremYu–Wang–Samworth bound for left singular vectors#

A population gap in the eigenvalues of the target Gram operator gives the same cross-block bound as for right singular vectors. The eigenbases of A A† and  † include complete bases of the kernels, so no positive-rank assumption is needed.

Adapted by target-Gram duality from the left-singular population bound in YuWangSamworth2015/YuWangSamworth2015/Rectangular/Theorem4.lean in the Kitware DKPS formalization (Jon Crall and GPT 5.6 High; Apache-2.0).

LinearMap.sq_mul_sum_sum_norm_inner_self_comp_adjoint_eigenvectorBasis_sq_le_four_mul_card_mul_sq.{u_1,
    u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] (A Â : E →ₗ[𝕜] F) {Γ a â ε : ℝ} (hΓ : 0 ≤ Γ)
  (hA : ∀ (x : E), ‖A x‖ ≤ a * ‖x‖) (h : ∀ (x : E), ‖ x‖ ≤ â * ‖x‖)
  (hE : ∀ (x : E), ‖(Â - A) x‖ ≤ ε * ‖x‖) (s : Finset (Fin (Module.finrank 𝕜 F)))
  (hgap : ∀ j ∈ s, ∀ k ∉ s, Γ ≤ |⋯.eigenvalues ⋯ j - ⋯.eigenvalues ⋯ k|) :
  Γ ^ 2 * ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 ((⋯.eigenvectorBasis ⋯) k) ((⋯.eigenvectorBasis ⋯) j)‖ ^ 2 ≤
    4 * ↑s.card * ((a + â) * ε) ^ 2

Lean

Formalized in Tau Ceti as LinearMap.sq_mul_sum_sum_norm_inner_self_comp_adjoint_eigenvectorBasis_sq_le_four_mul_card_mul_sq.

Other forms

Yu–Wang–Samworth bound for right singular vectors. Formalized in Tau Ceti as LinearMap.sq_mul_sum_sum_norm_inner_rightSingularBasis_sq_le_four_mul_card_mul_sq.

LinearMap.sq_mul_sum_sum_norm_inner_rightSingularBasis_sq_le_four_mul_card_mul_sq.{u_1, u_2, u_3}
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E]
  [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F]
  [FiniteDimensional 𝕜 F] (A Â : E →ₗ[𝕜] F) {Γ a â ε : ℝ} (hΓ : 0 ≤ Γ)
  (hA : ∀ (x : E), ‖A x‖ ≤ a * ‖x‖) (h : ∀ (x : E), ‖ x‖ ≤ â * ‖x‖)
  (hE : ∀ (x : E), ‖(Â - A) x‖ ≤ ε * ‖x‖) (s : Finset (Fin (Module.finrank 𝕜 E)))
  (hgap : ∀ j ∈ s, ∀ k ∉ s, Γ ≤ |A.singularValues ↑j ^ 2 - A.singularValues ↑k ^ 2|) :
  Γ ^ 2 * ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 (A.rightSingularBasis k) (Â.rightSingularBasis j)‖ ^ 2 ≤
    4 * ↑s.card * ((a + â) * ε) ^ 2

Sources

• Tau Ceti documentation: LinearMap.sq_mul_sum_sum_norm_inner_self_comp_adjoint_eigenvectorBasis_sq_le_four_mul_card_mul_sq
• Source of LinearMap.sq_mul_sum_sum_norm_inner_self_comp_adjoint_eigenvectorBasis_sq_le_four_mul_card_mul_sq in TauCeti/Analysis/InnerProductSpace/YuWangSamworth/SingularVectors.lean

LeanLinearMap.sq_mul_sum_sum_norm_inner_self_comp_adjoint_eigenvectorBasis_sq_le_four_mul_card_mul_sq · LinearMap.sq_mul_sum_sum_norm_inner_rightSingularBasis_sq_le_four_mul_card_mul_sq

Uses 1

Proof usesThe Yu–Wang–Samworth overlap bound, Frobenius form

TheoremThe Yu–Wang–Samworth overlap bound, Frobenius form#

If Δ ≥ 0 separates the eigenvalues of the population operator T indexed by s from the remaining ones, then the eigenvectors uⱼ of the perturbation S satisfy Δ² ∑_{j ∈ s} ∑_{k ∉ s} |⟪vₖ, uⱼ⟫|² ≤ 4 ‖S - T‖_F². No gap is assumed in the spectrum of S.

LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_frobenius_sq.{u_1, u_2}
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hS : S.IsSymmetric)
  (hn : Module.finrank 𝕜 E = n) {Δ : ℝ} (hΔ : 0 ≤ Δ) {s : Finset (Fin n)}
  (hgap : ∀ j ∈ s, ∀ k ∉ s, Δ ≤ |hT.eigenvalues hn j - hT.eigenvalues hn k|) :
  Δ ^ 2 *
      ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 ((hT.eigenvectorBasis hn) k) ((hS.eigenvectorBasis hn) j)‖ ^ 2 ≤
    4 * (TauCeti.UnitarilyInvariantSeminorm.frobenius 𝕜 E E) (S - T) ^ 2

Lean

Formalized in Tau Ceti as LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_frobenius_sq.

Other forms

The Yu–Wang–Samworth overlap bound, operator-norm form. Formalized in Tau Ceti as LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_card_mul_sq.

LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_card_mul_sq.{u_1, u_2} {𝕜 : Type u_1}
  {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E]
  {T S : E →ₗ[𝕜] E} {n : ℕ} (hT : T.IsSymmetric) (hS : S.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  {Δ : ℝ} (hΔ : 0 ≤ Δ) {s : Finset (Fin n)}
  (hgap : ∀ j ∈ s, ∀ k ∉ s, Δ ≤ |hT.eigenvalues hn j - hT.eigenvalues hn k|) {ε : ℝ}
  (hε : ∀ (x : E), ‖(S - T) x‖ ≤ ε * ‖x‖) :
  Δ ^ 2 *
      ∑ j ∈ s, ∑ k ∈ sᶜ, ‖inner 𝕜 ((hT.eigenvectorBasis hn) k) ((hS.eigenvectorBasis hn) j)‖ ^ 2 ≤
    4 * ↑s.card * ε ^ 2

Sources

• Tau Ceti documentation: LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_frobenius_sq
• Source of LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_frobenius_sq in TauCeti/Analysis/InnerProductSpace/YuWangSamworth/Basic.lean

LeanLinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_frobenius_sq · LinearMap.IsSymmetric.sq_mul_sum_sum_norm_inner_sq_le_four_mul_card_mul_sq

Uses 2 · Used by 1

Proof usesThe Frobenius upper residual bound · Weyl's inequality

Used byYu–Wang–Samworth bound for left singular vectors

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.