Theorems · Theorem · measure theory

MeasureTheory.lpNorm_const

∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E],
  p ≠ 0 → μ ≠ 0 → ∀ (c : E), MeasureTheory.lpNorm (fun _x => c) p μ = ‖c‖ * μ.real Set.univ ^ p.toReal⁻¹

Defined in

Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm

Cited by

1 results in Mathlib

Foundations

Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup