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 #

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) :

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.