Results on TrivSqZeroExt R M related to the norm

For now, this file contains results about exp for this type.

Main results

• TrivSqZeroExt.fst_exp
• TrivSqZeroExt.snd_exp
• TrivSqZeroExt.exp_inl
• TrivSqZeroExt.exp_inr

TODO

• Actually define a sensible norm on TrivSqZeroExt R M, so that we have access to lemmas like exp_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 TrivSqZeroExt.hasSum_fst_expSeries (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [TopologicalSpace R] [TopologicalSpace M] [Field 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) {e : R} (h : HasSum (fun n => ↑(expSeries 𝕜 R n) fun x => TrivSqZeroExt.fst x) e) : HasSum (fun n => TrivSqZeroExt.fst (↑(expSeries 𝕜 (TrivSqZeroExt R M) n) fun x => x)) e

If exp R x.fst converges to e then (exp R x).fst converges to e.

theorem TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [TopologicalSpace R] [TopologicalSpace M] [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (hx : MulOpposite.op (TrivSqZeroExt.fst x) • TrivSqZeroExt.snd x = TrivSqZeroExt.fst x • TrivSqZeroExt.snd x) {e : R} (h : HasSum (fun n => ↑(expSeries 𝕜 R n) fun x => TrivSqZeroExt.fst x) e) : HasSum (fun n => TrivSqZeroExt.snd (↑(expSeries 𝕜 (TrivSqZeroExt R M) n) fun x => x)) (e • TrivSqZeroExt.snd x)

If exp R x.fst converges to e then (exp R x).snd converges to e • x.snd.

theorem TrivSqZeroExt.hasSum_expSeries_of_smul_comm (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [TopologicalSpace R] [TopologicalSpace M] [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (hx : MulOpposite.op (TrivSqZeroExt.fst x) • TrivSqZeroExt.snd x = TrivSqZeroExt.fst x • TrivSqZeroExt.snd x) {e : R} (h : HasSum (fun n => ↑(expSeries 𝕜 R n) fun x => TrivSqZeroExt.fst x) e) : HasSum (fun n => ↑(expSeries 𝕜 (TrivSqZeroExt R M) n) fun x => x) (TrivSqZeroExt.inl e + TrivSqZeroExt.inr (e • TrivSqZeroExt.snd x))

If exp R x.fst converges to e then exp R x converges to inl e + inr (e • x.snd).

theorem TrivSqZeroExt.exp_def_of_smul_comm (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [IsROrC 𝕜] [NormedRing R] [AddCommGroup M] [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [CompleteSpace R] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) (hx : MulOpposite.op (TrivSqZeroExt.fst x) • TrivSqZeroExt.snd x = TrivSqZeroExt.fst x • TrivSqZeroExt.snd x) : exp 𝕜 x = TrivSqZeroExt.inl (exp 𝕜 (TrivSqZeroExt.fst x)) + TrivSqZeroExt.inr (exp 𝕜 (TrivSqZeroExt.fst x) • TrivSqZeroExt.snd x)

@[simp]

theorem TrivSqZeroExt.exp_inl (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [IsROrC 𝕜] [NormedRing R] [AddCommGroup M] [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [CompleteSpace R] [T2Space R] [T2Space M] (x : R) : exp 𝕜 (TrivSqZeroExt.inl x) = TrivSqZeroExt.inl (exp 𝕜 x)

@[simp]

theorem TrivSqZeroExt.exp_inr (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [IsROrC 𝕜] [NormedRing R] [AddCommGroup M] [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [CompleteSpace R] [T2Space R] [T2Space M] (m : M) : exp 𝕜 (TrivSqZeroExt.inr m) = 1 + TrivSqZeroExt.inr m

theorem TrivSqZeroExt.exp_def (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [IsROrC 𝕜] [NormedCommRing R] [AddCommGroup M] [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [CompleteSpace R] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) : exp 𝕜 x = TrivSqZeroExt.inl (exp 𝕜 (TrivSqZeroExt.fst x)) + TrivSqZeroExt.inr (exp 𝕜 (TrivSqZeroExt.fst x) • TrivSqZeroExt.snd x)

@[simp]

theorem TrivSqZeroExt.fst_exp (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [IsROrC 𝕜] [NormedCommRing R] [AddCommGroup M] [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [CompleteSpace R] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) : TrivSqZeroExt.fst (exp 𝕜 x) = exp 𝕜 (TrivSqZeroExt.fst x)

@[simp]

theorem TrivSqZeroExt.snd_exp (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [IsROrC 𝕜] [NormedCommRing R] [AddCommGroup M] [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [CompleteSpace R] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) : TrivSqZeroExt.snd (exp 𝕜 x) = exp 𝕜 (TrivSqZeroExt.fst x) • TrivSqZeroExt.snd x

theorem TrivSqZeroExt.eq_smul_exp_of_invertible (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [IsROrC 𝕜] [NormedCommRing R] [AddCommGroup M] [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [CompleteSpace R] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) [Invertible (TrivSqZeroExt.fst x)] : x = TrivSqZeroExt.fst x • exp 𝕜 (⅟(TrivSqZeroExt.fst x) • TrivSqZeroExt.inr (TrivSqZeroExt.snd x))

Polar form of trivial-square-zero extension.

theorem TrivSqZeroExt.eq_smul_exp_of_ne_zero (𝕜 : Type u_1) {R : Type u_2} {M : Type u_3} [IsROrC 𝕜] [NormedField R] [AddCommGroup M] [NormedAlgebra 𝕜 R] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [Module 𝕜 M] [IsScalarTower 𝕜 R M] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [CompleteSpace R] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) (hx : TrivSqZeroExt.fst x ≠ 0) : x = TrivSqZeroExt.fst x • exp 𝕜 ((TrivSqZeroExt.fst x)⁻¹ • TrivSqZeroExt.inr (TrivSqZeroExt.snd x))

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