mathlib3 documentation

data.is_R_or_C.basic

`is_R_or_C`: a typeclass for ℝ or ℂ #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the typeclass is_R_or_C intended to have only two instances: ℝ and ℂ. It is meant for definitions and theorems which hold for both the real and the complex case, and in particular when the real case follows directly from the complex case by setting re to id, im to zero and so on. Its API follows closely that of ℂ.

Applications include defining inner products and Hilbert spaces for both the real and complex case. One typically produces the definitions and proof for an arbitrary field of this typeclass, which basically amounts to doing the complex case, and the two cases then fall out immediately from the two instances of the class.

The instance for ℝ is registered in this file. The instance for ℂ is declared in analysis.complex.basic.

Implementation notes #

The coercion from reals into an is_R_or_C field is done by registering algebra_map ℝ K as a has_coe_t. For this to work, we must proceed carefully to avoid problems involving circular coercions in the case K=ℝ; in particular, we cannot use the plain has_coe and must set priorities carefully. This problem was already solved for ℕ, and we copy the solution detailed in data/nat/cast. See also Note [coercion into rings] for more details.

In addition, several lemmas need to be set at priority 900 to make sure that they do not override their counterparts in complex.lean (which causes linter errors).

A few lemmas requiring heavier imports are in data.is_R_or_C.lemmas.

@[class]

structure is_R_or_C (K : Type u_1) :

Type u_1

to_densely_normed_field : densely_normed_field K
to_star_ring : star_ring K
to_normed_algebra : normed_algebra ℝ K
to_complete_space : complete_space K
re : K →+ ℝ
im : K →+ ℝ
I : K
I_re_ax : ⇑is_R_or_C.re is_R_or_C.I = 0
I_mul_I_ax : is_R_or_C.I = 0 ∨ is_R_or_C.I * is_R_or_C.I = -1
re_add_im_ax : ∀ (z : K), ⇑(algebra_map ℝ K) (⇑is_R_or_C.re z) + ⇑(algebra_map ℝ K) (⇑is_R_or_C.im z) * is_R_or_C.I = z
of_real_re_ax : ∀ (r : ℝ), ⇑is_R_or_C.re (⇑(algebra_map ℝ K) r) = r
of_real_im_ax : ∀ (r : ℝ), ⇑is_R_or_C.im (⇑(algebra_map ℝ K) r) = 0
mul_re_ax : ∀ (z w : K), ⇑is_R_or_C.re (z * w) = ⇑is_R_or_C.re z * ⇑is_R_or_C.re w - ⇑is_R_or_C.im z * ⇑is_R_or_C.im w
mul_im_ax : ∀ (z w : K), ⇑is_R_or_C.im (z * w) = ⇑is_R_or_C.re z * ⇑is_R_or_C.im w + ⇑is_R_or_C.im z * ⇑is_R_or_C.re w
conj_re_ax : ∀ (z : K), ⇑is_R_or_C.re (⇑(star_ring_end K) z) = ⇑is_R_or_C.re z
conj_im_ax : ∀ (z : K), ⇑is_R_or_C.im (⇑(star_ring_end K) z) = -⇑is_R_or_C.im z
conj_I_ax : ⇑(star_ring_end K) is_R_or_C.I = -is_R_or_C.I
norm_sq_eq_def_ax : ∀ (z : K), ‖z‖ ^ 2 = ⇑is_R_or_C.re z * ⇑is_R_or_C.re z + ⇑is_R_or_C.im z * ⇑is_R_or_C.im z
mul_im_I_ax : ∀ (z : K), ⇑is_R_or_C.im z * ⇑is_R_or_C.im is_R_or_C.I = ⇑is_R_or_C.im z

This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.

Instances of this typeclass

Instances of other typeclasses for is_R_or_C

is_R_or_C.has_sizeof_inst

@[protected, instance]

noncomputable def is_R_or_C.algebra_map_coe {K : Type u_1} [is_R_or_C K] :

has_coe_t ℝ K

Equations

is_R_or_C.algebra_map_coe = {coe := ⇑(algebra_map ℝ K)}

theorem is_R_or_C.of_real_alg {K : Type u_1} [is_R_or_C K] (x : ℝ) :

↑x = x • 1

theorem is_R_or_C.real_smul_eq_coe_mul {K : Type u_1} [is_R_or_C K] (r : ℝ) (z : K) :

r • z = ↑r * z

theorem is_R_or_C.real_smul_eq_coe_smul {K : Type u_1} {E : Type u_2} [is_R_or_C K] [add_comm_group E] [module K E] [module ℝ E] [is_scalar_tower ℝ K E] (r : ℝ) (x : E) :

r • x = ↑r • x

theorem is_R_or_C.algebra_map_eq_of_real {K : Type u_1} [is_R_or_C K] :

⇑(algebra_map ℝ K) = coe

@[simp]

theorem is_R_or_C.re_add_im {K : Type u_1} [is_R_or_C K] (z : K) :

