English
A nonnegative integral equality under polar transformation holds: the lintegral over polarCoord.target with weight |p.1| equals the lintegral over ℝ^2.
Русский
Неотрицанное интегрирование сохраняется под полярной заменой: интеграл по polarCoord.target с весом |p.1| эквивалентен интегралу по всей плоскости.
LaTeX
$$$$ \int_{p \in \mathrm{polarCoord.target}} \mathbf{ofReal}(p.1) \; f(\mathrm{polarCoord.symm}(p)) \, dp \\= \int_{p \in \mathbb{R}^2} f(p) \, dp. $$$$
Lean4
theorem lintegral_comp_polarCoord_symm (f : ℝ × ℝ → ℝ≥0∞) :
∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) = ∫⁻ (p : ℝ × ℝ), f p :=
by
symm
calc
_ = ∫⁻ p in polarCoord.symm '' polarCoord.target, f p := by
rw [← setLIntegral_univ, setLIntegral_congr polarCoord_source_ae_eq_univ.symm,
polarCoord.symm_image_target_eq_source]
_ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal |p.1| • f (polarCoord.symm p) :=
by
rw [lintegral_image_eq_lintegral_abs_det_fderiv_mul volume _
(fun p _ ↦ (hasFDerivAt_polarCoord_symm p).hasFDerivWithinAt)]
· simp_rw [det_fderivPolarCoordSymm]; rfl
exacts [polarCoord.symm.injOn, measurableSet_Ioi.prod measurableSet_Ioo]
_ = ∫⁻ (p : ℝ × ℝ) in polarCoord.target, ENNReal.ofReal p.1 • f (polarCoord.symm p) :=
by
refine setLIntegral_congr_fun polarCoord.open_target.measurableSet (fun x hx ↦ ?_)
rw [abs_of_pos hx.1]
