# mathlib3documentation

analysis.normed_space.triv_sq_zero_ext

# Results on triv_sq_zero_ext R M related to the norm #

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

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

## Main results #

• triv_sq_zero_ext.fst_exp
• triv_sq_zero_ext.snd_exp
• triv_sq_zero_ext.exp_inl
• triv_sq_zero_ext.exp_inr

## TODO #

• Actually define a sensible norm on triv_sq_zero_ext R M, so that we have access to lemmas like exp_add.
• Generalize more of these results to non-commutative R. In principle, under sufficient conditions we should expect (exp 𝕜 x).snd = ∫ t in 0..1, exp 𝕜 (t • x.fst) • op (exp 𝕜 ((1 - t) • x.fst)) • x.snd (Physics.SE, and https://link.springer.com/chapter/10.1007/978-3-540-44953-9_2).
theorem triv_sq_zero_ext.has_sum_fst_exp_series (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [field 𝕜] [ring R] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [ M] (x : M) {e : R} (h : has_sum (λ (n : ), R n) (λ (_x : fin n), x.fst)) e) :
has_sum (λ (n : ), ( M) n) (λ (_x : fin n), x)).fst) e

If exp R x.fst converges to e then (exp R x).fst converges to e.

theorem triv_sq_zero_ext.has_sum_snd_exp_series_of_smul_comm (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [field 𝕜] [char_zero 𝕜] [ring R] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [ M] (x : M) (hx : = x.fst x.snd) {e : R} (h : has_sum (λ (n : ), R n) (λ (_x : fin n), x.fst)) e) :
has_sum (λ (n : ), ( M) n) (λ (_x : fin n), x)).snd) (e x.snd)

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

theorem triv_sq_zero_ext.has_sum_exp_series_of_smul_comm (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [field 𝕜] [char_zero 𝕜] [ring R] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [ M] (x : M) (hx : = x.fst x.snd) {e : R} (h : has_sum (λ (n : ), R n) (λ (_x : fin n), x.fst)) e) :
has_sum (λ (n : ), M) n) (λ (_x : fin n), x)) + 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_of_smul_comm (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_ring R] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [ M] [t2_space R] [t2_space M] (x : M) (hx : = 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_ring R] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [ M] [t2_space R] [t2_space M] (x : R) :
@[simp]
theorem triv_sq_zero_ext.exp_inr (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [normed_ring R] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [ M] [t2_space R] [t2_space M] (m : M) :
exp 𝕜 =
theorem triv_sq_zero_ext.exp_def (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [t2_space R] [t2_space M] (x : M) :
@[simp]
theorem triv_sq_zero_ext.fst_exp (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [is_R_or_C 𝕜] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [t2_space R] [t2_space M] (x : 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 𝕜] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [t2_space R] [t2_space M] (x : M) :
(exp 𝕜 x).snd = exp 𝕜 x.fst x.snd
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 𝕜] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [t2_space R] [t2_space M] (x : M) [invertible x.fst] :
x = x.fst exp 𝕜 ( x.fst

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] [ R] [ M] [ M] [ M] [ M] [ M] [ M] [t2_space R] [t2_space M] (x : M) (hx : x.fst 0) :
x = x.fst exp 𝕜 ((x.fst)⁻¹

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