import analysis.normed_space.basic

import analysis.normed_space.exponential

import topology.instances.triv_sq_zero_ext

variables (𝕜 : Type*) {R M : Type*}

local notation `tsze` := triv_sq_zero_ext

namespace triv_sq_zero_ext

section topology

variables [topological_space R] [topological_space M]

lemma has_sum_exp_series [field 𝕜] [char_zero 𝕜] [comm_ring R]

[add_comm_group M] [algebra 𝕜 R] [module R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M]

[topological_ring R] [topological_add_group M] [has_continuous_smul R M]

(x : tsze R M) {e : R} (h : has_sum (λ n, exp_series 𝕜 R n (λ _, x.fst)) e) :

has_sum (λ n, exp_series 𝕜 (tsze R M) n (λ _, x)) (inl e + inr (e • x.snd)) :=

simp_rw [exp_series_apply_eq] at *,

conv

{ congr,

funext,

rw [←inl_fst_add_inr_snd_eq (x ^ _), fst_pow, snd_pow, smul_add, ←inr_smul,

←inl_smul, nsmul_eq_smul_cast 𝕜 n, smul_smul, inv_mul_eq_div, ←inv_div, ←smul_assoc], },

refine (has_sum_inl M h).add (has_sum_inr M _),

apply has_sum.smul_const,

rw [←has_sum_nat_add_iff' 1], swap, apply_instance,

rw [finset.range_one, finset.sum_singleton, nat.cast_zero, div_zero, inv_zero, zero_smul,

sub_zero],

simp_rw [←nat.succ_eq_add_one, nat.pred_succ, nat.factorial_succ, nat.cast_mul,

←nat.succ_eq_add_one,

mul_div_cancel_left _ ((@nat.cast_ne_zero 𝕜 _ _ _).mpr $ nat.succ_ne_zero _)],

exact h,

end topology

section normed_ring

variables [is_R_or_C 𝕜] [normed_comm_ring R] [add_comm_group M]

variables [normed_algebra 𝕜 R] [module R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M]

variables [topological_space M] [topological_ring R]

variables [topological_add_group M] [has_continuous_smul R M]

variables [complete_space R] [t2_space R] [t2_space M]

lemma exp_def (x : tsze R M) : exp 𝕜 x = inl (exp 𝕜 x.fst) + inr (exp 𝕜 x.fst • x.snd) :=

simp_rw [exp, formal_multilinear_series.sum],

refine (has_sum_exp_series 𝕜 x _).tsum_eq,

exact exp_series_has_sum_exp _,

@[simp] lemma fst_exp (x : tsze R M) : fst (exp 𝕜 x) = exp 𝕜 x.fst :=

by rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]

@[simp] lemma snd_exp (x : tsze R M) : snd (exp 𝕜 x) = exp 𝕜 x.fst • x.snd :=

by rw [exp_def, snd_add, snd_inl, snd_inr, zero_add]

@[simp] lemma exp_inl (x : R) : exp 𝕜 (inl x : tsze R M) = inl (exp 𝕜 x) :=

by rw [exp_def, fst_inl, snd_inl, smul_zero, inr_zero, add_zero]

@[simp] lemma exp_inr (m : M) : exp 𝕜 (inr m : tsze R M) = 1 + inr m :=

by rw [exp_def, fst_inr, exp_zero, snd_inr, one_smul, inl_one]

lemma eq_smul_exp_of_invertible (x : tsze R M) [invertible x.fst] :

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

by rw [←inr_smul, exp_inr, smul_add, ←inl_one, ←inl_smul, ←inr_smul, smul_eq_mul, mul_one,

smul_smul, mul_inv_of_self, one_smul, inl_fst_add_inr_snd_eq]

end normed_ring

section normed_field

variables [is_R_or_C 𝕜] [normed_field R] [add_comm_group M]

variables [normed_algebra 𝕜 R] [module R M] [module 𝕜 M] [is_scalar_tower 𝕜 R M]

variables [topological_space M] [topological_ring R]

variables [topological_add_group M] [has_continuous_smul R M]

variables [complete_space R] [t2_space R] [t2_space M]

lemma eq_smul_exp_of_ne_zero (x : tsze R M) (hx : x.fst ≠ 0) :

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

letI : invertible x.fst := invertible_of_nonzero hx,

exact eq_smul_exp_of_invertible _ _

end normed_field

end triv_sq_zero_ext

import algebra.triv_sq_zero_ext

import topology.algebra.infinite_sum

import topology.algebra.module.basic

variables {α S R M : Type*}

local notation `tsze` := triv_sq_zero_ext

namespace triv_sq_zero_ext

variables [topological_space R] [topological_space M]

instance : topological_space (tsze R M) :=

topological_space.induced fst ‹_› ⊓ topological_space.induced snd ‹_›

instance [t2_space R] [t2_space M] : t2_space (tsze R M) :=

prod.t2_space

lemma nhds_def (x : tsze R M) : nhds x = (nhds x.fst).prod (nhds x.snd) :=

