mathlib3

632fef37 - feat(analysis/normed_space/M_structure): Define L-projections, show they form a Boolean algebra (#12173)

feat(analysis/normed_space/M_structure): Define L-projections, show they form a Boolean algebra (#12173) A continuous projection P on a normed space X is said to be an L-projection if, for all `x` in `X`, ``` ∥x∥ = ∥P x∥ + ∥(1-P) x∥. ``` The range of an L-projection is said to be an L-summand of X. A continuous 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 range of an M-projection is said to be an M-summand of X. The L-projections and M-projections form Boolean algebras. 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 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`. This initial PR limits itself to showing that the L-projections form a Boolean algebra. The approach followed is based on that used in `measure_theory.measurable_space`. The equivalent result for M-projections can be established by a similar argument or by a duality result (to be established). However, I thought it best to seek feedback before proceeding further. Co-authored-by: Christopher Hoskin <mans0954@users.noreply.github.com>