Polar-coordinate derivatives and integration over a closed annulus

The polar-coordinate change of variables for a translated closed annulus is the integral on [a, b] × [-π, π] with radial Jacobian r, when a ≥ 0. The two angular endpoints have measure zero, so the closed polar rectangle gives the same integral as the slit-plane chart. This form of Mathlib's Complex.integral_comp_polarCoord_symm is suitable for combining polar integration with Green's formula on a rectangle, without extending a map across the inner disc. For a continuous density in a real normed space, TauCeti.integral_annulus_eq_integral_circleMap expresses the same integral as an iterated integral with the radial variable outermost.

The derivative formulas describe the radial and angular vectors of the inverse complex polar map. Evaluating the alternating part of a bilinear pairing on those vectors gives its value on 1 and Complex.I, multiplied by the radial Jacobian.

theorem TauCeti.contDiff_add_polarCoord_symm (z₀ : ℂ) {n : WithTop ℕ∞} : ContDiff ℝ n fun (p : ℝ × ℝ) => z₀ + ↑Complex.polarCoord.symm p

The translated inverse complex polar map is smooth, including at zero radius.

theorem TauCeti.add_polarCoord_symm_mem_annulus (z₀ : ℂ) {a b : ℝ} (ha : 0 ≤ a) {p : ℝ × ℝ} (hp : p.1 ∈ Set.Icc a b) : z₀ + ↑Complex.polarCoord.symm p ∈ {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}

A polar point whose radius lies in a nonnegative closed interval maps into the annulus.

theorem TauCeti.add_polarCoord_symm_eq_circleMap (z₀ : ℂ) (p : ℝ × ℝ) : z₀ + ↑Complex.polarCoord.symm p = circleMap z₀ p.1 p.2

A constant-radius slice of the translated polar map is the circle parametrization.

theorem TauCeti.hasFDerivAt_add_polarCoord_symm (p : ℝ × ℝ) (z₀ : ℂ) : HasFDerivAt (fun (p : ℝ × ℝ) => z₀ + ↑Complex.polarCoord.symm p) (↑Complex.equivRealProdCLM.symm ∘SL fderivPolarCoordSymm p) p

The derivative of the translated inverse complex polar-coordinate map at any (r, θ). No restriction to the positive-radius chart is needed for this derivative formula.

theorem TauCeti.equivRealProd_symm_fderivPolarCoordSymm_apply_one_zero (p : ℝ × ℝ) : Complex.equivRealProdCLM.symm ((fderivPolarCoordSymm p) (1, 0)) = Complex.exp (↑p.2 * Complex.I)

The radial derivative of the inverse polar-coordinate map, expressed as a complex number, is the unit vector at the given angle.

theorem TauCeti.equivRealProd_symm_fderivPolarCoordSymm_apply_zero_one (p : ℝ × ℝ) : Complex.equivRealProdCLM.symm ((fderivPolarCoordSymm p) (0, 1)) = circleMap 0 p.1 p.2 * Complex.I

The angular derivative of the inverse polar-coordinate map, expressed as a complex number, is the tangent vector to the circle with the given radius and angle.

theorem LinearMap.apply_exp_circleMap_sub_swap {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] (B : V →ₗ[ℝ] V →ₗ[ℝ] W) (L : ℂ →ₗ[ℝ] V) (r θ : ℝ) : (B (L (Complex.exp (↑θ * Complex.I)))) (L (circleMap 0 r θ * Complex.I)) - (B (L (circleMap 0 r θ * Complex.I))) (L (Complex.exp (↑θ * Complex.I))) = r • ((B (L 1)) (L Complex.I) - (B (L Complex.I)) (L 1))

The alternating part of a bilinear map, after a real-linear map L, evaluated on the radial and angular polar-coordinate vectors is the radius times its value on 1 and I. The identity holds for every real radius, including zero and negative radii.

theorem MeasureTheory.Integrable.comp_complexPolarCoord_symm {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {f : ℂ → W} (hf : Integrable f volume) : IntegrableOn (fun (p : ℝ × ℝ) => p.1 • f (↑Complex.polarCoord.symm p)) polarCoord.target volume

The radial Jacobian makes the complex polar pullback of an integrable function integrable. This does not assert integrability on every angular slice; exceptional radii are only null.

theorem MeasureTheory.Integrable.integral_eq_integral_circleMap {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] {f : ℂ → W} (hf : Integrable f volume) (c : ℂ) : ∫ (z : ℂ), f z = ∫ (r : ℝ) in Set.Ioi 0, r • ∫ (θ : ℝ) in -Real.pi..Real.pi, f (circleMap c r θ)

Polar Fubini for an integrable planar function, with angular slices understood almost everywhere in the radius. Integrable point singularities require no continuous extension.

theorem Complex.integral_comp_polarCoord_symm_Icc {W : Type u_1} [NormedAddCommGroup W] [NormedSpace ℝ W] (f : ℂ → W) (z₀ : ℂ) {a b : ℝ} (ha : 0 ≤ a) : ∫ (p : ℝ × ℝ) in Set.Icc (a, -Real.pi) (b, Real.pi), p.1 • f (z₀ + ↑Complex.polarCoord.symm p) = ∫ (z : ℂ) in {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, f z

Polar integration over the closed annulus of radii a and b about z₀, with radial Jacobian p.1, including the disc case a = 0. The angular interval includes both endpoints, whose contribution is null.

theorem TauCeti.integral_annulus_eq_integral_circleMap {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℂ → F} {z₀ : ℂ} {a b : ℝ} (ha : 0 ≤ a) (hab : a ≤ b) (hf : ContinuousOn f {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}) : ∫ (z : ℂ) in {z : ℂ | a ≤ ‖z - z₀‖ ∧ ‖z - z₀‖ ≤ b}, f z = ∫ (r : ℝ) in a..b, r • ∫ (θ : ℝ) in -Real.pi..Real.pi, f (circleMap z₀ r θ)

Polar Fubini for a continuous density in a real normed space on a closed annulus, including the disc case a = 0, with the radial integral outermost and the angular variable running once around the circle.