norm_le_mul_norm_of_ae_le_mul — Mathlib

English

If almost everywhere ‖f x‖ ≤ c · ‖g x‖, then ‖f‖ ≤ c · ‖g‖.

Русский

Если почти всюду выполняется ‖f(x)‖ ≤ c · ‖g(x)‖, то ‖f‖ ≤ c · ‖g‖.

LaTeX

$$$\forall c \in \mathbb{R}_{+},\ (\forall^{\mathrm{ae}} x, \|f(x)\| ≤ c\|g(x)\|) \Rightarrow \|f\| ≤ c\|g\|.$$$

Lean4

theorem norm_le_mul_norm_of_ae_le_mul {c : ℝ} {f : Lp E p μ} {g : Lp F p μ} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ c * ‖g x‖) :
    ‖f‖ ≤ c * ‖g‖ := by
  rcases le_or_gt 0 c with hc | hc
  · lift c to ℝ≥0 using hc
    exact NNReal.coe_le_coe.mpr (nnnorm_le_mul_nnnorm_of_ae_le_mul h)
  · simp only [norm_def]
    have := eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg h hc p
    simp [this]

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