mathlib3 documentation

analysis.normed_space.M_structure

M-structure #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A projection P on a normed space X is said to be an L-projection (is_Lprojection) if, for all x in X, $\|x\| = \|P x\| + \|(1 - P) x\|$.

A projection P on a normed space X is said to be an M-projection if, for all x in X, $\|x\| = max(\|P x\|,\|(1 - P) x\|)$.

The L-projections on X form a Boolean algebra (is_Lprojection.subtype.boolean_algebra).

TODO (Motivational background) #

The M-projections on a normed space form a Boolean algebra.

The range of an L-projection on a normed space X is said to be an L-summand of X. The range of an M-projection is said to be an M-summand of X.

When X is a Banach space, the Boolean algebra of L-projections is complete. Let X be a normed space with dual X^*. A closed subspace M of X is said to be an M-ideal if the topological annihilator M^∘ is an L-summand of X^*.

M-ideal, M-summands and L-summands were introduced by Alfsen and Effros in [AE72] to study the structure of general Banach spaces. When A is a JB*-triple, the M-ideals of A are exactly the norm-closed ideals of A. When A is a JBW*-triple with predual X, the M-summands of A are exactly the weak*-closed ideals, and their pre-duals can be identified with the L-summands of X. In the special case when A is a C*-algebra, the M-ideals are exactly the norm-closed two-sided ideals of A, when A is also a W*-algebra the M-summands are exactly the weak*-closed two-sided ideals of A.

Implementation notes #

The approach to showing that the L-projections form a Boolean algebra is inspired by measure_theory.measurable_space.

Instead of using P : X →L[𝕜] X to represent projections, we use an arbitrary ring M with a faithful action on X. continuous_linear_map.apply_module can be used to recover the X →L[𝕜] X special case.

References #

Tags #

M-summand, M-projection, L-summand, L-projection, M-ideal, M-structure

structure is_Lprojection (X : Type u_1) [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] (P : M) :

Prop

proj : is_idempotent_elem P
Lnorm : ∀ (x : X), ‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖

A projection on a normed space X is said to be an L-projection if, for all x in X, $\|x\| = \|P x\| + \|(1 - P) x\|$.

Note that we write P • x instead of P x for reasons described in the module docstring.

structure is_Mprojection (X : Type u_1) [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] (P : M) :

Prop

proj : is_idempotent_elem P
Mnorm : ∀ (x : X), ‖x‖ = linear_order.max ‖P • x‖ ‖(1 - P) • x‖

A projection on a normed space X is said to be an M-projection if, for all x in X, $\|x\| = max(\|P x\|,\|(1 - P) x\|)$.

Note that we write P • x instead of P x for reasons described in the module docstring.

theorem is_Lprojection.Lcomplement {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] {P : M} (h : is_Lprojection X P) :

is_Lprojection X (1 - P)

theorem is_Lprojection.Lcomplement_iff {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] (P : M) :

is_Lprojection X P ↔ is_Lprojection X (1 - P)

