Properties of inner product spaces #

This file proves many basic properties of inner product spaces (real or complex).

Main results #

inner_mul_inner_self_le: the Cauchy-Schwartz inequality (one of many variants).
norm_inner_eq_norm_iff: the equality criteion in the Cauchy-Schwartz inequality (also in many variants).
inner_eq_sum_norm_sq_div_four: the polarization identity.
We show that the inner product is continuous, continuous_inner, and bundle it as the continuous sesquilinear map innerSL (see also innerₛₗ for the non-continuous version).

Tags #

inner product space, Hilbert space, norm

@[simp]

theorem inner_conj_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

(starRingEnd 𝕜) (inner y x) = inner x y

source

theorem real_inner_comm {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner y x = inner x y

source

theorem inner_eq_zero_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} :

inner x y = 0 ↔ inner y x = 0

source

@[simp]

theorem inner_self_im {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

RCLike.im (inner x x) = 0

source

theorem inner_add_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y z : E) :

inner (x + y) z = inner x z + inner y z

source

theorem inner_add_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y z : E) :

inner x (y + z) = inner x y + inner x z

source

theorem inner_re_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

RCLike.re (inner x y) = RCLike.re (inner y x)

source

theorem inner_im_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

RCLike.im (inner x y) = -RCLike.im (inner y x)

source

theorem inner_smul_left_eq_star_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {𝕝 : Type u_4} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] [StarModule 𝕝 𝕜] (x y : E) (r : 𝕝) :

inner (r • x) y = (starRingEnd 𝕝) r • inner x y

See inner_smul_left for the common special when 𝕜 = 𝕝.

source

theorem inner_smul_left_eq_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {𝕝 : Type u_4} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] [StarModule 𝕝 𝕜] [TrivialStar 𝕝] (x y : E) (r : 𝕝) :

inner (r • x) y = r • inner x y

Special case of inner_smul_left_eq_star_smul when the acting ring has a trivial star (eg ℕ, ℤ, ℚ≥0, ℚ, ℝ).

source

theorem inner_smul_right_eq_smul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {𝕝 : Type u_4} [CommSemiring 𝕝] [StarRing 𝕝] [Algebra 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] [StarModule 𝕝 𝕜] (x y : E) (r : 𝕝) :

inner x (r • y) = r • inner x y

See inner_smul_right for the common special when 𝕜 = 𝕝.

source

theorem inner_smul_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) (r : 𝕜) :

inner (r • x) y = (starRingEnd 𝕜) r * inner x y

See inner_smul_left_eq_star_smul for the case of a general algebra action.

source

theorem real_inner_smul_left {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) (r : ℝ) :

inner (r • x) y = r * inner x y

source

theorem inner_smul_real_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) (r : ℝ) :

inner (↑r • x) y = r • inner x y

source

theorem inner_smul_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) (r : 𝕜) :

inner x (r • y) = r * inner x y

See inner_smul_right_eq_smul for the case of a general algebra action.

source

theorem real_inner_smul_right {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) (r : ℝ) :

inner x (r • y) = r * inner x y

source

theorem inner_smul_real_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) (r : ℝ) :

inner x (↑r • y) = r • inner x y

source

def sesqFormOfInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜

The inner product as a sesquilinear form.

Note that in the case 𝕜 = ℝ this is a bilinear form.

Equations

sesqFormOfInner = LinearMap.mk₂'ₛₗ (RingHom.id 𝕜) (starRingEnd 𝕜) (fun (x y : E) => inner y x) ⋯ ⋯ ⋯ ⋯

Instances For

source

@[simp]

theorem sesqFormOfInner_apply_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (m y : E) :

(sesqFormOfInner m) y = inner y m

source

def bilinFormOfRealInner {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] :

LinearMap.BilinForm ℝ F

The real inner product as a bilinear form.

Note that unlike sesqFormOfInner, this does not reverse the order of the arguments.

Equations

bilinFormOfRealInner = sesqFormOfInner.flip

Instances For

source

