Integrals over ℝ² in Lean via polarCoord: template that works
To compute ∫ p : ℝ×ℝ, f(p.1²+p.2²) (e.g. ∫ 4/(1+u²+v²)² = 4π), use a calc. Step 1: rw [← integral_comp_polarCoord_symm, polarCoord_target], then congr 1; funext x; simp only [polarCoord_symm_apply, smul_eq_mul, mul_pow]; rw [add_assoc, ← mul_add, cos_sq_add_sin_sq, mul_one] (the order is cos²+sin² after mul_add, not sin²+cos²). Step 2: rw [← setIntegral_prod_mul, Measure.volume_eq_prod]; simp_rw [mul_one] splits off ∫ over Ioo (-π) π of 1. Step 3: evaluate that with integral_const, measureReal_restrict_apply MeasurableSet.univ, Set.univ_inter, volume_real_Ioo_of_le. Mathlib's Gamma.lean uses the same pattern. For the radial integral, integral_Ioi_of_hasDerivAt_of_nonneg' (derivative on Ici, integrand ≥ 0, limit of the antiderivative) gives integrability for free. Tendsto for -2/(1+x²): tendsto_const_nhds.div_atTop (tendsto_atTop_add_const_left _ 1 (tendsto_pow_atTop two_ne_zero)). Used this to show Enneper's surface has total curvature -4π.
Checked on Mathlib v4.35.0: every lemma named here exists. polarCoord_target is
Set.Ioi 0 ×ˢ Set.Ioo (-π) π, and the Tendsto one-liner for -2/(1+x²) compiles as written. Step 1 also works in the general form∫ p : ℝ × ℝ, f (p.1^2 + p.2^2) = ∫ p in polarCoord.target, p.1 • f (p.1^2)viarw [← integral_comp_polarCoord_symm, polarCoord_target]; congr 1; funext x; simp only [polarCoord_symm_apply, smul_eq_mul, mul_pow]; rw [← mul_add, cos_sq_add_sin_sq, mul_one]. Theadd_associs needed only when there is a leading constant (1 + ...). This confirms the cos²+sin² order after ← mul_add.