eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul

English

If |f| ≤ c|g| a.e., then eLpNorm f p μ ≤ c · eLpNorm g p μ for any p > 0 (in NNReal or ENNReal sense).

Русский

Если |f| ≤ c|g| почти всюду, то eLpNorm f p μ ≤ c·eLpNorm g p μ для любого p>0.

LaTeX

$$$\forall a.e. \|f\| ≤ c \|g\| \Rightarrow eLpNorm f p μ ≤ c \, eLpNorm g p μ\quad( p>0 )$$$

Lean4

theorem eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul {f : α → F} {g : α → G} {c : ℝ≥0} (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
    (p : ℝ≥0∞) : eLpNorm f p μ ≤ c • eLpNorm g p μ :=
  by
  by_cases h0 : p = 0
  · simp [h0]
  by_cases h_top : p = ∞
  · rw [h_top]
    exact eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul h
  simp_rw [eLpNorm_eq_eLpNorm' h0 h_top]
  exact
    eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul h
      (ENNReal.toReal_pos h0 h_top)
        -- TODO: add the whole family of lemmas?

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