@[simp]

theorem bilinFormOfRealInner_apply_apply {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (m m✝ : F) :

(bilinFormOfRealInner m) m✝ = inner m m✝

source

theorem sum_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E) :

inner (∑ i ∈ s, f i) x = ∑ i ∈ s, inner (f i) x

An inner product with a sum on the left.

source

theorem inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (s : Finset ι) (f : ι → E) (x : E) :

inner x (∑ i ∈ s, f i) = ∑ i ∈ s, inner x (f i)

An inner product with a sum on the right.

source

theorem Finsupp.sum_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :

inner (l.sum fun (i : ι) (a : 𝕜) => a • v i) x = l.sum fun (i : ι) (a : 𝕜) => (starRingEnd 𝕜) a • inner (v i) x

An inner product with a sum on the left, Finsupp version.

source

theorem Finsupp.inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (l : ι →₀ 𝕜) (v : ι → E) (x : E) :

inner x (l.sum fun (i : ι) (a : 𝕜) => a • v i) = l.sum fun (i : ι) (a : 𝕜) => a • inner x (v i)

An inner product with a sum on the right, Finsupp version.

source

theorem DFinsupp.sum_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {α : ι → Type u_5} [(i : ι) → AddZeroClass (α i)] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] (f : (i : ι) → α i → E) (l : Π₀ (i : ι), α i) (x : E) :

inner (l.sum f) x = l.sum fun (i : ι) (a : α i) => inner (f i a) x

source

theorem DFinsupp.inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {α : ι → Type u_5} [(i : ι) → AddZeroClass (α i)] [(i : ι) → (x : α i) → Decidable (x ≠ 0)] (f : (i : ι) → α i → E) (l : Π₀ (i : ι), α i) (x : E) :

inner x (l.sum f) = l.sum fun (i : ι) (a : α i) => inner x (f i a)

source

@[simp]

theorem inner_zero_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

inner 0 x = 0

source

theorem inner_re_zero_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

RCLike.re (inner 0 x) = 0

source

@[simp]

theorem inner_zero_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

inner x 0 = 0

source

theorem inner_re_zero_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

RCLike.re (inner x 0) = 0

source

theorem inner_self_nonneg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} :

0 ≤ RCLike.re (inner x x)

source

theorem real_inner_self_nonneg {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} :

0 ≤ inner x x

source

@[simp]

