of_bilin — Mathlib

English

If f ∈ MemLp q μ and g ∈ MemLp p μ, then the bilinear combination φ • f has MemLp with exponent r under Holder triple.

Русский

Если f ∈ MemLp q μ и g ∈ MemLp p μ, то билинейное сочетание φ•f принадлежит MemLp r μ.

LaTeX

$$$MemLp (φ \\cdot f) r μ ≤ c \\cdot MemLp f p μ \\cdot MemLp g q μ$ under HolderTriple$$

Lean4

theorem of_bilin {p q r : ℝ≥0∞} {f : α → E} {g : α → F} (b : E → F → G) (c : ℝ≥0) (hf : MemLp f p μ) (hg : MemLp g q μ)
    (h : AEStronglyMeasurable (fun x ↦ b (f x) (g x)) μ) (hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
    [hpqr : HolderTriple p q r] : MemLp (fun x ↦ b (f x) (g x)) r μ :=
  by
  refine ⟨h, ?_⟩
  apply (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm hf.1 hg.1 b c hb (hpqr := hpqr)).trans_lt
  have := hf.2
  have := hg.2
  finiteness

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