English
The natural map sending nonnegative simple functions to their Lp-equivalence classes has dense range in the Lp-space of nonnegative functions; i.e., simple nonnegative functions are dense in Lp+.
Русский
Естественный отображение неотрицательных простой функций в соответствующие классы Lp имеет плотный образ в пространстве Lp+; то есть неотрицательные простые функции плотны в Lp.
LaTeX
$$$\\\\operatorname{DenseRange}\\\\big( \\\\mathrm{coeSimpleFuncNonnegToLpNonneg}(p,\\\\mu, G) \\\\big)$$$
Lean4
theorem denseRange_coeSimpleFuncNonnegToLpNonneg [hp : Fact (1 ≤ p)] (hp_ne_top : p ≠ ∞) :
DenseRange (coeSimpleFuncNonnegToLpNonneg p μ G) := fun g ↦
by
borelize G
rw [mem_closure_iff_seq_limit]
have hg_memLp : MemLp (g : α → G) p μ := Lp.memLp (g : Lp G p μ)
have zero_mem : (0 : G) ∈ (range (g : α → G) ∪ {0} : Set G) ∩ {y | 0 ≤ y} := by
simp only [union_singleton, mem_inter_iff, mem_insert_iff, true_or, mem_setOf_eq, le_refl, and_self_iff]
have : SeparableSpace ((range (g : α → G) ∪ {0}) ∩ {y | 0 ≤ y} : Set G) :=
by
apply IsSeparable.separableSpace
apply IsSeparable.mono _ Set.inter_subset_left
exact (Lp.stronglyMeasurable (g : Lp G p μ)).isSeparable_range.union (finite_singleton _).isSeparable
have g_meas : Measurable (g : α → G) := (Lp.stronglyMeasurable (g : Lp G p μ)).measurable
let x n := SimpleFunc.approxOn (g : α → G) g_meas ((range (g : α → G) ∪ {0}) ∩ {y | 0 ≤ y}) 0 zero_mem n
have hx_nonneg : ∀ n, 0 ≤ x n := by
intro n a
change x n a ∈ {y : G | 0 ≤ y}
have A : (range (g : α → G) ∪ {0} : Set G) ∩ {y | 0 ≤ y} ⊆ {y | 0 ≤ y} := inter_subset_right
apply A
exact SimpleFunc.approxOn_mem g_meas _ n a
have hx_memLp : ∀ n, MemLp (x n) p μ := SimpleFunc.memLp_approxOn _ hg_memLp _ ⟨aestronglyMeasurable_const, by simp⟩
have h_toLp := fun n => MemLp.coeFn_toLp (hx_memLp n)
have hx_nonneg_Lp : ∀ n, 0 ≤ toLp (x n) (hx_memLp n) :=
by
intro n
rw [← Lp.simpleFunc.coeFn_le, Lp.simpleFunc.toLp_eq_toLp]
filter_upwards [Lp.simpleFunc.coeFn_zero p μ G, h_toLp n] with a ha0 ha_toLp
rw [ha0, ha_toLp]
exact hx_nonneg n a
have hx_tendsto : Tendsto (fun n : ℕ => eLpNorm ((x n : α → G) - (g : α → G)) p μ) atTop (𝓝 0) :=
by
apply SimpleFunc.tendsto_approxOn_Lp_eLpNorm g_meas zero_mem hp_ne_top
· have hg_nonneg : (0 : α → G) ≤ᵐ[μ] g := (Lp.coeFn_nonneg _).mpr g.2
refine hg_nonneg.mono fun a ha => subset_closure ?_
simpa using ha
· simp_rw [sub_zero]; exact hg_memLp.eLpNorm_lt_top
refine
⟨fun n => (coeSimpleFuncNonnegToLpNonneg p μ G) ⟨toLp (x n) (hx_memLp n), hx_nonneg_Lp n⟩, fun n =>
mem_range_self _, ?_⟩
suffices Tendsto (fun n : ℕ => (toLp (x n) (hx_memLp n) : Lp G p μ)) atTop (𝓝 (g : Lp G p μ))
by
rw [tendsto_iff_dist_tendsto_zero] at this ⊢
simp_rw [Subtype.dist_eq]
exact this
rw [Lp.tendsto_Lp_iff_tendsto_eLpNorm']
refine Filter.Tendsto.congr (fun n => eLpNorm_congr_ae (EventuallyEq.sub ?_ ?_)) hx_tendsto
· symm
rw [Lp.simpleFunc.toLp_eq_toLp]
exact h_toLp n
· rfl
