Recovered helper lemmas for the numerical range

These lemmas reconstruct identities lost during the accidental deletion. They support the recovered convexity and spectrum-inclusion proofs.

theorem norm_inv_norm_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {x : E} (hx : x ≠ 0) : ‖(↑‖x‖)⁻¹ • x‖ = 1

theorem inner_apply_real_smul_add_real_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (x₀ x₁ : E) (ω : ℂ) (u v : ℝ) : inner ℂ (↑u • x₀ + ↑v • ω • x₁) (A (↑u • x₀ + ↑v • ω • x₁)) = ↑u ^ 2 * inner ℂ x₀ (A x₀) + ↑(u * v) * (ω * inner ℂ x₀ (A x₁) + (starRingEnd ℂ) ω * inner ℂ x₁ (A x₀)) + ↑v ^ 2 * ↑‖ω‖ ^ 2 * inner ℂ x₁ (A x₁)

theorem inner_apply_self_eq_of_not_linearIndependent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {x₀ x₁ : E} (hx₀ : ‖x₀‖ = 1) (hx₁ : ‖x₁‖ = 1) (h : ¬LinearIndependent ℂ ![x₀, x₁]) : inner ℂ x₀ (A x₀) = inner ℂ x₁ (A x₁)

theorem inner_smul_sub_smul_one_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (c z₀ : ℂ) (A : E →L[ℂ] E) {x : E} (hx : ‖x‖ = 1) : inner ℂ x ((c • (A - z₀ • 1)) x) = c * (inner ℂ x (A x) - z₀)

theorem inner_sub_smul_one_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) (l : ℂ) {x : E} (hx : ‖x‖ = 1) : inner ℂ x ((A - l • 1) x) = inner ℂ x (A x) - l

theorem smul_add_smul_mem_numericalRange_of_mem_normalized {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {z₀ z₁ : ℂ} (hz : z₀ ≠ z₁) {a b : ℝ} (hab : a + b = 1) (hb : ↑b ∈ numericalRange ((z₁ - z₀)⁻¹ • (A - z₀ • 1))) : a • z₀ + b • z₁ ∈ numericalRange A

theorem inner_inv_norm_smul_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (A : E →L[ℂ] E) {x : E} (hx : x ≠ 0) : inner ℂ ((↑‖x‖)⁻¹ • x) (A ((↑‖x‖)⁻¹ • x)) = inner ℂ x (A x) / ↑‖x‖ ^ 2