English
Hölder-type inequality at the top exponent: eLpNorm_top ≤ product of top-norms with a bilinear bound.
Русский
Холдерова неравенство в верхних степенях: eLpNorm_top ≤ произведение топ-норм.
LaTeX
$$$eLpNorm_le_eLpNorm_top_mul_eLpNorm f g μ ≤ c \\cdot eLpNorm f ∞ μ \\cdot eLpNorm g p μ$ under HolderTriple$$
Lean4
/-- Hölder's inequality, as an inequality on the `ℒp` seminorm of an elementwise operation
`fun x => b (f x) (g x)`. -/
theorem eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm {p q r : ℝ≥0∞} (hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ) (b : E → F → G) (c : ℝ≥0) (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
[hpqr : HolderTriple p q r] : eLpNorm (fun x => b (f x) (g x)) r μ ≤ c * eLpNorm f p μ * eLpNorm g q μ :=
by
have hpqr := hpqr.one_div_eq
obtain (rfl | rfl | hp) := ENNReal.trichotomy p
· simp_all
· have : r = q := by simpa using hpqr
exact this ▸ eLpNorm_le_eLpNorm_top_mul_eLpNorm r f hg b c h
obtain (rfl | rfl | hq) := ENNReal.trichotomy q
· simp_all
· have : r = p := by simpa using hpqr
exact this ▸ eLpNorm_le_eLpNorm_mul_eLpNorm_top p hf g b c h
obtain ⟨hp₁, hp₂⟩ := ENNReal.toReal_pos_iff.mp hp
obtain ⟨hq₁, hq₂⟩ := ENNReal.toReal_pos_iff.mp hq
have hpqr' : 1 / r.toReal = 1 / p.toReal + 1 / q.toReal :=
by
have := congr(ENNReal.toReal $(hpqr))
rw [ENNReal.toReal_add (by simpa using hp₁.ne') (by simpa using hq₁.ne')] at this
simpa
have hr : 0 < r.toReal := one_div_pos.mp <| by rw [hpqr']; positivity
obtain ⟨hr₁, hr₂⟩ := ENNReal.toReal_pos_iff.mp hr
have hrp : r.toReal < p.toReal := lt_of_one_div_lt_one_div hp <| hpqr' ▸ lt_add_of_pos_right _ (by positivity)
rw [eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm', eLpNorm_eq_eLpNorm']
· exact eLpNorm'_le_eLpNorm'_mul_eLpNorm' hf hg b c h hr hrp hpqr'
all_goals
first
| positivity
| finiteness
