English
If there are closed s contained in an open u with finite μ-measure of s, and a vector c, there exists a continuous f with values in E, equal to c on s, vanishing outside u, uniformly bounded by ‖c‖, and such that its deviation from the s-indicator approximation has arbitrarily small eLp-norm; moreover f belongs to Lp.
Русский
При наличии замкнутого s ⊆ открытого u с конечной мерой μ(s) и вектора c существует непрерывная функция f с значениями в E, равная c на s, нулевая за пределами u, ограниченная по норме верхом ‖c‖, такая что eLp-норма разности f и индикатора s равна произвольно малой величине; кроме того f принадлежит Lp.
LaTeX
$$$\\exists f:\\alpha \\to E\\;\\Big( Continuous f \\land eLpNorm \\big(f - s.indicator (fun _y => c)\\,\\big) p μ \\le ε \\land \\forall x, \\|f x\\| ≤ \\|c\\| \\land \\operatorname{support} f \\subseteq u \\land MemLp f p μ \\Big)$$$
Lean4
/-- A variant of Urysohn's lemma, `ℒ^p` version, for an outer regular measure `μ`:
consider two sets `s ⊆ u` which are respectively closed and open with `μ s < ∞`, and a vector `c`.
Then one may find a continuous function `f` equal to `c` on `s` and to `0` outside of `u`,
bounded by `‖c‖` everywhere, and such that the `ℒ^p` norm of `f - s.indicator (fun y ↦ c)` is
arbitrarily small. Additionally, this function `f` belongs to `ℒ^p`. -/
theorem exists_continuous_eLpNorm_sub_le_of_closed [μ.OuterRegular] (hp : p ≠ ∞) {s u : Set α} (s_closed : IsClosed s)
(u_open : IsOpen u) (hsu : s ⊆ u) (hs : μ s ≠ ∞) (c : E) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
∃ f : α → E,
Continuous f ∧
eLpNorm (fun x => f x - s.indicator (fun _y => c) x) p μ ≤ ε ∧
(∀ x, ‖f x‖ ≤ ‖c‖) ∧ Function.support f ⊆ u ∧ MemLp f p μ :=
by
obtain ⟨η, η_pos, hη⟩ : ∃ η : ℝ≥0, 0 < η ∧ ∀ s : Set α, μ s ≤ η → eLpNorm (s.indicator fun _x => c) p μ ≤ ε :=
exists_eLpNorm_indicator_le hp c hε
have ηpos : (0 : ℝ≥0∞) < η := ENNReal.coe_lt_coe.2 η_pos
obtain ⟨V, sV, V_open, h'V, hV⟩ : ∃ (V : Set α), V ⊇ s ∧ IsOpen V ∧ μ V < ∞ ∧ μ (V \ s) < η :=
s_closed.measurableSet.exists_isOpen_diff_lt hs ηpos.ne'
let v := u ∩ V
have hsv : s ⊆ v := subset_inter hsu sV
have hμv : μ v < ∞ := (measure_mono inter_subset_right).trans_lt h'V
obtain ⟨g, hgv, hgs, hg_range⟩ :=
exists_continuous_zero_one_of_isClosed (u_open.inter V_open).isClosed_compl s_closed
(disjoint_compl_left_iff.2 hsv)
-- Multiply this by `c` to get a continuous approximation to the function `f`; the key point is
-- that this is pointwise bounded by the indicator of the set `v \ s`, which has small measure.
have g_norm : ∀ x, ‖g x‖ = g x := fun x => by rw [Real.norm_eq_abs, abs_of_nonneg (hg_range x).1]
have gc_bd0 : ∀ x, ‖g x • c‖ ≤ ‖c‖ := by
intro x
simp only [norm_smul, g_norm x]
apply mul_le_of_le_one_left (norm_nonneg _)
exact (hg_range x).2
have gc_bd : ∀ x, ‖g x • c - s.indicator (fun _x => c) x‖ ≤ ‖(v \ s).indicator (fun _x => c) x‖ :=
by
intro x
by_cases hv : x ∈ v
· rw [← Set.diff_union_of_subset hsv] at hv
rcases hv with hsv | hs
· simpa only [hsv.2, Set.indicator_of_notMem, not_false_iff, sub_zero, hsv, Set.indicator_of_mem] using gc_bd0 x
· simp [hgs hs, hs]
· simp [hgv hv, show x ∉ s from fun h => hv (hsv h)]
have gc_support : (Function.support fun x : α => g x • c) ⊆ v :=
by
refine Function.support_subset_iff'.2 fun x hx => ?_
simp only [hgv hx, Pi.zero_apply, zero_smul]
have gc_mem : MemLp (fun x => g x • c) p μ :=
by
refine MemLp.smul (memLp_top_const _) ?_ (p := p) (q := ∞)
refine ⟨g.continuous.aestronglyMeasurable, ?_⟩
have : eLpNorm (v.indicator fun _x => (1 : ℝ)) p μ < ⊤ :=
(eLpNorm_indicator_const_le _ _).trans_lt <| by simp [lt_top_iff_ne_top, hμv.ne]
refine (eLpNorm_mono fun x => ?_).trans_lt this
by_cases hx : x ∈ v
·
simp only [hx, abs_of_nonneg (hg_range x).1, (hg_range x).2, Real.norm_eq_abs, indicator_of_mem,
CStarRing.norm_one]
· simp only [hgv hx, Pi.zero_apply, Real.norm_eq_abs, abs_zero, abs_nonneg]
refine
⟨fun x => g x • c, g.continuous.smul continuous_const, (eLpNorm_mono gc_bd).trans ?_, gc_bd0,
gc_support.trans inter_subset_left, gc_mem⟩
exact hη _ ((measure_mono (diff_subset_diff inter_subset_right Subset.rfl)).trans hV.le)
