L∞ as a normed algebra and a C⋆-algebra #
For a normed ring R, the space L∞(μ, R) = Lp R ∞ μ of essentially bounded classes is a normed
ring under pointwise multiplication, on an arbitrary measure space. The product is Mathlib's
Hölder product f • g at the exponents ∞, ∞, ∞, and the unit is the class of the constant
function one. It is commutative when R is, a normed algebra over 𝕜 when R is, and a star
ring with the pointwise involution when R is a normed star ring. When R is a C⋆-ring, so is
L∞(μ, R): the essential supremum of ‖f‖ ^ 2 is the square of the essential supremum of ‖f‖.
Consequently L∞(μ, A) is a (commutative) C⋆-algebra whenever A is. In particular
Lp ℂ ∞ μ is a commutative C⋆-algebra, so Mathlib's Gelfand duality
gelfandStarTransform (Lp ℂ ∞ μ) identifies it isometrically, as a C⋆-algebra, with the
continuous functions on its character space. When μ ≠ 0, L∞(μ, R) is nontrivial if R is,
and its unit has norm one if that of R does.
The instances follow Mathlib's corresponding instances on the space lp B ∞ of bounded families
(lp.inftyNormedRing, lp.inftyNormedAlgebra, lp.inftyStarRing, lp.inftyCStarRing), with
almost everywhere equalities in place of pointwise ones.
Main declarations #
MeasureTheory.Lp.smul_eq_mul: the product is the Hölder product at exponents∞, ∞, ∞.MeasureTheory.Lp.coeFn_mul: the product is pointwise almost everywhere.MeasureTheory.Lp.coeFn_algebraMap: scalars act as almost everywhere constant classes.- The instances
NormedRing,NormedCommRing,NormedAlgebra,StarRing,CStarRing,CStarAlgebraandCommCStarAlgebraonLp R ∞ μ.
Pointwise multiplication on L∞(μ, R), given by the Hölder product at exponents
∞, ∞, ∞.
The product on L∞ is Mathlib's Hölder product at exponents ∞, ∞, ∞.
The scalar embedding into L∞ is the class of the corresponding constant function.
L∞(μ, R) satisfies the C⋆-identity ‖star f * f‖ = ‖f‖ * ‖f‖ when R does.