English
Let E be a normed module over two normed rings 𝕜 and 𝕜' with a compatible scalar-tower structure; then the Lp space of E-valued functions is itself a module over 𝕜 and 𝕜' in a way that respects the tower: for all k in 𝕜, k' in 𝕜', and f in Lp(E,p,μ), (k · k') · f = k · (k' · f).
Русский
Пусть E — нормированная модуль над двумерной структурой скаляров 𝕜 и 𝕜' с совместимой структурой каскада скаляров; тогда пространство Lp функций с значениями в E тоже является модулем над 𝕜 и 𝕜' так, что выполняется тождество (k · k') · f = k · (k' · f) для любых k ∈ 𝕜, k' ∈ 𝕜' и f ∈ Lp(E,p,μ).
LaTeX
$$$IsScalarTower\ 𝕜\ 𝕜'\ (Lp\ E\ p\ μ)$$$
Lean4
instance instIsScalarTower [SMul 𝕜 𝕜'] [IsScalarTower 𝕜 𝕜' E] : IsScalarTower 𝕜 𝕜' (Lp E p μ) where
smul_assoc k k' f := Subtype.ext <| smul_assoc k k' (f : α →ₘ[μ] E)
