instContinuousSMulComplexSubtypeAEEqFunVolumeMemAddSubgroupLp

English

There is a natural continuous complex scalar action on the Lp space of functions on UnitAddTorus: ℂ acts continuously on Lp(ℂ, p, volume).

Русский

Существует естественное непрерывное действие комплексного множителя на пространство Lp функций на UnitAddTorus: ℂ действует непрерывно на Lp(ℂ, p, volume).

LaTeX

$$$ \text{ContinuousSMul } \mathbb{C} \left( L^p(\mathbb{C}, p, \mathrm{volume}) \right) $$$

Lean4

instance {p : ℝ≥0∞} [Fact (1 ≤ p)] : ContinuousSMul ℂ (Lp ℂ p (volume : Measure (UnitAddTorus d))) :=
  inferInstance

Похожие утверждения