monlib / linear_algebra.of_norm

source

theorem cs_aux {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] {x y : E} (hy : y ≠ 0) :

‖x - (has_inner.inner y x * (↑‖y‖ ^ 2)⁻¹) • y‖ ^ 2 = ‖x‖ ^ 2 - ‖has_inner.inner x y‖ ^ 2 * (‖y‖ ^ 2)⁻¹

source

noncomputable def of_norm.inner_def {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x y : X) :

𝕜

Equations

of_norm.inner_def x y = 4⁻¹ * (↑‖x + y‖ ^ 2 - ↑‖x - y‖ ^ 2 + is_R_or_C.I * ↑‖is_R_or_C.I • x + y‖ ^ 2 - is_R_or_C.I * ↑‖is_R_or_C.I • x - y‖ ^ 2)

source

theorem of_norm.re_inner_def {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x y : X) :

⇑is_R_or_C.re (of_norm.inner_def x y) = 4⁻¹ * (‖x + y‖ ^ 2 - ‖x - y‖ ^ 2)

source

theorem of_norm.im_eq_re_neg_I {𝕜 : Type u_1} [is_R_or_C 𝕜] (x : 𝕜) :

⇑is_R_or_C.im x = ⇑is_R_or_C.re (-is_R_or_C.I * x)

source

theorem of_norm.inner_def_zero_left {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x : X) :

of_norm.inner_def 0 x = 0

source

theorem of_norm.inner_def_I_smul_left {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x y : X) :

of_norm.inner_def (is_R_or_C.I • x) y = -is_R_or_C.I * of_norm.inner_def x y

source

theorem of_norm.im_inner_def_aux {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x y : X) :

⇑is_R_or_C.im (of_norm.inner_def x y) = ⇑is_R_or_C.re (of_norm.inner_def (is_R_or_C.I • x) y)

source

theorem of_norm.re_inner_def_symm {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x y : X) :

⇑is_R_or_C.re (of_norm.inner_def x y) = ⇑is_R_or_C.re (of_norm.inner_def y x)

source

theorem of_norm.im_inner_def_symm {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x y : X) :

⇑is_R_or_C.im (of_norm.inner_def x y) = -⇑is_R_or_C.im (of_norm.inner_def y x)

source

theorem of_norm.inner_def_conj {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x y : X) :

⇑(star_ring_end 𝕜) (of_norm.inner_def x y) = of_norm.inner_def y x

source

