Results on TrivSqZeroExt R M related to the norm

This file contains results about NormedSpace.exp for TrivSqZeroExt.

It also contains a definition of the $ℓ^1$ norm, which defines $\|r + m\| \coloneqq \|r\| + \|m\|$. This is not a particularly canonical choice of definition, but it is sufficient to provide a NormedAlgebra instance, and thus enables NormedSpace.exp_add_of_commute to be used on TrivSqZeroExt. If the non-canonicity becomes problematic in future, we could keep the collection of instances behind an open scoped.

Main results

• TrivSqZeroExt.fst_exp
• TrivSqZeroExt.snd_exp
• TrivSqZeroExt.exp_inl
• TrivSqZeroExt.exp_inr
• The $ℓ^1$ norm on TrivSqZeroExt:
  • TrivSqZeroExt.instL1SeminormedAddCommGroup
  • TrivSqZeroExt.instL1SeminormedRing
  • TrivSqZeroExt.instL1SeminormedCommRing
  • TrivSqZeroExt.instL1BoundedSMul
  • TrivSqZeroExt.instL1NormedAddCommGroup
  • TrivSqZeroExt.instL1NormedRing
  • TrivSqZeroExt.instL1NormedCommRing
  • TrivSqZeroExt.instL1NormedSpace
  • TrivSqZeroExt.instL1NormedAlgebra

TODO

• 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).

@[simp]

theorem TrivSqZeroExt.fst_expSeries (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (n : ℕ) : ((NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) n) fun (x_1 : Fin n) => x).fst = (NormedSpace.expSeries 𝕜 R n) fun (x_1 : Fin n) => x.fst

theorem TrivSqZeroExt.snd_expSeries_of_smul_comm (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) (n : ℕ) : ((NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) (n + 1)) fun (x_1 : Fin (n + 1)) => x).snd = ((NormedSpace.expSeries 𝕜 R n) fun (x_1 : Fin n) => x.fst) • x.snd

