Measurability and integrability of the sinc function

Main statements

• measurable_sinc: the sinc function is measurable.
• integrable_sinc: the sinc function is integrable with respect to any finite measure on ℝ.

theorem Real.measurable_sinc : Measurable sinc

theorem Real.stronglyMeasurable_sinc : MeasureTheory.StronglyMeasurable sinc

theorem Real.integrable_sinc {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable sinc μ

theorem Measurable.sinc {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) : Measurable fun (x : α) => Real.sinc (f x)

theorem AEMeasurable.sinc {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : AEMeasurable (fun (x : α) => Real.sinc (f x)) μ

theorem MeasureTheory.StronglyMeasurable.sinc {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} (hf : StronglyMeasurable f) : StronglyMeasurable fun (x : α) => Real.sinc (f x)

theorem MeasureTheory.AEStronglyMeasurable.sinc {α : Type u_1} {x✝ : MeasurableSpace α} {f : α → ℝ} {μ : Measure α} (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun (x : α) => Real.sinc (f x)) μ