theorem of_norm.inner_def_add_left {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (h : ∀ (x y : X), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) (x y z : X) :

of_norm.inner_def (x + y) z = of_norm.inner_def x z + of_norm.inner_def y z

source

theorem of_norm.inner_def_nsmul_left {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (h : ∀ (x y : X), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) (n : ℕ) (x y : X) :

of_norm.inner_def (↑n • x) y = ↑n * of_norm.inner_def x y

source

theorem of_norm.inner_def_neg_one_smul_left {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (x y : X) :

of_norm.inner_def (↑-1 • x) y = -of_norm.inner_def x y

source

theorem continuous.inner_def {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] {f g : ℝ → X} (hf : continuous f) (hg : continuous g) :

continuous (λ (x : ℝ), of_norm.inner_def (f x) (g x))

source

theorem of_norm.inner_def_smul_left {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (h : ∀ (x y : X), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) (r : 𝕜) (x y : X) :

of_norm.inner_def (r • x) y = ⇑(star_ring_end 𝕜) r * of_norm.inner_def x y

source

noncomputable def of_norm.inner_product_spacce.of_norm {𝕜 : Type u_1} {X : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group X] [normed_space 𝕜 X] (h : ∀ (x y : X), ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) :

inner_product_space 𝕜 X

Equations

of_norm.inner_product_spacce.of_norm h = {to_normed_space := _inst_3, to_has_inner := {inner := λ (x y : X), of_norm.inner_def x y}, norm_sq_eq_inner := _, conj_symm := _, add_left := _, smul_left := _}

source

def is_continuous_linear_map (𝕜 : Type u_1) [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] (f : E → F) :

Prop

Equations

is_continuous_linear_map 𝕜 f = (is_linear_map 𝕜 f ∧ continuous f)

source

def is_continuous_linear_map.mk' {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} (h : is_continuous_linear_map 𝕜 f) :

E →L[𝕜] F

Equations

h.mk' = {to_linear_map := is_linear_map.mk' f _, cont := _}

source

theorem is_continuous_linear_map.coe_mk' {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} (h : is_continuous_linear_map 𝕜 f) :

f = ⇑(h.mk')

source

theorem is_bounded_linear_map_iff_is_continuous_linear_map {𝕜 : Type u_1} {E : Type u_2} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] (f : E → F) :

is_bounded_linear_map 𝕜 f ↔ is_continuous_linear_map 𝕜 f

source

def with_bound {E : Type u_1} [normed_add_comm_group E] {F : Type u_2} [normed_add_comm_group F] (f : E → F) :

Prop

Equations

with_bound f = ∃ (M : ℝ), 0 < M ∧ ∀ (x : E), ‖f x‖ ≤ M * ‖x‖

source

theorem is_bounded_linear_map.def {𝕜 : Type u_1} {E : Type u_2} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E → F} :

is_bounded_linear_map 𝕜 f ↔ is_linear_map 𝕜 f ∧ with_bound f

source

theorem linear_map.with_bound_iff_is_continuous {𝕜 : Type u_1} {E : Type u_2} [nontrivially_normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {f : E →ₗ[𝕜] F} :

with_bound ⇑f ↔ continuous ⇑f

source

theorem linear_map.ker_coe_def {R : Type u_1} {E : Type u_2} {F : Type u_3} [semiring R] [add_comm_monoid E] [add_comm_monoid F] [module R E] [module R F] {f : E →ₗ[R] F} :

↑(linear_map.ker f) = {x : E | ⇑f x = 0}

source

theorem exists_dual_vector_of_ne {𝕜 : Type u_1} [is_R_or_C 𝕜] {X : Type u_2} [normed_add_comm_group X] [normed_space 𝕜 X] {x y : X} (h : x ≠ y) :

∃ (f : normed_space.dual 𝕜 X), ⇑f x ≠ ⇑f y

source

theorem is_linear_map_zero (R : Type u_1) {E : Type u_2} {F : Type u_3} [comm_semiring R] [add_comm_monoid E] [module R E] [add_comm_monoid F] [module R F] :

is_linear_map R 0

source

theorem is_continuous_linear_map_zero {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] :

is_continuous_linear_map 𝕜 0

source

theorem is_continuous_linear_map.of_inner_symmetric_fun {𝕜 : Type u_1} [is_R_or_C 𝕜] {X : Type u_2} [normed_add_comm_group X] [inner_product_space 𝕜 X] [complete_space X] {f : X → X} (h : ∀ (a b : X), has_inner.inner (f a) b = has_inner.inner a (f b)) :

is_continuous_linear_map 𝕜 f

source

structure is_bilinear_map (𝕜 : Type u_3) [normed_field 𝕜] {E : Type u_4} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_5} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_6} [normed_add_comm_group G] [normed_space 𝕜 G] (f : E × F → G) :

Prop

add_left : ∀ (x₁ x₂ : E) (y : F), f (x₁ + x₂, y) = f (x₁, y) + f (x₂, y)
smul_left : ∀ (c : 𝕜) (x : E) (y : F), f (c • x, y) = c • f (x, y)
add_right : ∀ (x : E) (y₁ y₂ : F), f (x, y₁ + y₂) = f (x, y₁) + f (x, y₂)
smul_right : ∀ (c : 𝕜) (x : E) (y : F), f (x, c • y) = c • f (x, y)

source

def is_left_linear_map (𝕜 : Type u_1) [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] (f : E × F → G) :

Prop

Equations

is_left_linear_map 𝕜 f = ∀ (b : F), is_linear_map 𝕜 (λ (a : E), f (a, b))

source

theorem is_left_linear_map_iff {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E × F → G} :

is_left_linear_map 𝕜 f ↔ ∀ (b : F), is_linear_map 𝕜 (λ (a : E), f (a, b))

source

def is_right_linear_map (𝕜 : Type u_1) [normed_field 𝕜] {E : Type u_2} {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] (f : E × F → G) :

Prop

Equations

is_right_linear_map 𝕜 f = ∀ (a : E), is_linear_map 𝕜 (λ (b : F), f (a, b))

source

theorem is_right_linear_map_iff {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E × F → G} :

is_right_linear_map 𝕜 f ↔ ∀ (a : E), is_linear_map 𝕜 (λ (b : F), f (a, b))

source

theorem is_bilinear_map_iff_is_linear_map_left_right {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E × F → G} :

is_bilinear_map 𝕜 f ↔ is_left_linear_map 𝕜 f ∧ is_right_linear_map 𝕜 f

source

def is_bilinear_map.to_lm_lm {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E × F → G} (hf : is_bilinear_map 𝕜 f) :

E →ₗ[𝕜] F →ₗ[𝕜] G

Equations

hf.to_lm_lm = {to_fun := λ (x : E), {to_fun := λ (y : F), f (x, y), map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}

source

def is_lm_left_is_clm_right.to_lm_clm {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E × F → G} (hf₁ : ∀ (y : F), is_linear_map 𝕜 (λ (a : E), f (a, y))) (hf₂ : ∀ (x : E), is_continuous_linear_map 𝕜 (λ (a : F), f (x, a))) :

E →ₗ[𝕜] F →L[𝕜] G

Equations

is_lm_left_is_clm_right.to_lm_clm hf₁ hf₂ = {to_fun := λ (x : E), _.mk', map_add' := _, map_smul' := _}

source

theorem is_bilinear_map.zero_left {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E × F → G} (h : is_bilinear_map 𝕜 f) (y : F) :

f (0, y) = 0

source

theorem is_bilinear_map.zero_right {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E × F → G} (h : is_bilinear_map 𝕜 f) (x : E) :

f (x, 0) = 0

source

theorem is_bilinear_map.eq_zero_add_self {𝕜 : Type u_1} [normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {f : E × F → G} (h : is_bilinear_map 𝕜 f) (xy : E × F) :

f xy = f (xy.fst, 0) + f xy

source

theorem is_continuous_linear_map.to_is_lm {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [normed_field 𝕜] [normed_add_comm_group X] [normed_add_comm_group Y] [normed_space 𝕜 X] [normed_space 𝕜 Y] {β : X → Y} (hf : is_continuous_linear_map 𝕜 β) :

is_linear_map 𝕜 β

source

theorem continuous_linear_map.op_norm_le_iff {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [nontrivially_normed_field 𝕜] [normed_add_comm_group X] [normed_add_comm_group Y] [normed_space 𝕜 X] [normed_space 𝕜 Y] (f : X →L[𝕜] Y) {r : ℝ} (hr : 0 ≤ r) :

‖f‖ ≤ r ↔ ∀ (x : X), ‖⇑f x‖ ≤ r * ‖x‖