Documentation

Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt

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 #

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 NormedSpace.exp R x.fst converges to e then (NormedSpace.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 NormedSpace.exp R x.fst converges to e then NormedSpace.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] [BoundedSMul R M] [Module Rᵐᵒᵖ M] [BoundedSMul Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] :

SeminormedRing (TrivSqZeroExt R M)

Equations

TrivSqZeroExt.instL1SeminormedRing = 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] [BoundedSMul S R] [BoundedSMul S M] [Module R M] [BoundedSMul R M] [Module 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] [BoundedSMul R M] [Module 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 = 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 = 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 = 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 ⋯