theorem inner_self_ofReal_re {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

↑(RCLike.re (inner x x)) = inner x x

source

theorem inner_self_eq_norm_sq_to_K {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

inner x x = ↑‖x‖ ^ 2

source

theorem inner_self_re_eq_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

RCLike.re (inner x x) = ‖inner x x‖

source

theorem inner_self_ofReal_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

↑‖inner x x‖ = inner x x

source

theorem real_inner_self_abs {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) :

|inner x x| = inner x x

source

theorem norm_inner_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖inner x y‖ = ‖inner y x‖

source

@[simp]

theorem inner_neg_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

inner (-x) y = -inner x y

source

@[simp]

theorem inner_neg_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

inner x (-y) = -inner x y

source

theorem inner_neg_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

inner (-x) (-y) = inner x y

source

theorem inner_self_conj {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

(starRingEnd 𝕜) (inner x x) = inner x x

source

theorem inner_sub_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y z : E) :

inner (x - y) z = inner x z - inner y z

source

theorem inner_sub_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y z : E) :

inner x (y - z) = inner x y - inner x z

source

theorem inner_mul_symm_re_eq_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

RCLike.re (inner x y * inner y x) = ‖inner x y * inner y x‖

source

theorem inner_add_add_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

inner (x + y) (x + y) = inner x x + inner x y + inner y x + inner y y

Expand ⟪x + y, x + y⟫

source

theorem real_inner_add_add_self {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner (x + y) (x + y) = inner x x + 2 * inner x y + inner y y

Expand ⟪x + y, x + y⟫_ℝ

source

theorem inner_sub_sub_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

inner (x - y) (x - y) = inner x x - inner x y - inner y x + inner y y

source

theorem real_inner_sub_sub_self {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner (x - y) (x - y) = inner x x - 2 * inner x y + inner y y

Expand ⟪x - y, x - y⟫_ℝ

source

theorem parallelogram_law {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} :

inner (x + y) (x + y) + inner (x - y) (x - y) = 2 * (inner x x + inner y y)

Parallelogram law

source

theorem inner_mul_inner_self_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖inner x y‖ * ‖inner y x‖ ≤ RCLike.re (inner x x) * RCLike.re (inner y y)

Cauchy–Schwarz inequality.

source

theorem real_inner_mul_inner_self_le {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner x y * inner x y ≤ inner x x * inner y y

Cauchy–Schwarz inequality for real inner products.

source

@[simp]

theorem inner_self_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} :

inner x x = 0 ↔ x = 0

source

theorem inner_self_ne_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} :

inner x x ≠ 0 ↔ x ≠ 0

source

theorem ext_inner_left (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} (h : ∀ (v : E), inner v x = inner v y) :

x = y

source

theorem ext_inner_right (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} (h : ∀ (v : E), inner x v = inner y v) :

x = y

source

@[simp]

theorem inner_self_nonpos {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} :

RCLike.re (inner x x) ≤ 0 ↔ x = 0

source

theorem real_inner_self_nonpos {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} :

inner x x ≤ 0 ↔ x = 0

source

theorem linearIndependent_of_ne_zero_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hz : ∀ (i : ι), v i ≠ 0) (ho : Pairwise fun (i j : ι) => inner (v i) (v j) = 0) :

LinearIndependent 𝕜 v

A family of vectors is linearly independent if they are nonzero and orthogonal.

source

theorem norm_eq_sqrt_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

‖x‖ = √(RCLike.re (inner x x))

source

theorem norm_eq_sqrt_real_inner {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) :

‖x‖ = √(inner x x)

source

theorem inner_self_eq_norm_mul_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

RCLike.re (inner x x) = ‖x‖ * ‖x‖

source

theorem inner_self_eq_norm_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

RCLike.re (inner x x) = ‖x‖ ^ 2

source

theorem real_inner_self_eq_norm_mul_norm {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) :

inner x x = ‖x‖ * ‖x‖

source

theorem real_inner_self_eq_norm_sq {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) :

inner x x = ‖x‖ ^ 2

source

theorem norm_add_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re (inner x y) + ‖y‖ ^ 2

Expand the square

source

theorem norm_add_pow_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re (inner x y) + ‖y‖ ^ 2

Alias of norm_add_sq.

Expand the square

source

theorem norm_add_sq_real {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2

Expand the square

source

theorem norm_add_pow_two_real {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2

Alias of norm_add_sq_real.

Expand the square

source

theorem norm_add_mul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * RCLike.re (inner x y) + ‖y‖ * ‖y‖

Expand the square

source

theorem norm_add_mul_self_real {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + 2 * inner x y + ‖y‖ * ‖y‖

Expand the square

source

theorem norm_sub_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re (inner x y) + ‖y‖ ^ 2

Expand the square

source

theorem norm_sub_pow_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * RCLike.re (inner x y) + ‖y‖ ^ 2

Alias of norm_sub_sq.

Expand the square

source

theorem norm_sub_sq_real {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2

Expand the square

source

theorem norm_sub_pow_two_real {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

‖x - y‖ ^ 2 = ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2

Alias of norm_sub_sq_real.

Expand the square

source

theorem norm_sub_mul_self {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * RCLike.re (inner x y) + ‖y‖ * ‖y‖

Expand the square

source

theorem norm_sub_mul_self_real {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * inner x y + ‖y‖ * ‖y‖

Expand the square

source

theorem norm_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖inner x y‖ ≤ ‖x‖ * ‖y‖

Cauchy–Schwarz inequality with norm

source

theorem nnnorm_inner_le_nnnorm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖inner x y‖₊ ≤ ‖x‖₊ * ‖y‖₊

source

theorem re_inner_le_norm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

RCLike.re (inner x y) ≤ ‖x‖ * ‖y‖

source

theorem abs_real_inner_le_norm {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

|inner x y| ≤ ‖x‖ * ‖y‖

Cauchy–Schwarz inequality with norm

source

theorem real_inner_le_norm {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner x y ≤ ‖x‖ * ‖y‖

Cauchy–Schwarz inequality with norm

source

theorem inner_eq_zero_of_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} (y : E) (h : ‖x‖ = 0) :

inner x y = 0

source

theorem inner_eq_zero_of_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) {y : E} (h : ‖y‖ = 0) :

inner x y = 0

source

theorem parallelogram_law_with_norm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)

source

theorem parallelogram_law_with_nnnorm (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖x + y‖₊ * ‖x + y‖₊ + ‖x - y‖₊ * ‖x - y‖₊ = 2 * (‖x‖₊ * ‖x‖₊ + ‖y‖₊ * ‖y‖₊)

source

theorem re_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

RCLike.re (inner x y) = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

Polarization identity: The real part of the inner product, in terms of the norm.

source

theorem re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

RCLike.re (inner x y) = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

Polarization identity: The real part of the inner product, in terms of the norm.

source

theorem re_inner_eq_norm_add_mul_self_sub_norm_sub_mul_self_div_four {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

RCLike.re (inner x y) = (‖x + y‖ * ‖x + y‖ - ‖x - y‖ * ‖x - y‖) / 4

Polarization identity: The real part of the inner product, in terms of the norm.

source

theorem im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

RCLike.im (inner x y) = (‖x - RCLike.I • y‖ * ‖x - RCLike.I • y‖ - ‖x + RCLike.I • y‖ * ‖x + RCLike.I • y‖) / 4

Polarization identity: The imaginary part of the inner product, in terms of the norm.

source

theorem inner_eq_sum_norm_sq_div_four {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

inner x y = (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + (↑‖x - RCLike.I • y‖ ^ 2 - ↑‖x + RCLike.I • y‖ ^ 2) * RCLike.I) / 4

Polarization identity: The inner product, in terms of the norm.

source

@[instance 100]

instance InnerProductSpace.toUniformConvexSpace {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] :

UniformConvexSpace F

source

theorem real_inner_eq_norm_add_mul_self_sub_norm_mul_self_sub_norm_mul_self_div_two {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner x y = (‖x + y‖ * ‖x + y‖ - ‖x‖ * ‖x‖ - ‖y‖ * ‖y‖) / 2

Polarization identity: The real inner product, in terms of the norm.

source

theorem real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner x y = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

Polarization identity: The real inner product, in terms of the norm.

source

theorem norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ inner x y = 0

Pythagorean theorem, if-and-only-if vector inner product form.

source

theorem norm_add_eq_sqrt_iff_real_inner_eq_zero {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} :

‖x + y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ inner x y = 0

Pythagorean theorem, if-and-if vector inner product form using square roots.

source

theorem norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) (h : inner x y = 0) :

‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Pythagorean theorem, vector inner product form.

source

theorem norm_add_sq_eq_norm_sq_add_norm_sq_real {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} (h : inner x y = 0) :

‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Pythagorean theorem, vector inner product form.

source

theorem norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ inner x y = 0

Pythagorean theorem, subtracting vectors, if-and-only-if vector inner product form.

source

theorem norm_sub_eq_sqrt_iff_real_inner_eq_zero {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} :

‖x - y‖ = √(‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) ↔ inner x y = 0

Pythagorean theorem, subtracting vectors, if-and-if vector inner product form using square roots.

source

theorem norm_sub_sq_eq_norm_sq_add_norm_sq_real {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} (h : inner x y = 0) :

‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Pythagorean theorem, subtracting vectors, vector inner product form.

source

theorem real_inner_add_sub_eq_zero_iff {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner (x + y) (x - y) = 0 ↔ ‖x‖ = ‖y‖

The sum and difference of two vectors are orthogonal if and only if they have the same norm.

source

theorem norm_sub_eq_norm_add {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v w : E} (h : inner v w = 0) :

‖w - v‖ = ‖w + v‖

Given two orthogonal vectors, their sum and difference have equal norms.

source

theorem abs_real_inner_div_norm_mul_norm_le_one {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

|inner x y / (‖x‖ * ‖y‖)| ≤ 1

The real inner product of two vectors, divided by the product of their norms, has absolute value at most 1.

source

theorem real_inner_smul_self_left {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (r : ℝ) :

inner (r • x) x = r * (‖x‖ * ‖x‖)

The inner product of a vector with a multiple of itself.

source

theorem real_inner_smul_self_right {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] (x : F) (r : ℝ) :

inner x (r • x) = r * (‖x‖ * ‖x‖)

The inner product of a vector with a multiple of itself.

source

theorem isBoundedBilinearMap_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedSpace ℝ E] [IsScalarTower ℝ 𝕜 E] :

IsBoundedBilinearMap ℝ fun (p : E × E) => inner p.1 p.2

When an inner product space E over 𝕜 is considered as a real normed space, its inner product satisfies IsBoundedBilinearMap.

In order to state these results, we need a NormedSpace ℝ E instance. We will later establish such an instance by restriction-of-scalars, InnerProductSpace.rclikeToReal 𝕜 E, but this instance may be not definitionally equal to some other “natural” instance. So, we assume [NormedSpace ℝ E].

source

theorem inner_sum_smul_sum_smul_of_sum_eq_zero {F : Type u_3} [SeminormedAddCommGroup F] [InnerProductSpace ℝ F] {ι₁ : Type u_4} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (v₁ : ι₁ → F) (h₁ : ∑ i ∈ s₁, w₁ i = 0) {ι₂ : Type u_5} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (v₂ : ι₂ → F) (h₂ : ∑ i ∈ s₂, w₂ i = 0) :

inner (∑ i₁ ∈ s₁, w₁ i₁ • v₁ i₁) (∑ i₂ ∈ s₂, w₂ i₂ • v₂ i₂) = (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2

The inner product of two weighted sums, where the weights in each sum add to 0, in terms of the norms of pairwise differences.

source

theorem dist_div_norm_sq_smul {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) (R : ℝ) :

dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y

Formula for the distance between the images of two nonzero points under an inversion with center zero. See also EuclideanGeometry.dist_inversion_inversion for inversions around a general point.

source

theorem norm_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x : E} {r : 𝕜} (hx : x ≠ 0) (hr : r ≠ 0) :

‖inner x (r • x)‖ / (‖x‖ * ‖r • x‖) = 1

The inner product of a nonzero vector with a nonzero multiple of itself, divided by the product of their norms, has absolute value

source

theorem abs_real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_ne_zero_mul {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r ≠ 0) :

|inner x (r • x)| / (‖x‖ * ‖r • x‖) = 1

The inner product of a nonzero vector with a nonzero multiple of itself, divided by the product of their norms, has absolute value

source

theorem real_inner_div_norm_mul_norm_eq_one_of_ne_zero_of_pos_mul {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : 0 < r) :

inner x (r • x) / (‖x‖ * ‖r • x‖) = 1

The inner product of a nonzero vector with a positive multiple of itself, divided by the product of their norms, has value 1.

source

theorem real_inner_div_norm_mul_norm_eq_neg_one_of_ne_zero_of_neg_mul {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x : F} {r : ℝ} (hx : x ≠ 0) (hr : r < 0) :

inner x (r • x) / (‖x‖ * ‖r • x‖) = -1

The inner product of a nonzero vector with a negative multiple of itself, divided by the product of their norms, has value -1.

source

theorem norm_inner_eq_norm_tfae {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

[‖inner x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner x y / inner x x) • x, x = 0 ∨ ∃ (r : 𝕜), y = r • x, x = 0 ∨ y ∈ Submodule.span 𝕜 {x}].TFAE

source

theorem norm_inner_eq_norm_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :

‖inner x y‖ = ‖x‖ * ‖y‖ ↔ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x

If the inner product of two vectors is equal to the product of their norms, then the two vectors are multiples of each other. One form of the equality case for Cauchy-Schwarz. Compare inner_eq_norm_mul_iff, which takes the stronger hypothesis ⟪x, y⟫ = ‖x‖ * ‖y‖.

source

theorem norm_inner_div_norm_mul_norm_eq_one_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

‖inner x y / (↑‖x‖ * ↑‖y‖)‖ = 1 ↔ x ≠ 0 ∧ ∃ (r : 𝕜), r ≠ 0 ∧ y = r • x

The inner product of two vectors, divided by the product of their norms, has absolute value 1 if and only if they are nonzero and one is a multiple of the other. One form of equality case for Cauchy-Schwarz.

source

theorem abs_real_inner_div_norm_mul_norm_eq_one_iff {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

|inner x y / (‖x‖ * ‖y‖)| = 1 ↔ x ≠ 0 ∧ ∃ (r : ℝ), r ≠ 0 ∧ y = r • x

source

theorem inner_eq_norm_mul_iff_div {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} (h₀ : x ≠ 0) :

inner x y = ↑‖x‖ * ↑‖y‖ ↔ (↑‖y‖ / ↑‖x‖) • x = y

source

theorem inner_eq_norm_mul_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} :

inner x y = ↑‖x‖ * ↑‖y‖ ↔ ↑‖y‖ • x = ↑‖x‖ • y

If the inner product of two vectors is equal to the product of their norms (i.e., ⟪x, y⟫ = ‖x‖ * ‖y‖), then the two vectors are nonnegative real multiples of each other. One form of the equality case for Cauchy-Schwarz. Compare norm_inner_eq_norm_iff, which takes the weaker hypothesis abs ⟪x, y⟫ = ‖x‖ * ‖y‖.

source

theorem inner_eq_norm_mul_iff_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} :

inner x y = ‖x‖ * ‖y‖ ↔ ‖y‖ • x = ‖x‖ • y

source

theorem real_inner_div_norm_mul_norm_eq_one_iff {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner x y / (‖x‖ * ‖y‖) = 1 ↔ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x

The inner product of two vectors, divided by the product of their norms, has value 1 if and only if they are nonzero and one is a positive multiple of the other.

source

theorem real_inner_div_norm_mul_norm_eq_neg_one_iff {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (x y : F) :

inner x y / (‖x‖ * ‖y‖) = -1 ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

The inner product of two vectors, divided by the product of their norms, has value -1 if and only if they are nonzero and one is a negative multiple of the other.

source

theorem inner_eq_one_iff_of_norm_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :

inner x y = 1 ↔ x = y

If the inner product of two unit vectors is 1, then the two vectors are equal. One form of the equality case for Cauchy-Schwarz.

source

theorem inner_lt_norm_mul_iff_real {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} :

inner x y < ‖x‖ * ‖y‖ ↔ ‖y‖ • x ≠ ‖x‖ • y

source

theorem inner_lt_one_iff_real_of_norm_one {F : Type u_3} [NormedAddCommGroup F] [InnerProductSpace ℝ F] {x y : F} (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) :

inner x y < 1 ↔ x ≠ y

If the inner product of two unit vectors is strictly less than 1, then the two vectors are distinct. One form of the equality case for Cauchy-Schwarz.

source

theorem eq_of_norm_le_re_inner_eq_norm_sq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x y : E} (hle : ‖x‖ ≤ ‖y‖) (h : RCLike.re (inner x y) = ‖y‖ ^ 2) :

x = y

The sphere of radius r = ‖y‖ is tangent to the plane ⟪x, y⟫ = ‖y‖ ^ 2 at x = y.

source

instance RCLike.innerProductSpace {𝕜 : Type u_1} [RCLike 𝕜] :

InnerProductSpace 𝕜 𝕜

A field 𝕜 satisfying RCLike is itself a 𝕜-inner product space.

Equations

RCLike.innerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

source

@[simp]

theorem RCLike.inner_apply {𝕜 : Type u_1} [RCLike 𝕜] (x y : 𝕜) :

inner x y = (starRingEnd 𝕜) x * y

source

def Inner.rclikeToReal (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

Inner ℝ E

A general inner product implies a real inner product. This is not registered as an instance since 𝕜 does not appear in the return type Inner ℝ E.

Equations

Inner.rclikeToReal 𝕜 E = { inner := fun (x y : E) => RCLike.re (inner x y) }

Instances For

source

@[reducible, inline]

abbrev InnerProductSpace.rclikeToReal (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

InnerProductSpace ℝ E

A general inner product space structure implies a real inner product structure.

This is not registered as an instance since

𝕜 does not appear in the return type InnerProductSpace ℝ E,
It is likely to create instance diamonds, as it builds upon the diamond-prone NormedSpace.restrictScalars.

However, it can be used in a proof to obtain a real inner product space structure from a given 𝕜-inner product space structure.

Equations

InnerProductSpace.rclikeToReal 𝕜 E = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

Instances For

source

theorem real_inner_eq_re_inner (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) :

inner x y = RCLike.re (inner x y)

source

theorem real_inner_I_smul_self (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x : E) :

inner x (RCLike.I • x) = 0

source

def InnerProductSpace.complexToReal {G : Type u_4} [SeminormedAddCommGroup G] [InnerProductSpace ℂ G] :

InnerProductSpace ℝ G

A complex inner product implies a real inner product. This cannot be an instance since it creates a diamond with PiLp.innerProductSpace because re (sum i, inner (x i) (y i)) and sum i, re (inner (x i) (y i)) are not defeq.

Equations

InnerProductSpace.complexToReal = InnerProductSpace.rclikeToReal ℂ G

Instances For

source

instance instInnerProductSpaceRealComplex :

InnerProductSpace ℝ ℂ

Equations

instInnerProductSpaceRealComplex = InnerProductSpace.complexToReal

source

@[simp]

theorem Complex.inner (w z : ℂ) :

inner w z = ((starRingEnd ℂ) w * z).re

source

noncomputable instance RCLike.toInnerProductSpaceReal {𝕜 : Type u_1} [RCLike 𝕜] :

InnerProductSpace ℝ 𝕜

An RCLike field is a real inner product space.

Equations

RCLike.toInnerProductSpaceReal = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

Continuity of the inner product #

source

theorem continuous_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :

Continuous fun (p : E × E) => inner p.1 p.2

source

theorem Filter.Tendsto.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} {f g : α → E} {l : Filter α} {x y : E} (hf : Filter.Tendsto f l (nhds x)) (hg : Filter.Tendsto g l (nhds y)) :

Filter.Tendsto (fun (t : α) => inner (f t) (g t)) l (nhds (inner x y))

source

theorem ContinuousWithinAt.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f g : α → E} {x : α} {s : Set α} (hf : ContinuousWithinAt f s x) (hg : ContinuousWithinAt g s x) :

ContinuousWithinAt (fun (t : α) => inner (f t) (g t)) s x

source

theorem ContinuousAt.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f g : α → E} {x : α} (hf : ContinuousAt f x) (hg : ContinuousAt g x) :

ContinuousAt (fun (t : α) => inner (f t) (g t)) x

source

theorem ContinuousOn.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f g : α → E} {s : Set α} (hf : ContinuousOn f s) (hg : ContinuousOn g s) :

ContinuousOn (fun (t : α) => inner (f t) (g t)) s

source

theorem Continuous.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f g : α → E} (hf : Continuous f) (hg : Continuous g) :

Continuous fun (t : α) => inner (f t) (g t)

Documentation

Mathlib.Analysis.InnerProductSpace.Basic

Properties of inner product spaces #

Main results #

Tags #

Continuity of the inner product #