essSup_mul_le — Mathlib

English

For any f, g: α → ℝ≥0∞, the essential supremum of the product is at most the product of the essential supremums: essSup (f · g) ≤ essSup f · essSup g.

Русский

Для любых f, g: α → ℝ≥0∞ выполняется essSup (f · g) ≤ essSup f · essSup g.

LaTeX

$$$$ \operatorname{ess\,sup}_{x} (f(x) \cdot g(x)) \le \operatorname{ess\,sup}_{x} f(x) \cdot \operatorname{ess\,sup}_{x} g(x). $$$$

Lean4

theorem essSup_mul_le (f g : α → ℝ≥0∞) : essSup (f * g) μ ≤ essSup f μ * essSup g μ :=
  limsup_mul_le f g

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