theorem is_Lprojection.commute {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :

theorem is_Lprojection.mul {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :

is_Lprojection X (P * Q)

theorem is_Lprojection.join {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] {P Q : M} (h₁ : is_Lprojection X P) (h₂ : is_Lprojection X Q) :

is_Lprojection X (P + Q - P * Q)

@[protected, instance]

def is_Lprojection.subtype.has_compl {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] :

has_compl {f // is_Lprojection X f}

Equations

is_Lprojection.subtype.has_compl = {compl := λ (P : {f // is_Lprojection X f}), ⟨1 - ↑P, _⟩}

@[simp]

theorem is_Lprojection.coe_compl {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] (P : {P // is_Lprojection X P}) :

↑Pᶜ = 1 - ↑P

@[protected, instance]

def is_Lprojection.subtype.has_inf {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

has_inf {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.has_inf = {inf := λ (P Q : {P // is_Lprojection X P}), ⟨↑P * ↑Q, _⟩}

@[simp]

theorem is_Lprojection.coe_inf {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] (P Q : {P // is_Lprojection X P}) :

↑(P ⊓ Q) = ↑P * ↑Q

@[protected, instance]

def is_Lprojection.subtype.has_sup {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

has_sup {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.has_sup = {sup := λ (P Q : {P // is_Lprojection X P}), ⟨↑P + ↑Q - ↑P * ↑Q, _⟩}

@[simp]

theorem is_Lprojection.coe_sup {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] (P Q : {P // is_Lprojection X P}) :

↑(P ⊔ Q) = ↑P + ↑Q - ↑P * ↑Q

@[protected, instance]

def is_Lprojection.subtype.has_sdiff {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

has_sdiff {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.has_sdiff = {sdiff := λ (P Q : {P // is_Lprojection X P}), ⟨↑P * (1 - ↑Q), _⟩}

@[simp]

theorem is_Lprojection.coe_sdiff {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] (P Q : {P // is_Lprojection X P}) :

↑(P \ Q) = ↑P * (1 - ↑Q)

@[protected, instance]

def is_Lprojection.subtype.partial_order {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

partial_order {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.partial_order = {le := λ (P Q : {P // is_Lprojection X P}), ↑P = ↑(P ⊓ Q), lt := preorder.lt._default (λ (P Q : {P // is_Lprojection X P}), ↑P = ↑(P ⊓ Q)), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

theorem is_Lprojection.le_def {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] (P Q : {P // is_Lprojection X P}) :

P ≤ Q ↔ ↑P = ↑(P ⊓ Q)

@[protected, instance]

def is_Lprojection.subtype.has_zero {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] :

has_zero {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.has_zero = {zero := ⟨0, _⟩}

@[simp]

theorem is_Lprojection.coe_zero {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] :

↑0 = 0

@[protected, instance]

def is_Lprojection.subtype.has_one {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] :

has_one {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.has_one = {one := ⟨1, _⟩}

@[simp]

theorem is_Lprojection.coe_one {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] :

↑1 = 1

@[protected, instance]

def is_Lprojection.subtype.bounded_order {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

bounded_order {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.bounded_order = {top := 1, le_top := _, bot := 0, bot_le := _}

@[simp]

theorem is_Lprojection.coe_bot {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

↑bounded_order.bot = 0

@[simp]

theorem is_Lprojection.coe_top {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

↑bounded_order.top = 1

theorem is_Lprojection.compl_mul {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] {P : {P // is_Lprojection X P}} {Q : M} :

↑Pᶜ * Q = Q - ↑P * Q

theorem is_Lprojection.mul_compl_self {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] {P : {P // is_Lprojection X P}} :

↑P * ↑Pᶜ = 0

theorem is_Lprojection.distrib_lattice_lemma {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] {P Q R : {P // is_Lprojection X P}} :

(↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ

@[protected, instance]

def is_Lprojection.subtype.distrib_lattice {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

distrib_lattice {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.distrib_lattice = {sup := has_sup.sup is_Lprojection.subtype.has_sup, le := partial_order.le is_Lprojection.subtype.partial_order, lt := partial_order.lt is_Lprojection.subtype.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := has_inf.inf is_Lprojection.subtype.has_inf, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _}

@[protected, instance]

def is_Lprojection.subtype.boolean_algebra {X : Type u_1} [normed_add_comm_group X] {M : Type u_2} [ring M] [module M X] [has_faithful_smul M X] :

boolean_algebra {P // is_Lprojection X P}

Equations

is_Lprojection.subtype.boolean_algebra = {sup := distrib_lattice.sup is_Lprojection.subtype.distrib_lattice, le := distrib_lattice.le is_Lprojection.subtype.distrib_lattice, lt := distrib_lattice.lt is_Lprojection.subtype.distrib_lattice, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := distrib_lattice.inf is_Lprojection.subtype.distrib_lattice, inf_le_left := _, inf_le_right := _, le_inf := _, le_sup_inf := _, compl := has_compl.compl is_Lprojection.subtype.has_compl, sdiff := has_sdiff.sdiff is_Lprojection.subtype.has_sdiff, himp := λ (x y : {P // is_Lprojection X P}), distrib_lattice.sup y xᶜ, top := bounded_order.top is_Lprojection.subtype.bounded_order, bot := bounded_order.bot is_Lprojection.subtype.bounded_order, inf_compl_le_bot := _, top_le_sup_compl := _, le_top := _, bot_le := _, sdiff_eq := _, himp_eq := _}