Simultaneous continuous approximation for finitely many measures

Let α be a normal topological space with its Borel σ-algebra, for instance a compact Hausdorff space, and let μ i be finitely many weakly regular measures on α. A function f : α → E with values in a real normed space that is integrable for every μ i is approximated in L¹(μ i), simultaneously for all i, by a single continuous function g: approximate f in L¹ of the sum measure ∑ i, μ i, which is again weakly regular, and use monotonicity of the integral in the measure.

If the measures are finite and ‖f x‖ ≤ M everywhere, the approximant can be chosen with the same bound. Composing g with the radial retraction onto the closed ball of radius M keeps it continuous, does not move the values of f, and at most doubles the distance from them, so it costs only a factor of two in each L¹ error. A sequence of such approximants then has L¹ errors tending to zero for every μ i.

This is the approximation step that extends a representation of the continuous functions on a compact Hausdorff space to bounded Borel functions: the scalar measures of the representation are finitely many finite regular measures at a time, and the uniform bound keeps the approximating operators bounded.

Main results

• MeasureTheory.exists_continuous_forall_integral_norm_sub_le: an integrable function is approximated in L¹(μ i) for all i at once by one continuous function.
• MeasureTheory.exists_continuous_norm_le_forall_integral_norm_sub_le: a function bounded by M is approximated in this way by a continuous function bounded by M.
• MeasureTheory.exists_seq_continuous_norm_le_tendsto_integral_norm_sub: a sequence of continuous functions bounded by M whose L¹(μ i) distances to f tend to zero for all i.
• TauCeti.BoundedBorelFunction.eq_of_forall_ofContinuousMap_eq: on a compact normal space, two maps on bounded Borel symbols that are Lipschitz for L¹ distances against finite weakly regular measures and agree on continuous symbols are equal.

Provenance

The sum-measure argument for a finite family is adapted from ForTauCeti/Analysis/InnerProductSpace/BorelCalculus/Polarization.lean in the Kitware DKPS formalization.

References

• W. Rudin, Real and Complex Analysis, 3rd ed., McGraw–Hill (1987), Theorem 3.14 (density of continuous functions in L^p) and Lusin's theorem 2.24 (radial truncation of approximants).

theorem MeasureTheory.exists_continuous_forall_integral_norm_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_3} [Finite ι] {μ : ι → Measure α} [∀ (i : ι), (μ i).WeaklyRegular] {f : α → E} (hf : ∀ (i : ι), Integrable f (μ i)) {ε : ℝ} (hε : 0 < ε) : ∃ (g : C(α, E)), ∀ (i : ι), Integrable (⇑g) (μ i) ∧ ∫ (x : α), ‖f x - g x‖ ∂μ i ≤ ε

Simultaneous continuous approximation in L¹. On a normal Borel space, a function that is integrable for each of finitely many weakly regular measures μ i is approximated in L¹(μ i), for all i at once, by a single continuous function integrable for every μ i.

theorem MeasureTheory.exists_continuous_norm_le_forall_integral_norm_sub_le {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_3} [Finite ι] {μ : ι → Measure α} [∀ (i : ι), (μ i).WeaklyRegular] [∀ (i : ι), IsFiniteMeasure (μ i)] {f : α → E} (hf : ∀ (i : ι), AEStronglyMeasurable f (μ i)) {M : ℝ} (hfM : ∀ (x : α), ‖f x‖ ≤ M) {ε : ℝ} (hε : 0 < ε) : ∃ (g : C(α, E)), (∀ (x : α), ‖g x‖ ≤ M) ∧ ∀ (i : ι), Integrable (⇑g) (μ i) ∧ ∫ (x : α), ‖f x - g x‖ ∂μ i ≤ ε

Simultaneous bounded continuous approximation in L¹. On a normal Borel space, a function bounded by M and almost everywhere strongly measurable for each of finitely many finite weakly regular measures μ i is approximated in L¹(μ i), for all i at once, by a single continuous function that is also bounded by M and integrable for every μ i.

theorem MeasureTheory.exists_seq_continuous_norm_le_tendsto_integral_norm_sub {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [MeasurableSpace α] [BorelSpace α] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {ι : Type u_3} [Finite ι] {μ : ι → Measure α} [∀ (i : ι), (μ i).WeaklyRegular] [∀ (i : ι), IsFiniteMeasure (μ i)] {f : α → E} (hf : ∀ (i : ι), AEStronglyMeasurable f (μ i)) {M : ℝ} (hfM : ∀ (x : α), ‖f x‖ ≤ M) : ∃ (g : ℕ → C(α, E)), (∀ (n : ℕ) (x : α), ‖(g n) x‖ ≤ M) ∧ (∀ (n : ℕ) (i : ι), Integrable (⇑(g n)) (μ i)) ∧ ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), ‖f x - (g n) x‖ ∂μ i) Filter.atTop (nhds 0)

Bounded continuous approximating sequences. On a normal Borel space, a function bounded by M and almost everywhere strongly measurable for each of finitely many finite weakly regular measures μ i is the limit in L¹(μ i), for all i at once, of a sequence of continuous functions bounded by M and integrable for every μ i.

theorem TauCeti.BoundedBorelFunction.eq_of_forall_ofContinuousMap_eq {α : Type u_1} [TopologicalSpace α] [NormalSpace α] [CompactSpace α] [MeasurableSpace α] [BorelSpace α] {F : Type u_2} [MetricSpace F] {ν₁ ν₂ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure ν₁] [MeasureTheory.IsFiniteMeasure ν₂] [ν₁.WeaklyRegular] [ν₂.WeaklyRegular] {Φ Ψ : BoundedBorelFunction α → F} {C₁ C₂ : ℝ} (hΦ : ∀ (f g : BoundedBorelFunction α), dist (Φ f) (Φ g) ≤ C₁ * ∫ (x : α), ‖f x - g x‖ ∂ν₁) (hΨ : ∀ (f g : BoundedBorelFunction α), dist (Ψ f) (Ψ g) ≤ C₂ * ∫ (x : α), ‖f x - g x‖ ∂ν₂) (h : ∀ (g : C(α, ℂ)), Φ (ofContinuousMap g) = Ψ (ofContinuousMap g)) : Φ = Ψ

Extension from continuous symbols. Let ν₁ and ν₂ be finite weakly regular measures on a compact normal Borel space. If Φ is Lipschitz for the L¹(ν₁) distance of bounded Borel symbols, Ψ is Lipschitz for the L¹(ν₂) distance, and Φ and Ψ agree on continuous symbols, then they agree on every bounded Borel symbol: continuous symbols bounded by ‖f‖ approximate f in L¹(ν₁) and L¹(ν₂) at once.