div_const

Mathlib.MeasureTheory.Function.L1Space.Integrable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Integrable.div_const

← MathLib Explorer

English

If f ∈ Lp and g ∈ Lq with HolderTriple, then f g ∈ L1.

Русский

Если f ∈ Lp и g ∈ Lq с HolderTriple, то f g ∈ L1.

LaTeX

$$$\mathrm{MemLp}(f,p,\mu) \rightarrow \mathrm{MemLp}(g,q,\mu) \rightarrow \big[ p.HolderTriple q 1 \big] \Rightarrow \mathrm{Integrable}(f \cdot g,\mu).$$$

Lean4

@[fun_prop]
theorem div_const {f : α → 𝕜} (h : Integrable f μ) (c : 𝕜) : Integrable (fun x => f x / c) μ := by
  simp_rw [div_eq_mul_inv, h.mul_const]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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