is_R_or_C: a typeclass for ℝ or ℂ #
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 ℂ.
Possible applications include defining inner products and Hilbert spaces for both the real and complex case. One would produce 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).
@[class]
- to_nondiscrete_normed_field : nondiscrete_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 (⇑conj z) = ⇑is_R_or_C.re z
- conj_im_ax : ∀ (z : K), ⇑is_R_or_C.im (⇑conj z) = -⇑is_R_or_C.im z
- conj_I_ax : ⇑conj 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
- inv_def_ax : ∀ (z : K), z⁻¹ = (⇑conj z) * ⇑(algebra_map ℝ K) (∥z∥ ^ 2)⁻¹
- div_I_ax : ∀ (z : K), z / is_R_or_C.I = -z * is_R_or_C.I
This typeclass captures properties shared by ℝ and ℂ, with an API that closely matches that of ℂ.
Instances
@[protected, instance]
Equations
- is_R_or_C.algebra_map_coe = {coe := ⇑(algebra_map ℝ K)}
@[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]
@[simp, norm_cast]
@[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} :
⇑is_R_or_C.re z = ⇑is_R_or_C.re w → ⇑is_R_or_C.im z = ⇑is_R_or_C.im 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_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
The imaginary unit, I #
@[simp]
The imaginary unit.
@[simp]
@[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 (⇑conj 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 (⇑conj z) = -⇑is_R_or_C.im z
@[simp]
@[simp]
theorem
is_R_or_C.conj_eq_re_sub_im
{K : Type u_1}
[is_R_or_C K]
(z : K) :
⇑conj z = ↑(⇑is_R_or_C.re z) - (↑(⇑is_R_or_C.im z)) * is_R_or_C.I
Conjugation as a ring equivalence. This is used to convert the inner product into a sesquilinear product.
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_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
@[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]
@[simp]
@[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 * ⇑conj 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
The pseudo-coercion of_real as a ring_hom.
Equations
theorem
is_R_or_C.sub_conj
{K : Type u_1}
[is_R_or_C K]
(z : K) :
z - ⇑conj z = (2 * ↑(⇑is_R_or_C.im z)) * is_R_or_C.I
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 * ⇑conj w)
Inversion #
@[simp]
@[simp]
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
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
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]
@[simp]
@[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
@[protected, instance]
Equations
Cast lemmas #
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
@[simp, norm_cast]
Characteristic zero #
ℝ and ℂ are both of characteristic zero.
Note: This is not registered as an instance to avoid having multiple instances on ℝ and ℂ.
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 * (⇑conj z - z) / 2
Absolute value #
The complex absolute value function, defined as the square root of the norm squared.
Equations
@[simp, norm_cast]
theorem
is_R_or_C.abs_of_nonneg
{K : Type u_1}
[is_R_or_C K]
{r : ℝ}
(h : 0 ≤ r) :
is_R_or_C.abs ↑r = r
theorem
is_R_or_C.mul_self_abs
{K : Type u_1}
[is_R_or_C K]
(z : K) :
(is_R_or_C.abs z) * is_R_or_C.abs z = ⇑is_R_or_C.norm_sq z
@[simp]
@[simp]
theorem
is_R_or_C.abs_conj
{K : Type u_1}
[is_R_or_C K]
(z : K) :
is_R_or_C.abs (⇑conj z) = is_R_or_C.abs z
@[simp]
theorem
is_R_or_C.abs_mul
{K : Type u_1}
[is_R_or_C K]
(z w : K) :
is_R_or_C.abs (z * w) = (is_R_or_C.abs z) * is_R_or_C.abs w
theorem
is_R_or_C.im_eq_zero_of_le
{K : Type u_1}
[is_R_or_C K]
{a : K}
(h : is_R_or_C.abs 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 : is_R_or_C.abs a ≤ ⇑is_R_or_C.re a) :
↑(⇑is_R_or_C.re a) = a
theorem
is_R_or_C.abs_add
{K : Type u_1}
[is_R_or_C K]
(z w : K) :
is_R_or_C.abs (z + w) ≤ is_R_or_C.abs z + is_R_or_C.abs w
@[protected, instance]
@[simp]
@[simp]
@[simp]
theorem
is_R_or_C.abs_neg
{K : Type u_1}
[is_R_or_C K]
(z : K) :
is_R_or_C.abs (-z) = is_R_or_C.abs z
theorem
is_R_or_C.abs_sub
{K : Type u_1}
[is_R_or_C K]
(z w : K) :
is_R_or_C.abs (z - w) = is_R_or_C.abs (w - z)
theorem
is_R_or_C.abs_sub_le
{K : Type u_1}
[is_R_or_C K]
(a b c : K) :
is_R_or_C.abs (a - c) ≤ is_R_or_C.abs (a - b) + is_R_or_C.abs (b - c)
@[simp]
theorem
is_R_or_C.abs_inv
{K : Type u_1}
[is_R_or_C K]
(z : K) :
is_R_or_C.abs z⁻¹ = (is_R_or_C.abs z)⁻¹
@[simp]
theorem
is_R_or_C.abs_div
{K : Type u_1}
[is_R_or_C K]
(z w : K) :
is_R_or_C.abs (z / w) = is_R_or_C.abs z / is_R_or_C.abs w
theorem
is_R_or_C.abs_abs_sub_le_abs_sub
{K : Type u_1}
[is_R_or_C K]
(z w : K) :
|is_R_or_C.abs z - is_R_or_C.abs w| ≤ is_R_or_C.abs (z - w)
theorem
is_R_or_C.abs_re_div_abs_le_one
{K : Type u_1}
[is_R_or_C K]
(z : K) :
|⇑is_R_or_C.re z / is_R_or_C.abs z| ≤ 1
theorem
is_R_or_C.abs_im_div_abs_le_one
{K : Type u_1}
[is_R_or_C K]
(z : K) :
|⇑is_R_or_C.im z / is_R_or_C.abs z| ≤ 1
@[simp, norm_cast]
theorem
is_R_or_C.norm_sq_eq_abs
{K : Type u_1}
[is_R_or_C K]
(x : K) :
⇑is_R_or_C.norm_sq x = is_R_or_C.abs x ^ 2
theorem
is_R_or_C.re_eq_abs_of_mul_conj
{K : Type u_1}
[is_R_or_C K]
(x : K) :
⇑is_R_or_C.re (x * ⇑conj x) = is_R_or_C.abs (x * ⇑conj x)
Cauchy sequences #
theorem
is_R_or_C.is_cau_seq_re
{K : Type u_1}
[is_R_or_C K]
(f : cau_seq K is_R_or_C.abs) :
is_cau_seq 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 is_R_or_C.abs) :
is_cau_seq abs (λ (n : ℕ), ⇑is_R_or_C.im (⇑f n))
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), _⟩
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_abs
{K : Type u_1}
[is_R_or_C K]
{f : ℕ → K}
(hf : is_cau_seq is_R_or_C.abs f) :
is_cau_seq abs (is_R_or_C.abs ∘ f)
@[protected, nolint, instance]
An is_R_or_C field is finite-dimensional over ℝ, since it is spanned by {1, I}.
theorem
finite_dimensional.proper_is_R_or_C
(K : Type u_1)
[is_R_or_C K]
(E : Type u_2)
[normed_group E]
[normed_space K E]
[finite_dimensional K E] :
A finite dimensional vector space Over an is_R_or_C is a proper metric space.
This is not an instance because it would cause a search for finite_dimensional ?x E before
is_R_or_C ?x.
@[protected, instance]
def
finite_dimensional.is_R_or_C.proper_space_span_singleton
(K : Type u_1)
[is_R_or_C K]
{E : Type u_2}
[normed_group E]
[normed_space K E]
(x : E) :
proper_space ↥(submodule.span K {x})
@[protected, instance]
Equations
- real.is_R_or_C = {to_nondiscrete_normed_field := real.nondiscrete_normed_field, 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, inv_def_ax := real.is_R_or_C._proof_13, div_I_ax := real.is_R_or_C._proof_14}
@[simp]
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]
@[simp]
@[continuity]
@[simp]
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]
@[simp]
@[continuity]
@[simp]
Conjugate as a linear isometry
Equations
@[simp]
Conjugate as a continuous linear equivalence
Equations
@[simp]
@[simp]
@[simp]
@[continuity]
The ℝ → K coercion, as a linear map
Equations
@[simp]
The ℝ → K coercion, as a linear isometry
Equations
@[simp]
The ℝ → K coercion, as a continuous linear map
@[simp]
@[simp]
@[simp]
@[continuity]