English
Hölder-type inequality for the operator b(f,g) with a constant c: the eLpNorm of b(f,g) is bounded by c times the product of eLpNorms of f and g with appropriate exponents.
Русский
Неравенство Холдера для оператора b(f,g) относится к норме eLpNorm и ограничивает её произведением норм f и g.
LaTeX
$$$eLpNorm (b(f,g)) r μ ≤ c \\, eLpNorm f p μ \\cdot eLpNorm g q μ$ при подходящих p,q,r и условиях HolderTriple$$
Lean4
theorem eLpNorm_le_eLpNorm_mul_eLpNorm_top (p : ℝ≥0∞) {f : α → E} (hf : AEStronglyMeasurable f μ) (g : α → F)
(b : E → F → G) (c : ℝ≥0) (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) :
eLpNorm (fun x => b (f x) (g x)) p μ ≤ c * eLpNorm f p μ * eLpNorm g ∞ μ :=
calc
eLpNorm (fun x ↦ b (f x) (g x)) p μ ≤ c * eLpNorm g ∞ μ * eLpNorm f p μ :=
eLpNorm_le_eLpNorm_top_mul_eLpNorm p g hf (flip b) c <|
by
convert h using 3 with x
simp only [mul_assoc, mul_comm ‖f x‖₊]
_ = c * eLpNorm f p μ * eLpNorm g ∞ μ := by simp only [mul_assoc]; rw [mul_comm (eLpNorm _ _ _)]
