English
For p with finite nonzero, and for s measurable, the eLpNorm of s.indicator of (f−g) is bounded by c times μ(s)^{1/p} provided the pointwise distance is bounded by c on s.
Русский
Для p конечного и не нуля, для измеримого s, eLpNorm( s.indicator(f−g) ) ≤ c · μ(s)^{1/p} при условии, что расстояние между f и g на s ограничено c.
LaTeX
$$$ eLpNorm (s.indicator (f-g)) p μ ≤ c · μ(s)^{1/p}$ при $dist(f,g) ≤ c$ на s$$
Lean4
theorem eLpNorm_sub_le_of_dist_bdd (μ : Measure α) {p : ℝ≥0∞} (hp' : p ≠ ∞) {s : Set α} (hs : MeasurableSet[m] s)
{f g : α → β} {c : ℝ} (hc : 0 ≤ c) (hf : ∀ x ∈ s, dist (f x) (g x) ≤ c) :
eLpNorm (s.indicator (f - g)) p μ ≤ ENNReal.ofReal c * μ s ^ (1 / p.toReal) :=
by
by_cases hp : p = 0
· simp [hp]
have : ∀ x, ‖s.indicator (f - g) x‖ ≤ ‖s.indicator (fun _ => c) x‖ :=
by
intro x
by_cases hx : x ∈ s
· rw [Set.indicator_of_mem hx, Set.indicator_of_mem hx, Pi.sub_apply, ← dist_eq_norm, Real.norm_eq_abs,
abs_of_nonneg hc]
exact hf x hx
· simp [Set.indicator_of_notMem hx]
refine le_trans (eLpNorm_mono this) ?_
rw [eLpNorm_indicator_const hs hp hp']
refine mul_le_mul_right' (le_of_eq ?_) _
rw [← ofReal_norm_eq_enorm, Real.norm_eq_abs, abs_of_nonneg hc]
