Truncating a function to spanning sets

On a σ-finite measure space, multiplying a function f by the indicator of spanningSets μ N ∩ {x | ‖f x‖ ≤ N} gives a sequence converging to f pointwise, and the sets are measurable when f is strongly measurable.

theorem MeasureTheory.tendsto_indicator_spanningSets_inter_norm_le {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {V : Type u_2} [NormedAddCommGroup V] (f : α → V) (x : α) : Filter.Tendsto (fun (N : ℕ) => (spanningSets μ N ∩ {y : α | ‖f y‖ ≤ ↑N}).indicator f x) Filter.atTop (nhds (f x))

Every point eventually lies in spanningSets μ N ∩ {x | ‖f x‖ ≤ N}, so the indicator functions of these sets multiplied into f converge to f pointwise.

theorem MeasureTheory.measurableSet_spanningSets_inter_norm_le {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [SigmaFinite μ] {V : Type u_2} [NormedAddCommGroup V] {f : α → V} (hf : StronglyMeasurable f) (N : ℕ) : MeasurableSet (spanningSets μ N ∩ {x : α | ‖f x‖ ≤ ↑N})

The set where f is bounded by N and which lies in the N-th spanning set is measurable.