mathlib documentation

analysis.normed_space.triv_sq_zero_ext

Results on `triv_sq_zero_ext R M` related to the norm #

For now, this file contains results about exp for this type.

Main results #

TODO #

Actually define a sensible norm on triv_sq_zero_ext R M, so that we have access to lemmas like exp_add.
Generalize some of these results to non-commutative R.

theorem triv_sq_zero_ext.has_sum_exp_series (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [topological_space R] [topological_space M] [field 𝕜] [char_zero 𝕜] [comm_ring R] [add_comm_group M] [algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] (x : triv_sq_zero_ext R M) {e : R} (h : has_sum (λ (n : ℕ), ⇑(exp_series 𝕜 R n) (λ (_x : fin n), x.fst)) e) :

has_sum (λ (n : ℕ), ⇑(exp_series 𝕜 (triv_sq_zero_ext R M) n) (λ (_x : fin n), x)) (triv_sq_zero_ext.inl e + triv_sq_zero_ext.inr (e • x.snd))

If exp R x.fst converges to e then exp R x converges to inl e + inr (e • x.snd).

theorem triv_sq_zero_ext.exp_def (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_comm_ring R] [add_comm_group M] [normed_algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [topological_space M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [complete_space R] [t2_space R] [t2_space M] (x : triv_sq_zero_ext R M) :

exp 𝕜 x = triv_sq_zero_ext.inl (exp 𝕜 x.fst) + triv_sq_zero_ext.inr (exp 𝕜 x.fst • x.snd)

@[simp]

theorem triv_sq_zero_ext.fst_exp (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_comm_ring R] [add_comm_group M] [normed_algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [topological_space M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [complete_space R] [t2_space R] [t2_space M] (x : triv_sq_zero_ext R M) :

(exp 𝕜 x).fst = exp 𝕜 x.fst

@[simp]

theorem triv_sq_zero_ext.snd_exp (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_comm_ring R] [add_comm_group M] [normed_algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [topological_space M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [complete_space R] [t2_space R] [t2_space M] (x : triv_sq_zero_ext R M) :

(exp 𝕜 x).snd = exp 𝕜 x.fst • x.snd

@[simp]

theorem triv_sq_zero_ext.exp_inl (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_comm_ring R] [add_comm_group M] [normed_algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [topological_space M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [complete_space R] [t2_space R] [t2_space M] (x : R) :

exp 𝕜 (triv_sq_zero_ext.inl x) = triv_sq_zero_ext.inl (exp 𝕜 x)

@[simp]

theorem triv_sq_zero_ext.exp_inr (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_comm_ring R] [add_comm_group M] [normed_algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [topological_space M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [complete_space R] [t2_space R] [t2_space M] (m : M) :

exp 𝕜 (triv_sq_zero_ext.inr m) = 1 + triv_sq_zero_ext.inr m

theorem triv_sq_zero_ext.eq_smul_exp_of_invertible (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_comm_ring R] [add_comm_group M] [normed_algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [topological_space M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [complete_space R] [t2_space R] [t2_space M] (x : triv_sq_zero_ext R M) [invertible x.fst] :

x = x.fst • exp 𝕜 (⅟ x.fst • triv_sq_zero_ext.inr x.snd)

Polar form of trivial-square-zero extension.

theorem triv_sq_zero_ext.eq_smul_exp_of_ne_zero (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_field R] [add_comm_group M] [normed_algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [is_central_scalar R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [topological_space M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [complete_space R] [t2_space R] [t2_space M] (x : triv_sq_zero_ext R M) (hx : x.fst ≠ 0) :

x = x.fst • exp 𝕜 ((x.fst)⁻¹ • triv_sq_zero_ext.inr x.snd)

More convenient version of triv_sq_zero_ext.eq_smul_exp_of_invertible for when R is a field.