theorem TrivSqZeroExt.hasSum_snd_expSeries_of_smul_comm (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) {e : R} (h : HasSum (fun (n : ℕ) => (NormedSpace.expSeries 𝕜 R n) fun (x_1 : Fin n) => x.fst) e) : HasSum (fun (n : ℕ) => ((NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) n) fun (x_1 : 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 TrivSqZeroExt.hasSum_expSeries_of_smul_comm (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] (x : TrivSqZeroExt R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) {e : R} (h : HasSum (fun (n : ℕ) => (NormedSpace.expSeries 𝕜 R n) fun (x_1 : Fin n) => x.fst) e) : HasSum (fun (n : ℕ) => (NormedSpace.expSeries 𝕜 (TrivSqZeroExt R M) n) fun (x_1 : Fin n) => x) (TrivSqZeroExt.inl e + TrivSqZeroExt.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 TrivSqZeroExt.exp_def_of_smul_comm (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) : NormedSpace.exp 𝕜 x = TrivSqZeroExt.inl (NormedSpace.exp 𝕜 x.fst) + TrivSqZeroExt.inr (NormedSpace.exp 𝕜 x.fst • x.snd)

@[simp]

theorem TrivSqZeroExt.exp_inl (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : R) : NormedSpace.exp 𝕜 (TrivSqZeroExt.inl x) = TrivSqZeroExt.inl (NormedSpace.exp 𝕜 x)

@[simp]

theorem TrivSqZeroExt.exp_inr (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [Ring R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (m : M) : NormedSpace.exp 𝕜 (TrivSqZeroExt.inr m) = 1 + TrivSqZeroExt.inr m

theorem TrivSqZeroExt.exp_def (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [CommRing R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [IsScalarTower 𝕜 R M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) : NormedSpace.exp 𝕜 x = TrivSqZeroExt.inl (NormedSpace.exp 𝕜 x.fst) + TrivSqZeroExt.inr (NormedSpace.exp 𝕜 x.fst • x.snd)

@[simp]

theorem TrivSqZeroExt.fst_exp (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [CommRing R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [IsScalarTower 𝕜 R M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) : (NormedSpace.exp 𝕜 x).fst = NormedSpace.exp 𝕜 x.fst

@[simp]

theorem TrivSqZeroExt.snd_exp (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [CommRing R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [IsScalarTower 𝕜 R M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) : (NormedSpace.exp 𝕜 x).snd = NormedSpace.exp 𝕜 x.fst • x.snd

theorem TrivSqZeroExt.eq_smul_exp_of_invertible (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [Field 𝕜] [CharZero 𝕜] [CommRing R] [AddCommGroup M] [Algebra 𝕜 R] [Module 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [IsScalarTower 𝕜 R M] [TopologicalSpace R] [TopologicalSpace M] [TopologicalRing R] [TopologicalAddGroup M] [ContinuousSMul R M] [ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M) [Invertible x.fst] : x = x.fst • NormedSpace.exp 𝕜 (⅟x.fst • TrivSqZeroExt.inr x.snd)

Polar form of trivial-square-zero extension.

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

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

The $ℓ^1$ norm on the trivial square zero extension

instance TrivSqZeroExt.instL1SeminormedAddCommGroup {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] : SeminormedAddCommGroup (TrivSqZeroExt R M)

Equations

• TrivSqZeroExt.instL1SeminormedAddCommGroup = inferInstanceAs (SeminormedAddCommGroup (WithLp 1 (R × M)))

theorem TrivSqZeroExt.norm_def {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] (x : TrivSqZeroExt R M) : ‖x‖ = ‖x.fst‖ + ‖x.snd‖

theorem TrivSqZeroExt.nnnorm_def {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] (x : TrivSqZeroExt R M) : ‖x‖₊ = ‖x.fst‖₊ + ‖x.snd‖₊

@[simp]

theorem TrivSqZeroExt.norm_inl {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] (r : R) : ‖TrivSqZeroExt.inl r‖ = ‖r‖

@[simp]

theorem TrivSqZeroExt.norm_inr {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] (m : M) : ‖TrivSqZeroExt.inr m‖ = ‖m‖

@[simp]

theorem TrivSqZeroExt.nnnorm_inl {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] (r : R) : ‖TrivSqZeroExt.inl r‖₊ = ‖r‖₊

@[simp]

theorem TrivSqZeroExt.nnnorm_inr {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] (m : M) : ‖TrivSqZeroExt.inr m‖₊ = ‖m‖₊

instance TrivSqZeroExt.instL1SeminormedRing {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [BoundedSMul R M] [BoundedSMul Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : SeminormedRing (TrivSqZeroExt R M)

Equations

• TrivSqZeroExt.instL1SeminormedRing = let __spread.0 := inferInstance; let __spread.1 := inferInstance; SeminormedRing.mk ⋯ ⋯

instance TrivSqZeroExt.instL1BoundedSMul {S : Type u_2} {R : Type u_3} {M : Type u_4} [SeminormedCommRing S] [SeminormedRing R] [SeminormedAddCommGroup M] [Algebra S R] [Module S M] [Module R M] [Module Rᵐᵒᵖ M] [BoundedSMul S R] [BoundedSMul S M] [BoundedSMul R M] [BoundedSMul Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : BoundedSMul S (TrivSqZeroExt R M)

Equations

• ⋯ = ⋯

instance TrivSqZeroExt.instNormOneClass {R : Type u_3} {M : Type u_4} [SeminormedRing R] [SeminormedAddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [BoundedSMul R M] [BoundedSMul Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [NormOneClass R] : NormOneClass (TrivSqZeroExt R M)

Equations

• ⋯ = ⋯

instance TrivSqZeroExt.instL1SeminormedCommRing {R : Type u_3} {M : Type u_4} [SeminormedCommRing R] [SeminormedAddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [BoundedSMul R M] : SeminormedCommRing (TrivSqZeroExt R M)

Equations

• TrivSqZeroExt.instL1SeminormedCommRing = let __spread.0 := inferInstance; let __spread.1 := inferInstance; SeminormedCommRing.mk ⋯

instance TrivSqZeroExt.instL1NormedAddCommGroup {R : Type u_3} {M : Type u_4} [NormedRing R] [NormedAddCommGroup M] : NormedAddCommGroup (TrivSqZeroExt R M)

Equations

• TrivSqZeroExt.instL1NormedAddCommGroup = inferInstanceAs (NormedAddCommGroup (WithLp 1 (R × M)))

instance TrivSqZeroExt.instL1NormedRing {R : Type u_3} {M : Type u_4} [NormedRing R] [NormedAddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [BoundedSMul R M] [BoundedSMul Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] : NormedRing (TrivSqZeroExt R M)

Equations

• TrivSqZeroExt.instL1NormedRing = let __spread.0 := inferInstance; let __spread.1 := inferInstance; NormedRing.mk ⋯ ⋯

instance TrivSqZeroExt.instL1NormedCommRing {R : Type u_3} {M : Type u_4} [NormedCommRing R] [NormedAddCommGroup M] [Module R M] [Module Rᵐᵒᵖ M] [IsCentralScalar R M] [BoundedSMul R M] : NormedCommRing (TrivSqZeroExt R M)

Equations

• TrivSqZeroExt.instL1NormedCommRing = let __spread.0 := inferInstance; let __spread.1 := inferInstance; NormedCommRing.mk ⋯

instance TrivSqZeroExt.instL1NormedSpace (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [NormedField 𝕜] [NormedRing R] [NormedAddCommGroup M] [NormedAlgebra 𝕜 R] [NormedSpace 𝕜 M] : NormedSpace 𝕜 (TrivSqZeroExt R M)

Equations

• TrivSqZeroExt.instL1NormedSpace 𝕜 = inferInstanceAs (NormedSpace 𝕜 (WithLp 1 (R × M)))

instance TrivSqZeroExt.instL1NormedAlgebra (𝕜 : Type u_1) {R : Type u_3} {M : Type u_4} [NormedField 𝕜] [NormedRing R] [NormedAddCommGroup M] [NormedAlgebra 𝕜 R] [NormedSpace 𝕜 M] [Module R M] [Module Rᵐᵒᵖ M] [BoundedSMul R M] [BoundedSMul Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] [IsScalarTower 𝕜 R M] [IsScalarTower 𝕜 Rᵐᵒᵖ M] : NormedAlgebra 𝕜 (TrivSqZeroExt R M)

Equations

• TrivSqZeroExt.instL1NormedAlgebra 𝕜 = NormedAlgebra.mk ⋯