feat(analysis/normed_space/triv_sq_zero_ext): exponential of dual num…

…bers (#18200)

In order for convergence to be well-defined, we put the product topology on `triv_zero_sq_ext R M` via its obvious internal representation as a product.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Exponentials.20in.20seminormed.20algebras/near/321870256).

src/analysis/normed_space/dual_number.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.dual_number
+import analysis.normed_space.triv_sq_zero_ext
+
+/-!
+# Results on `dual_number R` related to the norm
+
+These are just restatements of similar statements about `triv_sq_zero_ext R M`.
+
+## Main results
+
+* `exp_eps`
+
+-/
+
+namespace dual_number
+open triv_sq_zero_ext
+
+variables (𝕜 : Type*) {R : Type*}
+
+variables [is_R_or_C 𝕜] [normed_comm_ring R] [normed_algebra 𝕜 R]
+variables [topological_ring R] [complete_space R] [t2_space R]
+
+@[simp] lemma exp_eps : exp 𝕜 (eps : dual_number R) = 1 + eps :=
+exp_inr _ _
+
+@[simp] lemma exp_smul_eps (r : R) : exp 𝕜 (r • eps : dual_number R) = 1 + r • eps :=
+by rw [eps, ←inr_smul, exp_inr]
+
+end dual_number

src/analysis/normed_space/triv_sq_zero_ext.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import analysis.normed_space.basic
+import analysis.normed_space.exponential
+import topology.instances.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.
+
+TODO: actually define a sensible norm on `triv_sq_zero_ext R M`, so that we have access to lemmas
+like `exp_add`.
+
+## 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`
+
+-/
+
+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]
+
+
+/-- If `exp R x.fst` converges to `e` then `exp R x` converges to `inl e + inr (e • x.snd)`. -/
+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)) :=
+begin
+  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
+
+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) :=
+begin
+  simp_rw [exp, formal_multilinear_series.sum],
+  refine (has_sum_exp_series 𝕜 x _).tsum_eq,
+  exact exp_series_has_sum_exp _,
+end
+
+@[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]
+
+/-- Polar form of trivial-square-zero extension. -/
+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]
+
+/-- More convenient version of `triv_sq_zero_ext.eq_smul_exp_of_invertible` for when `R` is a
+field. -/
+lemma eq_smul_exp_of_ne_zero (x : tsze R M) (hx : x.fst ≠ 0) :
+  x = x.fst • exp 𝕜 (x.fst⁻¹ • inr x.snd) :=
+begin
+  letI : invertible x.fst := invertible_of_nonzero hx,
+  exact eq_smul_exp_of_invertible _ _
+end
+
+end normed_field
+
+end triv_sq_zero_ext

src/topology/instances/triv_sq_zero_ext.lean

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2023 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import algebra.triv_sq_zero_ext
+import topology.algebra.infinite_sum
+import topology.algebra.module.basic
+
+/-!
+# Topology on `triv_sq_zero_ext R M`
+
+The type `triv_sq_zero_ext R M` inherits the topology from `R × M`.
+
+Note that this is not the topology induced by the seminorm on the dual numbers suggested by
+[this Math.SE answer](https://math.stackexchange.com/a/1056378/1896), which instead induces
+the topology pulled back through the projection map `triv_sq_zero_ext.fst : tsze R M → R`.
+Obviously, that topology is not Hausdorff and using it would result in `exp` converging to more than
+one value.
+
+## Main results
+
+* `triv_sq_zero_ext.topological_ring`: the ring operations are continuous
+
+-/
+
+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)
+
+/-- `triv_sq_zero_ext.fst` as a continuous linear map. -/
+@[simps]
+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 }
+
+/-- `triv_sq_zero_ext.snd` as a continuous linear map. -/
+@[simps]
+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 }
+
+/-- `triv_sq_zero_ext.inl` as a continuous linear map. -/
+@[simps]
+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 }
+
+/-- `triv_sq_zero_ext.inr` as a continuous linear map. -/
+@[simps]
+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