↑(⇑is_R_or_C.re z) + ↑(⇑is_R_or_C.im z) * is_R_or_C.I = z

@[simp, norm_cast]

theorem is_R_or_C.of_real_re {K : Type u_1} [is_R_or_C K] (r : ℝ) :

⇑is_R_or_C.re ↑r = r

@[simp, norm_cast]

theorem is_R_or_C.of_real_im {K : Type u_1} [is_R_or_C K] (r : ℝ) :

⇑is_R_or_C.im ↑r = 0

@[simp]

theorem is_R_or_C.mul_re {K : Type u_1} [is_R_or_C K] (z w : K) :

⇑is_R_or_C.re (z * w) = ⇑is_R_or_C.re z * ⇑is_R_or_C.re w - ⇑is_R_or_C.im z * ⇑is_R_or_C.im w

@[simp]

theorem is_R_or_C.mul_im {K : Type u_1} [is_R_or_C K] (z w : K) :

⇑is_R_or_C.im (z * w) = ⇑is_R_or_C.re z * ⇑is_R_or_C.im w + ⇑is_R_or_C.im z * ⇑is_R_or_C.re w

theorem is_R_or_C.ext_iff {K : Type u_1} [is_R_or_C K] {z w : K} :

z = w ↔ ⇑is_R_or_C.re z = ⇑is_R_or_C.re w ∧ ⇑is_R_or_C.im z = ⇑is_R_or_C.im w

theorem is_R_or_C.ext {K : Type u_1} [is_R_or_C K] {z w : K} (hre : ⇑is_R_or_C.re z = ⇑is_R_or_C.re w) (him : ⇑is_R_or_C.im z = ⇑is_R_or_C.im w) :

z = w

@[norm_cast]

theorem is_R_or_C.of_real_zero {K : Type u_1} [is_R_or_C K] :

↑0 = 0

theorem is_R_or_C.zero_re' {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.re 0 = 0

@[norm_cast]

theorem is_R_or_C.of_real_one {K : Type u_1} [is_R_or_C K] :

↑1 = 1

@[simp]

