mathlib3 documentation

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 #

TODO #

theorem triv_sq_zero_ext.has_sum_fst_exp_series (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [topological_space R] [topological_space M] [field 𝕜] [ring R] [add_comm_group M] [algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [is_scalar_tower 𝕜 Rᵐᵒᵖ M] [topological_ring R] [topological_add_group M] [has_continuous_smul R 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)).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} [topological_space R] [topological_space M] [field 𝕜] [char_zero 𝕜] [ring R] [add_comm_group M] [algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [is_scalar_tower 𝕜 Rᵐᵒᵖ M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [has_continuous_smul Rᵐᵒᵖ M] (x : triv_sq_zero_ext R M) (hx : mul_opposite.op x.fst x.snd = x.fst x.snd) {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)).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} [topological_space R] [topological_space M] [field 𝕜] [char_zero 𝕜] [ring R] [add_comm_group M] [algebra 𝕜 R] [module R M] [module Rᵐᵒᵖ M] [smul_comm_class R Rᵐᵒᵖ M] [module 𝕜 M] [is_scalar_tower 𝕜 R M] [is_scalar_tower 𝕜 Rᵐᵒᵖ M] [topological_ring R] [topological_add_group M] [has_continuous_smul R M] [has_continuous_smul Rᵐᵒᵖ M] (x : triv_sq_zero_ext R M) (hx : mul_opposite.op x.fst x.snd = x.fst x.snd) {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).

@[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

Polar form of trivial-square-zero extension.

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