Lean4
/-- If the measure `μ` is separable (in particular if `X` is countably generated and `μ` is
`s`-finite), if `E` is a second-countable `NormedAddCommGroup`, and if `1 ≤ p < +∞`,
then the associated `Lᵖ` space is second-countable. -/
instance SecondCountableTopology [IsSeparable μ] [TopologicalSpace.SeparableSpace E] :
SecondCountableTopology (Lp E p μ) := by
-- It is enough to show that the space is separable, i.e. admits a countable and dense subset.
refine
@UniformSpace.secondCountable_of_separable _ _ _
?_
-- There exists a countable and measure-dense family, and we can keep only the sets with finite
-- measure while preserving the two properties. This family is denoted `𝒜₀`.
rcases exists_countable_measureDense μ with ⟨𝒜, count_𝒜, h𝒜⟩
have h𝒜₀ := Measure.MeasureDense.fin_meas h𝒜
set 𝒜₀ := {s | s ∈ 𝒜 ∧ μ s ≠ ∞}
have count_𝒜₀ : 𝒜₀.Countable := count_𝒜.mono fun _ ⟨h, _⟩ ↦ h
have p_ne_zero : p ≠ 0 := ne_of_gt <| lt_of_lt_of_le (by simp) one_le_p.elim
rcases exists_countable_dense E with
⟨u, countable_u, dense_u⟩
-- The countable and dense subset of `Lᵖ` we are going to build is the set of finite sums of
-- constant indicators with support in `𝒜₀`, and is denoted `D`. To make manipulations easier,
-- we define the function `key` which given an integer `n` and two families of `n` elements
-- in `u` and `𝒜₀` associates the corresponding sum.
let key (n : ℕ) (d : Fin n → u) (s : Fin n → 𝒜₀) : (Lp E p μ) :=
∑ i, indicatorConstLp p (h𝒜₀.measurable (s i) (Subtype.mem (s i))) (s i).2.2 (d i : E)
let D := {s : Lp E p μ | ∃ n d t, s = key n d t}
refine ⟨D, ?_, ?_⟩
· -- Countability directly follows from countability of `u` and `𝒜₀`. The function `f` below
-- is the uncurried version of `key`, which is easier to manipulate as countability of the
-- domain is automatically inferred.
let f (nds : Σ n : ℕ, (Fin n → u) × (Fin n → 𝒜₀)) : Lp E p μ := key nds.1 nds.2.1 nds.2.2
have := count_𝒜₀.to_subtype
have := countable_u.to_subtype
have : D ⊆ range f := by
rintro - ⟨n, d, s, rfl⟩
use ⟨n, (d, s)⟩
exact (countable_range f).mono this
· -- Let's turn to the density. Thanks to the density of simple functions in `Lᵖ`, it is enough
-- to show that the closure of `D` contains constant indicators which are in `Lᵖ` (i. e. the
-- set has finite measure), is closed by sum and closed.
-- This is given by `Lp.induction`.
refine Lp.induction p_ne_top.elim (motive := fun f ↦ f ∈ closure D) ?_ ?_ isClosed_closure
· intro a s ms hμs
apply ne_of_lt at hμs
rw [SeminormedAddCommGroup.mem_closure_iff]
intro ε ε_pos
have μs_pow_nonneg : 0 ≤ μ.real s ^ (1 / p.toReal) :=
Real.rpow_nonneg ENNReal.toReal_nonneg
_
-- To do so, we first pick `b ∈ u` such that `‖a - b‖ < ε / (3 * (1 + (μ s)^(1/p)))`.
have approx_a_pos : 0 < ε / (3 * (1 + μ.real s ^ (1 / p.toReal))) := div_pos ε_pos (by linarith [μs_pow_nonneg])
have ⟨b, b_mem, hb⟩ := SeminormedAddCommGroup.mem_closure_iff.1 (dense_u a) _ approx_a_pos
rcases
SeminormedAddCommGroup.mem_closure_iff.1 (h𝒜₀.indicatorConstLp_subset_closure p b ⟨s, ms, hμs, rfl⟩) (ε / 3)
(by linarith [ε_pos]) with
⟨-, ⟨t, ht, hμt, rfl⟩, hst⟩
have mt := h𝒜₀.measurable t ht
refine ⟨indicatorConstLp p mt hμt b, ⟨1, fun _ ↦ ⟨b, b_mem⟩, fun _ ↦ ⟨t, ht⟩, by simp [key]⟩, ?_⟩
rw [Lp.simpleFunc.coe_indicatorConst, ← sub_add_sub_cancel _ (indicatorConstLp p ms hμs b), ← add_halves ε]
refine lt_of_le_of_lt (b := ε / 3 + ε / 3) (norm_add_le_of_le ?_ hst.le) (by linarith [ε_pos])
rw [indicatorConstLp_sub, norm_indicatorConstLp p_ne_zero p_ne_top.elim]
calc
‖a - b‖ * μ.real s ^ (1 / p.toReal) ≤ (ε / (3 * (1 + μ.real s ^ (1 / p.toReal)))) * μ.real s ^ (1 / p.toReal) :=
mul_le_mul_of_nonneg_right (le_of_lt hb) μs_pow_nonneg
_ ≤ ε / 3 := by
rw [← mul_one (ε / 3), div_mul_eq_div_mul_one_div, mul_assoc, one_div_mul_eq_div]
exact
mul_le_mul_of_nonneg_left ((div_le_one (by linarith [μs_pow_nonneg])).2 (by linarith)) (by linarith [ε_pos])
· -- Now we have to show that the closure of `D` is closed by sum. Let `f` and `g` be two
-- functions in `Lᵖ` which are also in the closure of `D`.
rintro f g hf hg - f_mem g_mem
rw [SeminormedAddCommGroup.mem_closure_iff] at *
intro ε ε_pos
rcases f_mem (ε / 2) (by linarith [ε_pos]) with ⟨bf, ⟨nf, df, sf, bf_eq⟩, hbf⟩
rcases g_mem (ε / 2) (by linarith [ε_pos]) with
⟨bg, ⟨ng, dg, sg, bg_eq⟩, hbg⟩
-- It is obvious that `D` is closed by sum, it suffices to concatenate the family of
-- elements of `u` and the family of elements of `𝒜₀`.
let d := fun i : Fin (nf + ng) ↦
if h : i < nf then df (Fin.castLT i h) else dg (Fin.subNat nf (Fin.cast (Nat.add_comm ..) i) (le_of_not_gt h))
let s := fun i : Fin (nf + ng) ↦
if h : i < nf then sf (Fin.castLT i h)
else
sg
(Fin.subNat nf (Fin.cast (Nat.add_comm ..) i) (le_of_not_gt h))
-- So we can use `bf + bg`.
refine ⟨bf + bg, ⟨nf + ng, d, s, ?_⟩, ?_⟩
· simp [key, d, s, Fin.sum_univ_add, bf_eq, bg_eq]
· -- We have
-- `‖f + g - (bf + bg)‖ₚ`
-- `≤ ‖f - bf‖ₚ + ‖g - bg‖ₚ`
-- `< ε/2 + ε/2 = ε`.
calc
‖MemLp.toLp f hf + MemLp.toLp g hg - (bf + bg)‖ = ‖(MemLp.toLp f hf) - bf + ((MemLp.toLp g hg) - bg)‖ := by
congr; abel
_ ≤ ‖(MemLp.toLp f hf) - bf‖ + ‖(MemLp.toLp g hg) - bg‖ := norm_add_le ..
_ < ε := by linarith [hbf, hbg]
