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 #

@[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)
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] :

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) :

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 #

Equations
Equations
Equations
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