Scalar translations of the numerical radius

On a nontrivial Hilbert space, scalar operators have their expected numerical radius. Consequently scalar translation changes numerical radius by at most the modulus of the scalar, and centered numerical radii are Lipschitz in the center.

@[simp]

theorem numericalRadius_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] : numericalRadius 1 = 1

The identity operator has numerical radius one.

@[simp]

theorem numericalRadius_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (c : ℂ) : numericalRadius (c • 1) = ‖c‖

A scalar operator has numerical radius equal to the scalar modulus.

theorem abs_numericalRadius_add_smul_one_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) (c : ℂ) : |numericalRadius (A + c • 1) - numericalRadius A| ≤ ‖c‖

Adding a scalar operator changes numerical radius by at most the scalar modulus.

theorem abs_numericalRadius_sub_smul_one_sub_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) (c : ℂ) : |numericalRadius (A - c • 1) - numericalRadius A| ≤ ‖c‖

Subtracting a scalar operator changes numerical radius by at most the scalar modulus.

theorem abs_numericalRadius_sub_smul_one_sub_norm_le_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) (c : ℂ) : |numericalRadius (A - c • 1) - ‖c‖| ≤ numericalRadius A

The centered numerical radius differs from the modulus of its center by at most w(A).

theorem norm_sub_numericalRadius_le_numericalRadius_sub_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) (c : ℂ) : ‖c‖ - numericalRadius A ≤ numericalRadius (A - c • 1)

In particular, the centered numerical radius grows at least linearly in the modulus of the center.

theorem abs_numericalRadius_sub_smul_one_sub_numericalRadius_sub_smul_one_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) (c d : ℂ) : |numericalRadius (A - c • 1) - numericalRadius (A - d • 1)| ≤ ‖c - d‖

Centering at two scalars changes numerical radius by at most the distance between the centers.

theorem lipschitzWith_numericalRadius_sub_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : LipschitzWith 1 fun (c : ℂ) => numericalRadius (A - c • 1)

The numerical radius of A - cI is 1-Lipschitz as a function of the center c.

theorem continuous_numericalRadius_sub_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : Continuous fun (c : ℂ) => numericalRadius (A - c • 1)

The centered numerical radius depends continuously on the center.

theorem convexOn_numericalRadius_sub_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : ConvexOn ℝ Set.univ fun (c : ℂ) => numericalRadius (A - c • 1)

The numerical radius of the scalar translate A-cI is convex as a function of the center c.

theorem convex_setOf_numericalRadius_sub_smul_one_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (r : ℝ) : Convex ℝ {c : ℂ | numericalRadius (A - c • 1) ≤ r}

Every sublevel set of the centered numerical radius is convex.

theorem isCompact_setOf_numericalRadius_sub_smul_one_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) (r : ℝ) : IsCompact {c : ℂ | numericalRadius (A - c • 1) ≤ r}

Every sublevel set of the centered numerical radius is compact.