by cases x; exact nhds_prod_eq

lemma nhds_inl [has_zero M] (x : R) : nhds (inl x : tsze R M) = (nhds x).prod (nhds 0) := nhds_def _

lemma nhds_inr [has_zero R] (m : M) : nhds (inr m : tsze R M) = (nhds 0).prod (nhds m) := nhds_def _

lemma continuous_fst : continuous (fst : tsze R M → R) := continuous_fst

lemma continuous_snd : continuous (snd : tsze R M → M) := continuous_snd

lemma continuous_inl [has_zero M] : continuous (inl : R → tsze R M) :=

continuous_id.prod_mk continuous_const

lemma continuous_inr [has_zero R] : continuous (inr : M → tsze R M) :=

continuous_const.prod_mk continuous_id

lemma embedding_inl [has_zero M] : embedding (inl : R → tsze R M) :=

embedding_of_embedding_compose continuous_inl continuous_fst embedding_id

lemma embedding_inr [has_zero R] : embedding (inr : M → tsze R M) :=

embedding_of_embedding_compose continuous_inr continuous_snd embedding_id

variables (R M)

def fst_clm [comm_semiring R] [add_comm_monoid M] [module R M] : tsze R M →L[R] R :=

{ to_fun := fst,

.. continuous_linear_map.fst R R M }

def snd_clm [comm_semiring R] [add_comm_monoid M] [module R M] : tsze R M →L[R] M :=

{ to_fun := snd,

cont := continuous_snd,

.. continuous_linear_map.snd R R M }

def inl_clm [comm_semiring R] [add_comm_monoid M] [module R M] : R →L[R] tsze R M :=

{ to_fun := inl,

.. continuous_linear_map.inl R R M }

def inr_clm [comm_semiring R] [add_comm_monoid M] [module R M] : M →L[R] tsze R M :=

{ to_fun := inr,

.. continuous_linear_map.inr R R M }

variables {R M}

instance [has_add R] [has_add M]

[has_continuous_add R] [has_continuous_add M] :

has_continuous_add (tsze R M) :=

prod.has_continuous_add

instance [has_mul R] [has_add M] [has_smul R M]

[has_continuous_mul R] [has_continuous_smul R M] [has_continuous_add M] :

has_continuous_mul (tsze R M) :=

⟨((continuous_fst.comp _root_.continuous_fst).mul (continuous_fst.comp _root_.continuous_snd))

.prod_mk $

((continuous_fst.comp _root_.continuous_fst).smul

(continuous_snd.comp _root_.continuous_snd)).add

((continuous_fst.comp _root_.continuous_snd).smul

(continuous_snd.comp _root_.continuous_fst))⟩

instance [has_neg R] [has_neg M]

[has_continuous_neg R] [has_continuous_neg M] :

has_continuous_neg (tsze R M) :=

prod.has_continuous_neg

instance [semiring R] [add_comm_monoid M] [module R M]

[topological_semiring R] [has_continuous_add M] [has_continuous_smul R M] :

topological_semiring (tsze R M) :=

{}

instance [comm_ring R] [add_comm_group M] [module R M]

[topological_ring R] [topological_add_group M] [has_continuous_smul R M] :

topological_ring (tsze R M) :=

{}

instance [has_smul S R] [has_smul S M]

[has_continuous_const_smul S R] [has_continuous_const_smul S M] :

has_continuous_const_smul S (tsze R M) :=

prod.has_continuous_const_smul

instance [topological_space S] [has_smul S R] [has_smul S M]

[has_continuous_smul S R] [has_continuous_smul S M] :

has_continuous_smul S (tsze R M) :=

prod.has_continuous_smul

variables (M)

lemma has_sum_inl [add_comm_monoid R] [add_comm_monoid M] {f : α → R} {a : R} (h : has_sum f a) :

has_sum (λ x, inl (f x)) (inl a : tsze R M) :=

h.map (⟨inl, inl_zero _, inl_add _⟩ : R →+ tsze R M) continuous_inl

lemma has_sum_inr [add_comm_monoid R] [add_comm_monoid M] {f : α → M} {a : M} (h : has_sum f a) :

has_sum (λ x, inr (f x)) (inr a : tsze R M) :=

h.map (⟨inr, inr_zero _, inr_add _⟩ : M →+ tsze R M) continuous_inr

lemma has_sum_fst [add_comm_monoid R] [add_comm_monoid M] {f : α → tsze R M} {a : tsze R M}

(h : has_sum f a) : has_sum (λ x, fst (f x)) (fst a) :=

h.map (⟨fst, fst_zero, fst_add⟩ : tsze R M →+ R) continuous_fst

lemma has_sum_snd [add_comm_monoid R] [add_comm_monoid M] {f : α → tsze R M} {a : tsze R M}

(h : has_sum f a) : has_sum (λ x, snd (f x)) (snd a) :=

h.map (⟨snd, snd_zero, snd_add⟩ : tsze R M →+ M) continuous_snd

end triv_sq_zero_ext