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 #
- Actually define a sensible norm on
triv_sq_zero_ext R M, so that we have access to lemmas likeexp_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}
[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).
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]
[add_comm_group M]
[normed_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_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R M]
[has_continuous_smul Rᵐᵒᵖ M]
[complete_space R]
[t2_space R]
[t2_space M]
(x : triv_sq_zero_ext R M)
(hx : mul_opposite.op x.fst • x.snd = 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]
[add_comm_group M]
[normed_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_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R 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_ring R]
[add_comm_group M]
[normed_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_space M]
[topological_ring R]
[topological_add_group M]
[has_continuous_smul R 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.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) :
@[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) :
@[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) :
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] :
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) :
More convenient version of triv_sq_zero_ext.eq_smul_exp_of_invertible for when R is a
field.