theorem tendsto_numericalRadius_sub_smul_one_cocompact_atTop {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : Filter.Tendsto (fun (c : ℂ) => numericalRadius (A - c • 1)) (Filter.cocompact ℂ) Filter.atTop

The centered numerical radius tends to infinity as the center leaves compact subsets of the complex plane.

theorem exists_center_minimizing_numericalRadius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : ∃ (c : ℂ), ∀ (d : ℂ), numericalRadius (A - c • 1) ≤ numericalRadius (A - d • 1)

There is a center minimizing the numerical radius of the scalar translate A-cI.

def centeredNumericalRadiusMinimizers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : Set ℂ

The set of scalar centers that globally minimize w(A-cI).

Equations

• centeredNumericalRadiusMinimizers A = {c : ℂ | ∀ (d : ℂ), numericalRadius (A - c • 1) ≤ numericalRadius (A - d • 1)}

theorem centeredNumericalRadiusMinimizers_eq_setOf_le_of_minimizer {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {c : ℂ} (hc : ∀ (d : ℂ), numericalRadius (A - c • 1) ≤ numericalRadius (A - d • 1)) : centeredNumericalRadiusMinimizers A = {d : ℂ | numericalRadius (A - d • 1) ≤ numericalRadius (A - c • 1)}

Once a minimizing center is fixed, the full minimizer set is its centered-radius sublevel set.

theorem centeredNumericalRadiusMinimizers_nonempty {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : (centeredNumericalRadiusMinimizers A).Nonempty

The set of globally minimizing scalar centers is nonempty.

theorem isCompact_centeredNumericalRadiusMinimizers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : IsCompact (centeredNumericalRadiusMinimizers A)

The set of globally minimizing scalar centers is compact.

theorem convex_centeredNumericalRadiusMinimizers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : Convex ℝ (centeredNumericalRadiusMinimizers A)

The set of globally minimizing scalar centers is convex.

theorem norm_le_two_mul_numericalRadius_of_mem_centeredMinimizers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) {c : ℂ} (hc : c ∈ centeredNumericalRadiusMinimizers A) : ‖c‖ ≤ 2 * numericalRadius A

Every globally minimizing scalar center has modulus at most 2w(A).

theorem centeredNumericalRadiusMinimizers_subset_closedBall_two_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : centeredNumericalRadiusMinimizers A ⊆ Metric.closedBall 0 (2 * numericalRadius A)

The full minimizer set lies in the explicit disk of radius 2w(A).

theorem exists_mem_centeredNumericalRadiusMinimizers_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (A : E →L[ℂ] E) : ∃ c ∈ centeredNumericalRadiusMinimizers A, ‖c‖ ≤ 2 * numericalRadius A

There is a globally minimizing center in the explicit numerical-radius disk of radius 2w(A).

theorem centeredNumericalRadiusMinimizers_add_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (b : ℂ) : centeredNumericalRadiusMinimizers (A + b • 1) = (fun (c : ℂ) => c + b) '' centeredNumericalRadiusMinimizers A

Adding bI to an operator translates every optimal center by b.

theorem centeredNumericalRadiusMinimizers_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {a : ℂ} (ha : a ≠ 0) : centeredNumericalRadiusMinimizers (a • A) = (fun (c : ℂ) => a * c) '' centeredNumericalRadiusMinimizers A

Multiplying an operator by a nonzero scalar multiplies every optimal center by the same scalar.

@[simp]

theorem centeredNumericalRadiusMinimizers_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) : centeredNumericalRadiusMinimizers (-A) = (fun (c : ℂ) => -c) '' centeredNumericalRadiusMinimizers A

Negating an operator negates every optimal scalar center.

theorem centeredNumericalRadiusMinimizers_smul_add_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {a : ℂ} (ha : a ≠ 0) (b : ℂ) : centeredNumericalRadiusMinimizers (a • A + b • 1) = (fun (c : ℂ) => a * c + b) '' centeredNumericalRadiusMinimizers A

An invertible affine change A ↦ aA+bI carries optimal centers by the same affine map.

@[simp]

theorem centeredNumericalRadiusMinimizers_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] : centeredNumericalRadiusMinimizers 0 = {0}

The zero operator has the unique optimal center zero.

@[simp]

theorem centeredNumericalRadiusMinimizers_smul_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] (c : ℂ) : centeredNumericalRadiusMinimizers (c • 1) = {c}

A scalar operator cI has the unique optimal center c.

theorem centeredNumericalRadiusMinimizers_adjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) : centeredNumericalRadiusMinimizers (ContinuousLinearMap.adjoint A) = ⇑(starRingEnd ℂ) '' centeredNumericalRadiusMinimizers A

Taking the adjoint conjugates every optimal scalar center.

theorem centeredNumericalRadiusMinimizers_unitary_conjugate {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) : centeredNumericalRadiusMinimizers (ContinuousLinearMap.adjoint U * A * U) = centeredNumericalRadiusMinimizers A

Unitary conjugation preserves every optimal scalar center.

