Lean4
/-- A continuous function with compact support on a product space can be uniformly approximated by
simple functions. The subtlety is that we do not assume that the spaces are separable, so the
product of the Borel sigma algebras might not contain all open sets, but still it contains enough
of them to approximate compactly supported continuous functions. -/
theorem exists_simpleFunc_approx_of_prod [PseudoMetricSpace α] {f : X × Y → α} (hf : Continuous f)
(h'f : HasCompactSupport f) {ε : ℝ} (hε : 0 < ε) : ∃ (g : SimpleFunc (X × Y) α), ∀ x, dist (f x) (g x) < ε :=
by
have M :
∀ (K : Set (X × Y)),
IsCompact K →
∃ (g : SimpleFunc (X × Y) α), ∃ (s : Set (X × Y)), MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε :=
by
intro K hK
apply
IsCompact.induction_on (p := fun t ↦
∃ (g : SimpleFunc (X × Y) α), ∃ (s : Set (X × Y)), MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) (g x) < ε) hK
· exact ⟨0, ∅, by simp⟩
· intro t t' htt' ⟨g, s, s_meas, ts, hg⟩
exact ⟨g, s, s_meas, htt'.trans ts, hg⟩
· intro t t' ⟨g, s, s_meas, ts, hg⟩ ⟨g', s', s'_meas, t's', hg'⟩
refine ⟨g.piecewise s s_meas g', s ∪ s', s_meas.union s'_meas, union_subset_union ts t's', fun p hp ↦ ?_⟩
by_cases H : p ∈ s
· simpa [H, SimpleFunc.piecewise_apply] using hg p H
· simp only [SimpleFunc.piecewise_apply, H, ite_false]
apply hg'
simpa [H] using (mem_union _ _ _).1 hp
· rintro ⟨x, y⟩ -
obtain ⟨u, v, hu, xu, hv, yv, huv⟩ :
∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧ u ×ˢ v ⊆ {z | dist (f z) (f (x, y)) < ε} :=
mem_nhds_prod_iff'.1 <| Metric.continuousAt_iff'.1 hf.continuousAt ε hε
refine ⟨u ×ˢ v, nhdsWithin_le_nhds <| (hu.prod hv).mem_nhds (mk_mem_prod xu yv), ?_⟩
exact
⟨SimpleFunc.const _ (f (x, y)), u ×ˢ v, hu.measurableSet.prod hv.measurableSet, Subset.rfl, fun z hz ↦ huv hz⟩
obtain ⟨g, s, s_meas, fs, hg⟩ :
∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
MeasurableSet s ∧ tsupport f ⊆ s ∧ ∀ (x : X × Y), x ∈ s → dist (f x) (g x) < ε :=
M _ h'f
refine ⟨g.piecewise s s_meas 0, fun p ↦ ?_⟩
by_cases H : p ∈ s
· simpa [H, SimpleFunc.piecewise_apply] using hg p H
· have : f p = 0 := by
contrapose! H
rw [← Function.mem_support] at H
exact fs (subset_tsupport _ H)
simp [SimpleFunc.piecewise_apply, H, this, hε]
