The star operation on Lp #
Mathlib equips Lp R p μ with the pointwise involution star when R is a normed star group.
This file records that this involution is additive, isometric and, over a star module,
conjugate-linear. Thus Lp R p μ is a star additive monoid and a star module for every exponent
p, and a normed star group for 1 ≤ p. Over ℂ the involution is pointwise complex
conjugation of classes of functions; these laws are part of the C⋆-algebra structure of L∞.
@[instance_reducible]
noncomputable instance
MeasureTheory.Lp.instStarAddMonoid
{α : Type u_1}
{R : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
:
StarAddMonoid ↥(Lp R p μ)
instance
MeasureTheory.Lp.instNormedStarGroup
{α : Type u_1}
{R : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
[Fact (1 ≤ p)]
:
NormedStarGroup ↥(Lp R p μ)
instance
MeasureTheory.Lp.instStarModule
{α : Type u_1}
{R : Type u_2}
{𝕜 : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
{p : ENNReal}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
[NormedRing 𝕜]
[Star 𝕜]
[Module 𝕜 R]
[IsBoundedSMul 𝕜 R]
[StarModule 𝕜 R]
:
StarModule 𝕜 ↥(Lp R p μ)