eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul'

English

Under a pointwise bound by c, the ess sup-based Lp norm is controlled by c times the ess sup-based Lp norm of the other function.

Русский

При точном по точкам ограничении на c ess sup-норма по Lp не превысит c-умноженную ess sup-норму другого функции.

LaTeX

$$$\text{If } \forall x, \|f(x)\| ≤ c \|g(x)\|, \; eLpNormEssSup(f,μ) ≤ c \cdot eLpNormEssSup(g,μ)$$$

Lean4

theorem eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' {f : α → ε} {g : α → ε'} {c : ℝ≥0∞}
    (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ) : eLpNormEssSup f μ ≤ c • eLpNormEssSup g μ :=
  calc
    essSup (‖f ·‖ₑ) μ ≤ essSup (c * ‖g ·‖ₑ) μ := essSup_mono_ae <| h
    _ = c • essSup (‖g ·‖ₑ) μ := ENNReal.essSup_const_mul

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