English
From finiteness of the measure, the density of 𝒜 extends to the finite-measure sets.
Русский
Из конечности меры следует плотность 𝒜 в отношении конечномеров.
LaTeX
$$$ μ.MeasureDense 𝒜 \\Rightarrow μ.MeasureDense \\{s \\mid s \\in 𝒜 \\land μ s \\neq \\infty\\}$$$
Lean4
/-- If `𝒜` is a measure-dense family of sets and `c : E`, then the set of constant indicators
with constant `c` whose underlying set is in `𝒜` is dense in the set of constant indicators
which are in `Lp E p μ` when `1 ≤ p < ∞`. -/
theorem indicatorConstLp_subset_closure (h𝒜 : μ.MeasureDense 𝒜) (c : E) :
{indicatorConstLp p hs hμs c | (s : Set X) (hs : MeasurableSet s) (hμs : μ s ≠ ∞)} ⊆
closure {indicatorConstLp p (h𝒜.measurable s hs) hμs c | (s : Set X) (hs : s ∈ 𝒜) (hμs : μ s ≠ ∞)} :=
by
obtain rfl | hc := eq_or_ne c 0
· refine Subset.trans ?_ subset_closure
rintro - ⟨s, ms, hμs, rfl⟩
obtain ⟨t, ht, hμt⟩ := h𝒜.nonempty'
refine ⟨t, ht, hμt, ?_⟩
simp_rw [indicatorConstLp]
simp
· have p_pos : 0 < p := lt_of_lt_of_le (by simp) one_le_p.elim
rintro - ⟨s, ms, hμs, rfl⟩
refine Metric.mem_closure_iff.2 fun ε hε ↦ ?_
have aux : 0 < (ε / ‖c‖) ^ p.toReal := rpow_pos_of_pos (div_pos hε (norm_pos_iff.2 hc)) _
obtain ⟨t, ht, hμt, hμst⟩ := h𝒜.fin_meas_approx ms hμs ((ε / ‖c‖) ^ p.toReal) aux
refine ⟨indicatorConstLp p (h𝒜.measurable t ht) hμt c, ⟨t, ht, hμt, rfl⟩, ?_⟩
rw [dist_indicatorConstLp_eq_norm, norm_indicatorConstLp p_pos.ne.symm p_ne_top.elim]
calc
‖c‖ * μ.real (s ∆ t) ^ (1 / p.toReal) < ‖c‖ * (ENNReal.ofReal ((ε / ‖c‖) ^ p.toReal)).toReal ^ (1 / p.toReal) :=
by
have := toReal_pos p_pos.ne.symm p_ne_top.elim
rw [measureReal_def]
gcongr
exact ofReal_ne_top
_ = ε := by
rw [toReal_ofReal (rpow_nonneg (div_nonneg hε.le (norm_nonneg _)) _), one_div,
Real.rpow_rpow_inv (div_nonneg hε.le (norm_nonneg _)) (toReal_pos p_pos.ne.symm p_ne_top.elim).ne.symm,
mul_div_cancel₀ _ (norm_ne_zero_iff.2 hc)]
