eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'

English

If a.e. bound uses c ∈ ℝ≥0, then eLpNorm f p μ ≤ c · eLpNorm g p μ.

Русский

Если почти везде выполняется неравенство с c ∈ ℝ≥0, то eLpNorm f p μ ≤ c · eLpNorm g p μ.

LaTeX

$$$\text{ae bound: } \|f(x)\| ≤ c \|g(x)\| \text{ with } c ∈ ℝ_{≥0} \Rightarrow eLpNorm f p μ ≤ c \cdot eLpNorm g p μ$$$

Lean4

theorem eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul' {f : α → ε} {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)

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