constₗ — Mathlib

English

The operator Lp.const viewed as a linear map E → Lp(E, p, μ) is the canonical linear map sending c to indicatorConstLp(p, hs, hμs, c).

Русский

Оператор Lp.const как линейное отображение E → Lp(I), переводит c в indicatorConstLp(p, hs, hμs, c).

LaTeX

$$Lp.constₗ p μ c is the linear map to Lp E p μ given by indicatorConstLp(p, hs, hμs, c).$$

Lean4

/-- `MeasureTheory.Lp.const` as a `LinearMap`. -/
@[simps]
protected def constₗ (𝕜 : Type*) [NormedRing 𝕜] [Module 𝕜 E] [IsBoundedSMul 𝕜 E] : E →ₗ[𝕜] Lp E p μ
    where
  toFun := Lp.const p μ
  map_add' := map_add _
  map_smul' _ _ := rfl

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