eLpNorm'_measure_zero_of_exponent_zero

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero

English

When the exponent is zero, the eLpNorm' of any function with respect to the zero measure equals 1.

Русский

Если показатель степени равен нулю, то eLpNorm' любой функции по нулевой мере равен 1.

LaTeX

$$$eLpNorm'(f, 0, 0) = 1$$$

Lean4

theorem eLpNorm'_measure_zero_of_exponent_zero {f : α → ε} : eLpNorm' f 0 (0 : Measure α) = 1 := by simp [eLpNorm']

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru