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_expTrivSqZeroExt.snd_expTrivSqZeroExt.exp_inlTrivSqZeroExt.exp_inr- The $ℓ^1$ norm on
TrivSqZeroExt:TrivSqZeroExt.instL1SeminormedAddCommGroupTrivSqZeroExt.instL1SeminormedRingTrivSqZeroExt.instL1SeminormedCommRingTrivSqZeroExt.instL1IsBoundedSMulTrivSqZeroExt.instL1NormedAddCommGroupTrivSqZeroExt.instL1NormedRingTrivSqZeroExt.instL1NormedCommRingTrivSqZeroExt.instL1NormedSpaceTrivSqZeroExt.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]
[IsTopologicalRing R]
[IsTopologicalAddGroup 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]
[IsTopologicalRing R]
[IsTopologicalAddGroup 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]
[IsTopologicalRing R]
[IsTopologicalAddGroup 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]
[IsTopologicalRing R]
[IsTopologicalAddGroup 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) (inl e + 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
{R : Type u_3}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[Module Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M]
[TopologicalSpace R]
[TopologicalSpace M]
[IsTopologicalRing R]
[IsTopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[Algebra ℚ R]
[Module ℚ M]
[T2Space R]
[T2Space M]
(x : TrivSqZeroExt R M)
(hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd)
:
@[simp]
theorem
TrivSqZeroExt.exp_inl
{R : Type u_3}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[Module Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M]
[TopologicalSpace R]
[TopologicalSpace M]
[IsTopologicalRing R]
[IsTopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[Algebra ℚ R]
[Module ℚ M]
[T2Space R]
[T2Space M]
(x : R)
:
@[simp]
theorem
TrivSqZeroExt.exp_inr
{R : Type u_3}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
[Module Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M]
[TopologicalSpace R]
[TopologicalSpace M]
[IsTopologicalRing R]
[IsTopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[Algebra ℚ R]
[Module ℚ M]
[T2Space R]
[T2Space M]
(m : M)
:
theorem
TrivSqZeroExt.exp_def
{R : Type u_3}
{M : Type u_4}
[CommRing R]
[AddCommGroup M]
[Algebra ℚ R]
[Module ℚ M]
[Module R M]
[Module Rᵐᵒᵖ M]
[IsCentralScalar R M]
[TopologicalSpace R]
[TopologicalSpace M]
[IsTopologicalRing R]
[IsTopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[T2Space R]
[T2Space M]
(x : TrivSqZeroExt R M)
:
@[simp]
theorem
TrivSqZeroExt.fst_exp
{R : Type u_3}
{M : Type u_4}
[CommRing R]
[AddCommGroup M]
[Algebra ℚ R]
[Module ℚ M]
[Module R M]
[Module Rᵐᵒᵖ M]
[IsCentralScalar R M]
[TopologicalSpace R]
[TopologicalSpace M]
[IsTopologicalRing R]
[IsTopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[T2Space R]
[T2Space M]
(x : TrivSqZeroExt R M)
:
@[simp]
theorem
TrivSqZeroExt.snd_exp
{R : Type u_3}
{M : Type u_4}
[CommRing R]
[AddCommGroup M]
[Algebra ℚ R]
[Module ℚ M]
[Module R M]
[Module Rᵐᵒᵖ M]
[IsCentralScalar R M]
[TopologicalSpace R]
[TopologicalSpace M]
[IsTopologicalRing R]
[IsTopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[T2Space R]
[T2Space M]
(x : TrivSqZeroExt R M)
:
theorem
TrivSqZeroExt.eq_smul_exp_of_invertible
{R : Type u_3}
{M : Type u_4}
[CommRing R]
[AddCommGroup M]
[Algebra ℚ R]
[Module ℚ M]
[Module R M]
[Module Rᵐᵒᵖ M]
[IsCentralScalar R M]
[TopologicalSpace R]
[TopologicalSpace M]
[IsTopologicalRing R]
[IsTopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[T2Space R]
[T2Space M]
(x : TrivSqZeroExt R M)
[Invertible x.fst]
:
Polar form of trivial-square-zero extension.
theorem
TrivSqZeroExt.eq_smul_exp_of_ne_zero
{R : Type u_3}
{M : Type u_4}
[Field R]
[AddCommGroup M]
[Algebra ℚ R]
[Module ℚ M]
[Module R M]
[Module Rᵐᵒᵖ M]
[IsCentralScalar R M]
[TopologicalSpace R]
[TopologicalSpace M]
[IsTopologicalRing R]
[IsTopologicalAddGroup M]
[ContinuousSMul R M]
[ContinuousSMul Rᵐᵒᵖ M]
[T2Space R]
[T2Space M]
(x : TrivSqZeroExt R M)
(hx : x.fst ≠ 0)
:
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]
:
theorem
TrivSqZeroExt.norm_def
{R : Type u_3}
{M : Type u_4}
[SeminormedRing R]
[SeminormedAddCommGroup M]
(x : TrivSqZeroExt R M)
:
theorem
TrivSqZeroExt.nnnorm_def
{R : Type u_3}
{M : Type u_4}
[SeminormedRing R]
[SeminormedAddCommGroup M]
(x : TrivSqZeroExt R M)
:
@[simp]
theorem
TrivSqZeroExt.norm_inl
{R : Type u_3}
{M : Type u_4}
[SeminormedRing R]
[SeminormedAddCommGroup M]
(r : R)
:
@[simp]
theorem
TrivSqZeroExt.norm_inr
{R : Type u_3}
{M : Type u_4}
[SeminormedRing R]
[SeminormedAddCommGroup M]
(m : M)
:
@[simp]
theorem
TrivSqZeroExt.nnnorm_inl
{R : Type u_3}
{M : Type u_4}
[SeminormedRing R]
[SeminormedAddCommGroup M]
(r : R)
:
@[simp]
theorem
TrivSqZeroExt.nnnorm_inr
{R : Type u_3}
{M : Type u_4}
[SeminormedRing R]
[SeminormedAddCommGroup M]
(m : M)
:
instance
TrivSqZeroExt.instL1SeminormedRing
{R : Type u_3}
{M : Type u_4}
[SeminormedRing R]
[SeminormedAddCommGroup M]
[Module R M]
[IsBoundedSMul R M]
[Module Rᵐᵒᵖ M]
[IsBoundedSMul Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M]
:
SeminormedRing (TrivSqZeroExt R M)
Equations
- One or more equations did not get rendered due to their size.
instance
TrivSqZeroExt.instL1IsBoundedSMul
{S : Type u_2}
{R : Type u_3}
{M : Type u_4}
[SeminormedCommRing S]
[SeminormedRing R]
[SeminormedAddCommGroup M]
[Algebra S R]
[Module S M]
[IsBoundedSMul S R]
[IsBoundedSMul S M]
[Module R M]
[IsBoundedSMul R M]
[Module Rᵐᵒᵖ M]
[IsBoundedSMul Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M]
:
IsBoundedSMul S (TrivSqZeroExt R M)
instance
TrivSqZeroExt.instNormOneClass
{R : Type u_3}
{M : Type u_4}
[SeminormedRing R]
[SeminormedAddCommGroup M]
[Module R M]
[IsBoundedSMul R M]
[Module Rᵐᵒᵖ M]
[IsBoundedSMul Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M]
[NormOneClass R]
:
NormOneClass (TrivSqZeroExt R M)
instance
TrivSqZeroExt.instL1SeminormedCommRing
{R : Type u_3}
{M : Type u_4}
[SeminormedCommRing R]
[SeminormedAddCommGroup M]
[Module R M]
[Module Rᵐᵒᵖ M]
[IsCentralScalar R M]
[IsBoundedSMul R M]
:
Equations
- One or more equations did not get rendered due to their size.
instance
TrivSqZeroExt.instL1NormedAddCommGroup
{R : Type u_3}
{M : Type u_4}
[NormedRing R]
[NormedAddCommGroup M]
:
instance
TrivSqZeroExt.instL1NormedRing
{R : Type u_3}
{M : Type u_4}
[NormedRing R]
[NormedAddCommGroup M]
[Module R M]
[Module Rᵐᵒᵖ M]
[IsBoundedSMul R M]
[IsBoundedSMul Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M]
:
NormedRing (TrivSqZeroExt R M)
Equations
- One or more equations did not get rendered due to their size.
instance
TrivSqZeroExt.instL1NormedCommRing
{R : Type u_3}
{M : Type u_4}
[NormedCommRing R]
[NormedAddCommGroup M]
[Module R M]
[Module Rᵐᵒᵖ M]
[IsCentralScalar R M]
[IsBoundedSMul R M]
:
NormedCommRing (TrivSqZeroExt R M)
Equations
- One or more equations did not get rendered due to their size.
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)
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]
[IsBoundedSMul R M]
[IsBoundedSMul Rᵐᵒᵖ M]
[SMulCommClass R Rᵐᵒᵖ M]
[IsScalarTower 𝕜 R M]
[IsScalarTower 𝕜 Rᵐᵒᵖ M]
:
NormedAlgebra 𝕜 (TrivSqZeroExt R M)
Equations
- TrivSqZeroExt.instL1NormedAlgebra 𝕜 = { toAlgebra := TrivSqZeroExt.algebra' 𝕜 R M, norm_smul_le := ⋯ }