English
For p, q, r with HolderTriple, and suitable AEStronglyMeasurable f and g, the Lp-norm of the bilinear form is controlled by the product of the Lp-norms of f and g.
Русский
Для достаточного набора p, q, r и соответствующих условий, норма Lp слева контролируется произведением норм f и g.
LaTeX
$$$eLpNorm' (f) r μ ≤ eLpNorm' f p μ · eLpNorm' g q μ$ под условия HolderTriple и AEStronglyMeasurable$$
Lean4
theorem eLpNorm_le_eLpNorm_top_mul_eLpNorm (p : ℝ≥0∞) (f : α → E) {g : α → F} (hg : AEStronglyMeasurable g μ)
(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 ∞ μ * eLpNorm g p μ :=
by
calc
eLpNorm (fun x => b (f x) (g x)) p μ ≤ eLpNorm (fun x => (c : ℝ) • ‖f x‖ * ‖g x‖) p μ := eLpNorm_mono_ae_real h
_ ≤ c * eLpNorm f ∞ μ * eLpNorm g p μ := ?_
simp only [smul_mul_assoc, ← Pi.smul_def, eLpNorm_const_smul]
rw [Real.enorm_eq_ofReal c.coe_nonneg, ENNReal.ofReal_coe_nnreal, mul_assoc]
gcongr
obtain (rfl | rfl | hp) := ENNReal.trichotomy p
· simp
· rw [← eLpNorm_norm f, ← eLpNorm_norm g]
simp_rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm, enorm_mul, enorm_norm]
exact ENNReal.essSup_mul_le (‖f ·‖ₑ) (‖g ·‖ₑ)
obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
simp_rw [eLpNorm_eq_lintegral_rpow_enorm hp₁.ne' hp₂.ne, eLpNorm_exponent_top, eLpNormEssSup, one_div,
ENNReal.rpow_inv_le_iff hp, enorm_mul, enorm_norm]
rw [ENNReal.mul_rpow_of_nonneg (hz := hp.le), ENNReal.rpow_inv_rpow hp.ne', ← lintegral_const_mul'' _ (by fun_prop)]
simp only [← ENNReal.mul_rpow_of_nonneg (hz := hp.le)]
apply lintegral_mono_ae
filter_upwards [h, enorm_ae_le_eLpNormEssSup f μ] with x hb hf
refine ENNReal.rpow_le_rpow ?_ hp.le
gcongr
exact hf