theorem is_R_or_C.one_re {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.re 1 = 1

@[simp]

theorem is_R_or_C.one_im {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.im 1 = 0

theorem is_R_or_C.of_real_injective {K : Type u_1} [is_R_or_C K] :

function.injective coe

@[norm_cast]

theorem is_R_or_C.of_real_inj {K : Type u_1} [is_R_or_C K] {z w : ℝ} :

↑z = ↑w ↔ z = w

@[simp]

theorem is_R_or_C.bit0_re {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.re (bit0 z) = bit0 (⇑is_R_or_C.re z)

@[simp]

theorem is_R_or_C.bit1_re {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.re (bit1 z) = bit1 (⇑is_R_or_C.re z)

@[simp]

theorem is_R_or_C.bit0_im {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.im (bit0 z) = bit0 (⇑is_R_or_C.im z)

@[simp]

theorem is_R_or_C.bit1_im {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.im (bit1 z) = bit0 (⇑is_R_or_C.im z)

theorem is_R_or_C.of_real_eq_zero {K : Type u_1} [is_R_or_C K] {x : ℝ} :

↑x = 0 ↔ x = 0

theorem is_R_or_C.of_real_ne_zero {K : Type u_1} [is_R_or_C K] {x : ℝ} :

↑x ≠ 0 ↔ x ≠ 0

@[simp, norm_cast]

theorem is_R_or_C.of_real_add {K : Type u_1} [is_R_or_C K] (r s : ℝ) :

↑(r + s) = ↑r + ↑s

@[simp, norm_cast]

theorem is_R_or_C.of_real_bit0 {K : Type u_1} [is_R_or_C K] (r : ℝ) :

↑(bit0 r) = bit0 ↑r

@[simp, norm_cast]

theorem is_R_or_C.of_real_bit1 {K : Type u_1} [is_R_or_C K] (r : ℝ) :

↑(bit1 r) = bit1 ↑r

@[simp, norm_cast]

theorem is_R_or_C.of_real_neg {K : Type u_1} [is_R_or_C K] (r : ℝ) :

@[simp, norm_cast]

theorem is_R_or_C.of_real_sub {K : Type u_1} [is_R_or_C K] (r s : ℝ) :

↑(r - s) = ↑r - ↑s

@[simp, norm_cast]

theorem is_R_or_C.of_real_sum {K : Type u_1} [is_R_or_C K] {α : Type u_2} (s : finset α) (f : α → ℝ) :

↑(s.sum (λ (i : α), f i)) = s.sum (λ (i : α), ↑(f i))

@[simp, norm_cast]

theorem is_R_or_C.of_real_finsupp_sum {K : Type u_1} [is_R_or_C K] {α : Type u_2} {M : Type u_3} [has_zero M] (f : α →₀ M) (g : α → M → ℝ) :

↑(f.sum (λ (a : α) (b : M), g a b)) = f.sum (λ (a : α) (b : M), ↑(g a b))

@[simp, norm_cast]

theorem is_R_or_C.of_real_mul {K : Type u_1} [is_R_or_C K] (r s : ℝ) :

↑(r * s) = ↑r * ↑s

@[simp, norm_cast]

theorem is_R_or_C.of_real_pow {K : Type u_1} [is_R_or_C K] (r : ℝ) (n : ℕ) :

↑(r ^ n) = ↑r ^ n

@[simp, norm_cast]

theorem is_R_or_C.of_real_prod {K : Type u_1} [is_R_or_C K] {α : Type u_2} (s : finset α) (f : α → ℝ) :

↑(s.prod (λ (i : α), f i)) = s.prod (λ (i : α), ↑(f i))

@[simp, norm_cast]

theorem is_R_or_C.of_real_finsupp_prod {K : Type u_1} [is_R_or_C K] {α : Type u_2} {M : Type u_3} [has_zero M] (f : α →₀ M) (g : α → M → ℝ) :

↑(f.prod (λ (a : α) (b : M), g a b)) = f.prod (λ (a : α) (b : M), ↑(g a b))

@[simp, norm_cast]

theorem is_R_or_C.real_smul_of_real {K : Type u_1} [is_R_or_C K] (r x : ℝ) :

r • ↑x = ↑r * ↑x

theorem is_R_or_C.of_real_mul_re {K : Type u_1} [is_R_or_C K] (r : ℝ) (z : K) :

⇑is_R_or_C.re (↑r * z) = r * ⇑is_R_or_C.re z

theorem is_R_or_C.of_real_mul_im {K : Type u_1} [is_R_or_C K] (r : ℝ) (z : K) :

⇑is_R_or_C.im (↑r * z) = r * ⇑is_R_or_C.im z

theorem is_R_or_C.smul_re {K : Type u_1} [is_R_or_C K] (r : ℝ) (z : K) :

⇑is_R_or_C.re (r • z) = r * ⇑is_R_or_C.re z

theorem is_R_or_C.smul_im {K : Type u_1} [is_R_or_C K] (r : ℝ) (z : K) :

⇑is_R_or_C.im (r • z) = r * ⇑is_R_or_C.im z

@[simp, norm_cast]

theorem is_R_or_C.norm_of_real {K : Type u_1} [is_R_or_C K] (r : ℝ) :

‖↑r‖ = |r|

Characteristic zero #

@[protected, instance]

def is_R_or_C.char_zero_R_or_C {K : Type u_1} [is_R_or_C K] :

ℝ and ℂ are both of characteristic zero.

The imaginary unit, `I` #

@[simp]

theorem is_R_or_C.I_re {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.re is_R_or_C.I = 0

The imaginary unit.

@[simp]

theorem is_R_or_C.I_im {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.im z * ⇑is_R_or_C.im is_R_or_C.I = ⇑is_R_or_C.im z

@[simp]

theorem is_R_or_C.I_im' {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.im is_R_or_C.I * ⇑is_R_or_C.im z = ⇑is_R_or_C.im z

@[simp]

theorem is_R_or_C.I_mul_re {K : Type u_1} [is_R_or_C K] (z : K) :

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

theorem is_R_or_C.I_mul_I {K : Type u_1} [is_R_or_C K] :

is_R_or_C.I = 0 ∨ is_R_or_C.I * is_R_or_C.I = -1

@[simp]

theorem is_R_or_C.conj_re {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.re (⇑(star_ring_end K) z) = ⇑is_R_or_C.re z

@[simp]

theorem is_R_or_C.conj_im {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.im (⇑(star_ring_end K) z) = -⇑is_R_or_C.im z

@[simp]

theorem is_R_or_C.conj_I {K : Type u_1} [is_R_or_C K] :

⇑(star_ring_end K) is_R_or_C.I = -is_R_or_C.I

@[simp]

theorem is_R_or_C.conj_of_real {K : Type u_1} [is_R_or_C K] (r : ℝ) :

⇑(star_ring_end K) ↑r = ↑r

@[simp]

theorem is_R_or_C.conj_bit0 {K : Type u_1} [is_R_or_C K] (z : K) :

⇑(star_ring_end K) (bit0 z) = bit0 (⇑(star_ring_end K) z)

@[simp]

theorem is_R_or_C.conj_bit1 {K : Type u_1} [is_R_or_C K] (z : K) :

⇑(star_ring_end K) (bit1 z) = bit1 (⇑(star_ring_end K) z)

@[simp]

theorem is_R_or_C.conj_neg_I {K : Type u_1} [is_R_or_C K] :

⇑(star_ring_end K) (-is_R_or_C.I) = is_R_or_C.I

theorem is_R_or_C.conj_eq_re_sub_im {K : Type u_1} [is_R_or_C K] (z : K) :

⇑(star_ring_end K) z = ↑(⇑is_R_or_C.re z) - ↑(⇑is_R_or_C.im z) * is_R_or_C.I

theorem is_R_or_C.sub_conj {K : Type u_1} [is_R_or_C K] (z : K) :

z - ⇑(star_ring_end K) z = 2 * ↑(⇑is_R_or_C.im z) * is_R_or_C.I

theorem is_R_or_C.conj_smul {K : Type u_1} [is_R_or_C K] (r : ℝ) (z : K) :

⇑(star_ring_end K) (r • z) = r • ⇑(star_ring_end K) z

theorem is_R_or_C.add_conj {K : Type u_1} [is_R_or_C K] (z : K) :

z + ⇑(star_ring_end K) z = 2 * ↑(⇑is_R_or_C.re z)

theorem is_R_or_C.re_eq_add_conj {K : Type u_1} [is_R_or_C K] (z : K) :

↑(⇑is_R_or_C.re z) = (z + ⇑(star_ring_end K) z) / 2

theorem is_R_or_C.im_eq_conj_sub {K : Type u_1} [is_R_or_C K] (z : K) :

↑(⇑is_R_or_C.im z) = is_R_or_C.I * (⇑(star_ring_end K) z - z) / 2

theorem is_R_or_C.is_real_tfae {K : Type u_1} [is_R_or_C K] (z : K) :

[⇑(star_ring_end K) z = z, ∃ (r : ℝ), ↑r = z, ↑(⇑is_R_or_C.re z) = z, ⇑is_R_or_C.im z = 0].tfae

There are several equivalent ways to say that a number z is in fact a real number.

theorem is_R_or_C.conj_eq_iff_real {K : Type u_1} [is_R_or_C K] {z : K} :

⇑(star_ring_end K) z = z ↔ ∃ (r : ℝ), z = ↑r

theorem is_R_or_C.conj_eq_iff_re {K : Type u_1} [is_R_or_C K] {z : K} :

⇑(star_ring_end K) z = z ↔ ↑(⇑is_R_or_C.re z) = z

theorem is_R_or_C.conj_eq_iff_im {K : Type u_1} [is_R_or_C K] {z : K} :

⇑(star_ring_end K) z = z ↔ ⇑is_R_or_C.im z = 0

@[simp]

theorem is_R_or_C.star_def {K : Type u_1} [is_R_or_C K] :

has_star.star = ⇑(star_ring_end K)

@[reducible]

def is_R_or_C.conj_to_ring_equiv (K : Type u_1) [is_R_or_C K] :

K ≃+* Kᵐᵒᵖ

Conjugation as a ring equivalence. This is used to convert the inner product into a sesquilinear product.

def is_R_or_C.norm_sq {K : Type u_1} [is_R_or_C K] :

The norm squared function.

Equations

is_R_or_C.norm_sq = {to_fun := λ (z : K), ⇑is_R_or_C.re z * ⇑is_R_or_C.re z + ⇑is_R_or_C.im z * ⇑is_R_or_C.im z, map_zero' := _, map_one' := _, map_mul' := _}

theorem is_R_or_C.norm_sq_apply {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.norm_sq z = ⇑is_R_or_C.re z * ⇑is_R_or_C.re z + ⇑is_R_or_C.im z * ⇑is_R_or_C.im z

theorem is_R_or_C.norm_sq_eq_def {K : Type u_1} [is_R_or_C K] {z : K} :

‖z‖ ^ 2 = ⇑is_R_or_C.re z * ⇑is_R_or_C.re z + ⇑is_R_or_C.im z * ⇑is_R_or_C.im z

theorem is_R_or_C.norm_sq_eq_def' {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.norm_sq z = ‖z‖ ^ 2

theorem is_R_or_C.norm_sq_zero {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.norm_sq 0 = 0

theorem is_R_or_C.norm_sq_one {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.norm_sq 1 = 1

theorem is_R_or_C.norm_sq_nonneg {K : Type u_1} [is_R_or_C K] (z : K) :

0 ≤ ⇑is_R_or_C.norm_sq z

@[simp]

theorem is_R_or_C.norm_sq_eq_zero {K : Type u_1} [is_R_or_C K] {z : K} :

⇑is_R_or_C.norm_sq z = 0 ↔ z = 0

@[simp]

theorem is_R_or_C.norm_sq_pos {K : Type u_1} [is_R_or_C K] {z : K} :

0 < ⇑is_R_or_C.norm_sq z ↔ z ≠ 0

@[simp]

theorem is_R_or_C.norm_sq_neg {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.norm_sq (-z) = ⇑is_R_or_C.norm_sq z

@[simp]

theorem is_R_or_C.norm_sq_conj {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.norm_sq (⇑(star_ring_end K) z) = ⇑is_R_or_C.norm_sq z

@[simp]

theorem is_R_or_C.norm_sq_mul {K : Type u_1} [is_R_or_C K] (z w : K) :

⇑is_R_or_C.norm_sq (z * w) = ⇑is_R_or_C.norm_sq z * ⇑is_R_or_C.norm_sq w

theorem is_R_or_C.norm_sq_add {K : Type u_1} [is_R_or_C K] (z w : K) :

⇑is_R_or_C.norm_sq (z + w) = ⇑is_R_or_C.norm_sq z + ⇑is_R_or_C.norm_sq w + 2 * ⇑is_R_or_C.re (z * ⇑(star_ring_end K) w)

theorem is_R_or_C.re_sq_le_norm_sq {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.re z * ⇑is_R_or_C.re z ≤ ⇑is_R_or_C.norm_sq z

theorem is_R_or_C.im_sq_le_norm_sq {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.im z * ⇑is_R_or_C.im z ≤ ⇑is_R_or_C.norm_sq z

theorem is_R_or_C.mul_conj {K : Type u_1} [is_R_or_C K] (z : K) :

z * ⇑(star_ring_end K) z = ↑(⇑is_R_or_C.norm_sq z)

theorem is_R_or_C.conj_mul {K : Type u_1} [is_R_or_C K] (x : K) :

⇑(star_ring_end K) x * x = ↑(⇑is_R_or_C.norm_sq x)

theorem is_R_or_C.norm_sq_sub {K : Type u_1} [is_R_or_C K] (z w : K) :

⇑is_R_or_C.norm_sq (z - w) = ⇑is_R_or_C.norm_sq z + ⇑is_R_or_C.norm_sq w - 2 * ⇑is_R_or_C.re (z * ⇑(star_ring_end K) w)

theorem is_R_or_C.sqrt_norm_sq_eq_norm {K : Type u_1} [is_R_or_C K] {z : K} :

√ (⇑is_R_or_C.norm_sq z) = ‖z‖

Inversion #

@[simp, norm_cast]

theorem is_R_or_C.of_real_inv {K : Type u_1} [is_R_or_C K] (r : ℝ) :

↑r⁻¹ = (↑r)⁻¹

theorem is_R_or_C.inv_def {K : Type u_1} [is_R_or_C K] (z : K) :

z⁻¹ = ⇑(star_ring_end K) z * ↑(‖z‖ ^ 2)⁻¹

@[simp]

theorem is_R_or_C.inv_re {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.re z⁻¹ = ⇑is_R_or_C.re z / ⇑is_R_or_C.norm_sq z

@[simp]

theorem is_R_or_C.inv_im {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.im z⁻¹ = -⇑is_R_or_C.im z / ⇑is_R_or_C.norm_sq z

theorem is_R_or_C.div_re {K : Type u_1} [is_R_or_C K] (z w : K) :

⇑is_R_or_C.re (z / w) = ⇑is_R_or_C.re z * ⇑is_R_or_C.re w / ⇑is_R_or_C.norm_sq w + ⇑is_R_or_C.im z * ⇑is_R_or_C.im w / ⇑is_R_or_C.norm_sq w

theorem is_R_or_C.div_im {K : Type u_1} [is_R_or_C K] (z w : K) :

⇑is_R_or_C.im (z / w) = ⇑is_R_or_C.im z * ⇑is_R_or_C.re w / ⇑is_R_or_C.norm_sq w - ⇑is_R_or_C.re z * ⇑is_R_or_C.im w / ⇑is_R_or_C.norm_sq w

@[simp]

theorem is_R_or_C.conj_inv {K : Type u_1} [is_R_or_C K] (x : K) :

⇑(star_ring_end K) x⁻¹ = (⇑(star_ring_end K) x)⁻¹

@[simp, norm_cast]

theorem is_R_or_C.of_real_div {K : Type u_1} [is_R_or_C K] (r s : ℝ) :

↑(r / s) = ↑r / ↑s

theorem is_R_or_C.div_re_of_real {K : Type u_1} [is_R_or_C K] {z : K} {r : ℝ} :

⇑is_R_or_C.re (z / ↑r) = ⇑is_R_or_C.re z / r

@[simp, norm_cast]

theorem is_R_or_C.of_real_zpow {K : Type u_1} [is_R_or_C K] (r : ℝ) (n : ℤ) :

↑(r ^ n) = ↑r ^ n

theorem is_R_or_C.I_mul_I_of_nonzero {K : Type u_1} [is_R_or_C K] :

is_R_or_C.I ≠ 0 → is_R_or_C.I * is_R_or_C.I = -1

@[simp]

theorem is_R_or_C.inv_I {K : Type u_1} [is_R_or_C K] :

is_R_or_C.I ⁻¹ = -is_R_or_C.I

@[simp]

theorem is_R_or_C.div_I {K : Type u_1} [is_R_or_C K] (z : K) :

z / is_R_or_C.I = -(z * is_R_or_C.I)

@[simp]

theorem is_R_or_C.norm_sq_inv {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.norm_sq z⁻¹ = (⇑is_R_or_C.norm_sq z)⁻¹

@[simp]

theorem is_R_or_C.norm_sq_div {K : Type u_1} [is_R_or_C K] (z w : K) :

⇑is_R_or_C.norm_sq (z / w) = ⇑is_R_or_C.norm_sq z / ⇑is_R_or_C.norm_sq w

@[simp]

theorem is_R_or_C.norm_conj {K : Type u_1} [is_R_or_C K] {z : K} :

‖⇑(star_ring_end K) z‖ = ‖z‖

@[protected, instance]

def is_R_or_C.cstar_ring {K : Type u_1} [is_R_or_C K] :

Cast lemmas #

@[simp, norm_cast]

theorem is_R_or_C.of_real_nat_cast {K : Type u_1} [is_R_or_C K] (n : ℕ) :

@[simp, norm_cast]

theorem is_R_or_C.nat_cast_re {K : Type u_1} [is_R_or_C K] (n : ℕ) :

⇑is_R_or_C.re ↑n = ↑n

@[simp, norm_cast]

theorem is_R_or_C.nat_cast_im {K : Type u_1} [is_R_or_C K] (n : ℕ) :

⇑is_R_or_C.im ↑n = 0

@[simp, norm_cast]

theorem is_R_or_C.of_real_int_cast {K : Type u_1} [is_R_or_C K] (n : ℤ) :

@[simp, norm_cast]

theorem is_R_or_C.int_cast_re {K : Type u_1} [is_R_or_C K] (n : ℤ) :

⇑is_R_or_C.re ↑n = ↑n

@[simp, norm_cast]

theorem is_R_or_C.int_cast_im {K : Type u_1} [is_R_or_C K] (n : ℤ) :

⇑is_R_or_C.im ↑n = 0

@[simp, norm_cast]

theorem is_R_or_C.of_real_rat_cast {K : Type u_1} [is_R_or_C K] (n : ℚ) :

@[simp, norm_cast]

theorem is_R_or_C.rat_cast_re {K : Type u_1} [is_R_or_C K] (q : ℚ) :

⇑is_R_or_C.re ↑q = ↑q

@[simp, norm_cast]

theorem is_R_or_C.rat_cast_im {K : Type u_1} [is_R_or_C K] (q : ℚ) :

⇑is_R_or_C.im ↑q = 0

Norm #

theorem is_R_or_C.norm_of_nonneg {K : Type u_1} [is_R_or_C K] {r : ℝ} (h : 0 ≤ r) :

@[simp, norm_cast]

theorem is_R_or_C.norm_nat_cast {K : Type u_1} [is_R_or_C K] (n : ℕ) :

‖↑n‖ = ↑n

theorem is_R_or_C.mul_self_norm {K : Type u_1} [is_R_or_C K] (z : K) :

‖z‖ * ‖z‖ = ⇑is_R_or_C.norm_sq z

@[simp]

theorem is_R_or_C.norm_two {K : Type u_1} [is_R_or_C K] :

theorem is_R_or_C.abs_re_le_norm {K : Type u_1} [is_R_or_C K] (z : K) :

|⇑is_R_or_C.re z| ≤ ‖z‖

theorem is_R_or_C.abs_im_le_norm {K : Type u_1} [is_R_or_C K] (z : K) :

|⇑is_R_or_C.im z| ≤ ‖z‖

theorem is_R_or_C.norm_re_le_norm {K : Type u_1} [is_R_or_C K] (z : K) :

‖⇑is_R_or_C.re z‖ ≤ ‖z‖

theorem is_R_or_C.norm_im_le_norm {K : Type u_1} [is_R_or_C K] (z : K) :

‖⇑is_R_or_C.im z‖ ≤ ‖z‖

theorem is_R_or_C.re_le_norm {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.re z ≤ ‖z‖

theorem is_R_or_C.im_le_norm {K : Type u_1} [is_R_or_C K] (z : K) :

⇑is_R_or_C.im z ≤ ‖z‖

theorem is_R_or_C.im_eq_zero_of_le {K : Type u_1} [is_R_or_C K] {a : K} (h : ‖a‖ ≤ ⇑is_R_or_C.re a) :

⇑is_R_or_C.im a = 0

theorem is_R_or_C.re_eq_self_of_le {K : Type u_1} [is_R_or_C K] {a : K} (h : ‖a‖ ≤ ⇑is_R_or_C.re a) :

↑(⇑is_R_or_C.re a) = a

theorem is_R_or_C.abs_re_div_norm_le_one {K : Type u_1} [is_R_or_C K] (z : K) :

|⇑is_R_or_C.re z / ‖z‖| ≤ 1

theorem is_R_or_C.abs_im_div_norm_le_one {K : Type u_1} [is_R_or_C K] (z : K) :

|⇑is_R_or_C.im z / ‖z‖| ≤ 1

theorem is_R_or_C.norm_I_of_ne_zero {K : Type u_1} [is_R_or_C K] (hI : is_R_or_C.I ≠ 0) :

‖is_R_or_C.I ‖ = 1

theorem is_R_or_C.re_eq_norm_of_mul_conj {K : Type u_1} [is_R_or_C K] (x : K) :

⇑is_R_or_C.re (x * ⇑(star_ring_end K) x) = ‖x * ⇑(star_ring_end K) x‖

theorem is_R_or_C.norm_sq_re_add_conj {K : Type u_1} [is_R_or_C K] (x : K) :

‖x + ⇑(star_ring_end K) x‖ ^ 2 = ⇑is_R_or_C.re (x + ⇑(star_ring_end K) x) ^ 2

theorem is_R_or_C.norm_sq_re_conj_add {K : Type u_1} [is_R_or_C K] (x : K) :

‖⇑(star_ring_end K) x + x‖ ^ 2 = ⇑is_R_or_C.re (⇑(star_ring_end K) x + x) ^ 2

Cauchy sequences #

theorem is_R_or_C.is_cau_seq_re {K : Type u_1} [is_R_or_C K] (f : cau_seq K has_norm.norm) :

is_cau_seq has_abs.abs (λ (n : ℕ), ⇑is_R_or_C.re (⇑f n))

theorem is_R_or_C.is_cau_seq_im {K : Type u_1} [is_R_or_C K] (f : cau_seq K has_norm.norm) :

is_cau_seq has_abs.abs (λ (n : ℕ), ⇑is_R_or_C.im (⇑f n))

noncomputable def is_R_or_C.cau_seq_re {K : Type u_1} [is_R_or_C K] (f : cau_seq K has_norm.norm) :

cau_seq ℝ has_abs.abs

The real part of a K Cauchy sequence, as a real Cauchy sequence.

Equations

is_R_or_C.cau_seq_re f = ⟨λ (n : ℕ), ⇑is_R_or_C.re (⇑f n), _⟩

noncomputable def is_R_or_C.cau_seq_im {K : Type u_1} [is_R_or_C K] (f : cau_seq K has_norm.norm) :

cau_seq ℝ has_abs.abs

The imaginary part of a K Cauchy sequence, as a real Cauchy sequence.

Equations

is_R_or_C.cau_seq_im f = ⟨λ (n : ℕ), ⇑is_R_or_C.im (⇑f n), _⟩

theorem is_R_or_C.is_cau_seq_norm {K : Type u_1} [is_R_or_C K] {f : ℕ → K} (hf : is_cau_seq has_norm.norm f) :

is_cau_seq has_abs.abs (has_norm.norm ∘ f)

@[protected, instance]

noncomputable def real.is_R_or_C :

Equations

real.is_R_or_C = {to_densely_normed_field := {to_normed_field := densely_normed_field.to_normed_field real.densely_normed_field, lt_norm_lt := _}, to_star_ring := real.star_ring, to_normed_algebra := normed_algebra.id ℝ real.normed_field, to_complete_space := real.complete_space, re := add_monoid_hom.id ℝ (add_monoid.to_add_zero_class ℝ), im := 0, I := 0, I_re_ax := real.is_R_or_C._proof_1, I_mul_I_ax := real.is_R_or_C._proof_2, re_add_im_ax := real.is_R_or_C._proof_3, of_real_re_ax := real.is_R_or_C._proof_4, of_real_im_ax := real.is_R_or_C._proof_5, mul_re_ax := real.is_R_or_C._proof_6, mul_im_ax := real.is_R_or_C._proof_7, conj_re_ax := real.is_R_or_C._proof_8, conj_im_ax := real.is_R_or_C._proof_9, conj_I_ax := real.is_R_or_C._proof_10, norm_sq_eq_def_ax := real.is_R_or_C._proof_11, mul_im_I_ax := real.is_R_or_C._proof_12}

@[simp]

theorem is_R_or_C.re_to_real {x : ℝ} :

⇑is_R_or_C.re x = x

@[simp]

theorem is_R_or_C.im_to_real {x : ℝ} :

⇑is_R_or_C.im x = 0

@[simp]

theorem is_R_or_C.conj_to_real {x : ℝ} :

⇑(star_ring_end ℝ) x = x

@[simp]

theorem is_R_or_C.I_to_real :

is_R_or_C.I = 0

@[simp]

theorem is_R_or_C.norm_sq_to_real {x : ℝ} :

⇑is_R_or_C.norm_sq x = x * x

@[simp]

theorem is_R_or_C.coe_real_eq_id :

def is_R_or_C.re_lm {K : Type u_1} [is_R_or_C K] :

K →ₗ[ℝ ] ℝ

The real part in a is_R_or_C field, as a linear map.

Equations

is_R_or_C.re_lm = {to_fun := is_R_or_C.re.to_fun, map_add' := _, map_smul' := _}

@[simp]

theorem is_R_or_C.re_lm_coe {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.re_lm = ⇑is_R_or_C.re

noncomputable def is_R_or_C.re_clm {K : Type u_1} [is_R_or_C K] :

K →L[ℝ ] ℝ

The real part in a is_R_or_C field, as a continuous linear map.

Equations

is_R_or_C.re_clm = is_R_or_C.re_lm.mk_continuous 1 is_R_or_C.re_clm._proof_1

@[simp, norm_cast]

theorem is_R_or_C.re_clm_coe {K : Type u_1} [is_R_or_C K] :

↑is_R_or_C.re_clm = is_R_or_C.re_lm

@[simp]

theorem is_R_or_C.re_clm_apply {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.re_clm = ⇑is_R_or_C.re

@[continuity]

theorem is_R_or_C.continuous_re {K : Type u_1} [is_R_or_C K] :

continuous ⇑is_R_or_C.re

def is_R_or_C.im_lm {K : Type u_1} [is_R_or_C K] :

K →ₗ[ℝ ] ℝ

The imaginary part in a is_R_or_C field, as a linear map.

Equations

is_R_or_C.im_lm = {to_fun := is_R_or_C.im.to_fun, map_add' := _, map_smul' := _}

@[simp]

theorem is_R_or_C.im_lm_coe {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.im_lm = ⇑is_R_or_C.im

noncomputable def is_R_or_C.im_clm {K : Type u_1} [is_R_or_C K] :

K →L[ℝ ] ℝ

The imaginary part in a is_R_or_C field, as a continuous linear map.

Equations

is_R_or_C.im_clm = is_R_or_C.im_lm.mk_continuous 1 is_R_or_C.im_clm._proof_1

@[simp, norm_cast]

theorem is_R_or_C.im_clm_coe {K : Type u_1} [is_R_or_C K] :

↑is_R_or_C.im_clm = is_R_or_C.im_lm

@[simp]

theorem is_R_or_C.im_clm_apply {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.im_clm = ⇑is_R_or_C.im

@[continuity]

theorem is_R_or_C.continuous_im {K : Type u_1} [is_R_or_C K] :

continuous ⇑is_R_or_C.im

def is_R_or_C.conj_ae {K : Type u_1} [is_R_or_C K] :

K ≃ₐ[ℝ ] K

Conjugate as an ℝ-algebra equivalence

Equations

is_R_or_C.conj_ae = {to_fun := (star_ring_end K).to_fun, inv_fun := ⇑(star_ring_end K), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

@[simp]

theorem is_R_or_C.conj_ae_coe {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.conj_ae = ⇑(star_ring_end K)

noncomputable def is_R_or_C.conj_lie {K : Type u_1} [is_R_or_C K] :

K ≃ₗᵢ[ℝ ] K

Conjugate as a linear isometry

Equations

is_R_or_C.conj_lie = {to_linear_equiv := is_R_or_C.conj_ae.to_linear_equiv, norm_map' := _}

@[simp]

theorem is_R_or_C.conj_lie_apply {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.conj_lie = ⇑(star_ring_end K)

noncomputable def is_R_or_C.conj_cle {K : Type u_1} [is_R_or_C K] :

Conjugate as a continuous linear equivalence

Equations

is_R_or_C.conj_cle = ↑is_R_or_C.conj_lie

@[simp]

theorem is_R_or_C.conj_cle_coe {K : Type u_1} [is_R_or_C K] :

is_R_or_C.conj_cle.to_linear_equiv = is_R_or_C.conj_ae.to_linear_equiv

@[simp]

theorem is_R_or_C.conj_cle_apply {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.conj_cle = ⇑(star_ring_end K)

@[protected, instance]

def is_R_or_C.has_continuous_star {K : Type u_1} [is_R_or_C K] :

has_continuous_star K

@[continuity]

theorem is_R_or_C.continuous_conj {K : Type u_1} [is_R_or_C K] :

continuous ⇑(star_ring_end K)

noncomputable def is_R_or_C.of_real_am {K : Type u_1} [is_R_or_C K] :

ℝ →ₐ[ℝ ] K

The ℝ → K coercion, as a linear map

Equations

is_R_or_C.of_real_am = algebra.of_id ℝ K

@[simp]

theorem is_R_or_C.of_real_am_coe {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.of_real_am = coe

noncomputable def is_R_or_C.of_real_li {K : Type u_1} [is_R_or_C K] :

ℝ →ₗᵢ[ℝ ] K

The ℝ → K coercion, as a linear isometry

Equations

is_R_or_C.of_real_li = {to_linear_map := is_R_or_C.of_real_am.to_linear_map, norm_map' := _}

@[simp]

theorem is_R_or_C.of_real_li_apply {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.of_real_li = coe

noncomputable def is_R_or_C.of_real_clm {K : Type u_1} [is_R_or_C K] :

ℝ →L[ℝ ] K

The ℝ → K coercion, as a continuous linear map

Equations

is_R_or_C.of_real_clm = is_R_or_C.of_real_li.to_continuous_linear_map

@[simp]

theorem is_R_or_C.of_real_clm_coe {K : Type u_1} [is_R_or_C K] :

↑is_R_or_C.of_real_clm = is_R_or_C.of_real_am.to_linear_map

@[simp]

theorem is_R_or_C.of_real_clm_apply {K : Type u_1} [is_R_or_C K] :

⇑is_R_or_C.of_real_clm = coe

@[continuity]

theorem is_R_or_C.continuous_of_real {K : Type u_1} [is_R_or_C K] :

@[continuity]

theorem is_R_or_C.continuous_norm_sq {K : Type u_1} [is_R_or_C K] :

continuous ⇑is_R_or_C.norm_sq