Approximation by interval step functions

Sampling a continuous function at the left nodes of a sufficiently fine uniform subdivision approximates it uniformly on a compact interval. Together with the density of continuous functions in L¹, this gives approximation of an integrable function by interval step functions.

noncomputable def MeasureTheory.intervalStep {E : Type u_1} (a δ : ℝ) (g : ℝ → E) (t : ℝ) : E

Sampling at the left endpoints of intervals of width δ starting at a. Points to the left of a are sampled at a when 0 < δ.

Equations

• MeasureTheory.intervalStep a δ g t = g (a + ↑⌊(t - a) / δ⌋₊ * δ)

theorem MeasureTheory.integrableOn_intervalStep {E : Type u_1} [NormedAddCommGroup E] (a b δ : ℝ) (g : ℝ → E) : IntegrableOn (intervalStep a δ g) (Set.Ioc a b) volume

Sampling any function gives a step function integrable on a finite interval.

theorem MeasureTheory.exists_intervalStep_dist_lt {E : Type u_1} [PseudoMetricSpace E] (g : ℝ → E) {a b ε : ℝ} (hg : ContinuousOn g (Set.Icc a b)) (hab : a < b) (hε : 0 < ε) : ∃ (N : ℕ), 0 < N ∧ ∀ t ∈ Set.Icc a b, dist (intervalStep a ((b - a) / ↑N) g t) (g t) < ε

Left-node sampling on a sufficiently fine uniform subdivision uniformly approximates a function continuous on a compact interval.

theorem MeasureTheory.intervalStep_eq {E : Type u_1} {a δ t : ℝ} (hδ : 0 < δ) (g : ℝ → E) (i : ℕ) (ht : t ∈ Set.Ico (a + ↑i * δ) (a + (↑i + 1) * δ)) : intervalStep a δ g t = g (a + ↑i * δ)

The sampled step function is constant between two successive subdivision nodes.

theorem MeasureTheory.IntegrableOn.exists_intervalStep_integral_norm_sub_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b ε : ℝ} (hf : IntegrableOn f (Set.Ioc a b) volume) (hab : a < b) (hε : 0 < ε) : ∃ (N : ℕ), 0 < N ∧ ∃ (g : BoundedContinuousFunction ℝ E), ∫ (t : ℝ) in Set.Ioc a b, ‖intervalStep a ((b - a) / ↑N) (⇑g) t - f t‖ ≤ ε

An integrable function on a finite interval can be approximated in L¹ by finite interval step functions.