eLpNorm_conj

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.eLpNorm_conj

English

Conjugation does not change the eLpNorm: eLpNorm(conj f) = eLpNorm(f).

Русский

Сложение сопряжения функции не меняет норму Lp: eLpNorm(conj f) = eLpNorm(f).

LaTeX

$$$$eLpNorm(conj f)_{p} = eLpNorm(f)_{p}.$$$$

Lean4

@[simp]
theorem eLpNorm_conj (f : α → 𝕜) (p : ℝ≥0∞) (μ : Measure α) : eLpNorm (conj f) p μ = eLpNorm f p μ := by
  simp [← eLpNorm_norm]

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

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

Разделы

Аффилиация

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