theorem centeredNumericalRadiusMinimizers_unitary_conjugate' {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A U : E →L[ℂ] E) (hU : U ∈ unitary (E →L[ℂ] E)) : centeredNumericalRadiusMinimizers (U * A * ContinuousLinearMap.adjoint U) = centeredNumericalRadiusMinimizers A

The alternate orientation of unitary conjugation also preserves every optimal scalar center.

theorem image_starRingEnd_centeredNumericalRadiusMinimizers_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : IsSelfAdjoint A) : ⇑(starRingEnd ℂ) '' centeredNumericalRadiusMinimizers A = centeredNumericalRadiusMinimizers A

The optimal centers of a self-adjoint operator are invariant under complex conjugation.

@[simp]

theorem star_mem_centeredNumericalRadiusMinimizers_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : IsSelfAdjoint A) (c : ℂ) : (starRingEnd ℂ) c ∈ centeredNumericalRadiusMinimizers A ↔ c ∈ centeredNumericalRadiusMinimizers A

Membership among the optimal centers of a self-adjoint operator is preserved and reflected by complex conjugation.

theorem exists_real_mem_centeredNumericalRadiusMinimizers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : IsSelfAdjoint A) : ∃ (r : ℝ), ↑r ∈ centeredNumericalRadiusMinimizers A

A self-adjoint operator has a real globally optimal scalar center.

theorem exists_real_mem_centeredNumericalRadiusMinimizers_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : IsSelfAdjoint A) : ∃ (r : ℝ), ↑r ∈ centeredNumericalRadiusMinimizers A ∧ ‖↑r‖ ≤ 2 * numericalRadius A

A self-adjoint operator has a real optimal center in the explicit numerical-radius disk.

theorem exists_real_center_minimizing_numericalRadius_of_isSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : IsSelfAdjoint A) : ∃ (r : ℝ), ∀ (c : ℂ), numericalRadius (A - ↑r • 1) ≤ numericalRadius (A - c • 1)

For a self-adjoint operator, the centered numerical radius attains its global minimum at a real center.

@[simp]

theorem neg_star_mem_centeredNumericalRadiusMinimizers_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : A ∈ skewAdjoint (E →L[ℂ] E)) (c : ℂ) : -(starRingEnd ℂ) c ∈ centeredNumericalRadiusMinimizers A ↔ c ∈ centeredNumericalRadiusMinimizers A

The optimal centers of a skew-adjoint operator are preserved and reflected by reflection across the imaginary axis.

theorem image_neg_star_centeredNumericalRadiusMinimizers_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : A ∈ skewAdjoint (E →L[ℂ] E)) : (fun (c : ℂ) => -star c) '' centeredNumericalRadiusMinimizers A = centeredNumericalRadiusMinimizers A

Reflection across the imaginary axis fixes the optimal-center set of a skew-adjoint operator.

theorem exists_imaginary_mem_centeredNumericalRadiusMinimizers {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : A ∈ skewAdjoint (E →L[ℂ] E)) : ∃ (r : ℝ), ↑r * Complex.I ∈ centeredNumericalRadiusMinimizers A

A skew-adjoint operator has a purely imaginary globally optimal scalar center.

theorem exists_imaginary_mem_centeredNumericalRadiusMinimizers_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : A ∈ skewAdjoint (E →L[ℂ] E)) : ∃ (r : ℝ), ↑r * Complex.I ∈ centeredNumericalRadiusMinimizers A ∧ ‖↑r * Complex.I‖ ≤ 2 * numericalRadius A

A skew-adjoint operator has a purely imaginary optimal center in the explicit numerical-radius disk.

theorem exists_imaginary_center_minimizing_numericalRadius_of_mem_skewAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [Nontrivial E] [CompleteSpace E] (A : E →L[ℂ] E) (hA : A ∈ skewAdjoint (E →L[ℂ] E)) : ∃ (r : ℝ), ∀ (c : ℂ), numericalRadius (A - (↑r * Complex.I) • 1) ≤ numericalRadius (A - c • 1)

For a skew-adjoint operator, the centered numerical radius attains its global minimum at a purely imaginary center.