Measurability of radial projection

This file proves that normalization x ↦ ‖x‖⁻¹ • x and the direction map TauCeti.sphereDirection e to the unit sphere are measurable.

Main results

• TauCeti.measurable_normalize: normalization is measurable.
• TauCeti.measurable_sphereDirection: the direction map is measurable.

theorem TauCeti.measurable_normalize {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] : Measurable NormedSpace.normalize

Normalization x ↦ ‖x‖⁻¹ • x is measurable.

theorem TauCeti.measurable_sphereDirection {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (e : ↑(Metric.sphere 0 1)) : Measurable (sphereDirection e)

The direction map is measurable.