English
The polarCoord source is almost everywhere equal to the whole space with respect to volume measure.
Русский
Область определения полярной карты почти всюду совпадает с всей плоскостью по мере объёма.
LaTeX
$$$$ \text{polarCoord.source} =_{\mathrm{ae}} \text{univ}. $$$$
Lean4
theorem polarCoord_source_ae_eq_univ : polarCoord.source =ᵐ[volume] univ :=
by
have A : polarCoord.sourceᶜ ⊆ LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) :=
by
intro x hx
simp only [polarCoord_source, compl_union, mem_inter_iff, mem_compl_iff, mem_setOf_eq, not_lt,
Classical.not_not] at hx
exact hx.2
have B : volume (LinearMap.ker (LinearMap.snd ℝ ℝ ℝ) : Set (ℝ × ℝ)) = 0 :=
by
apply Measure.addHaar_submodule
rw [Ne, LinearMap.ker_eq_top]
intro h
have : (LinearMap.snd ℝ ℝ ℝ) (0, 1) = (0 : ℝ × ℝ →ₗ[ℝ] ℝ) (0, 1) := by rw [h]
simp at this
simp only [ae_eq_univ]
exact le_antisymm ((measure_mono A).trans (le_of_eq B)) bot_le
