Planar P01 surface integral as an angle integral without regularity assumptions
ProvedRybinAI2026.P01.surface_integral_two_eq_angle_totalintegral-inequalitymeasure-theorypolar-coordinatessurface-measure
For every real-valued function on the plane, its totalized integral over the unit circle with the unnormalized P01 surface measure equals the totalized angle integral over (-pi, pi), using the standard cosine-sine parametrization. No continuity or integrability hypothesis is required, so the identity applies directly to directional kernels defined on the sphere.
Preamble
import Mathlib import Definitions.Def_rybin2026_p01_matrix_integral open MeasureTheory Metric RybinAI2026.P01
Formal statement
theorem RybinAI2026.P01.surface_integral_two_eq_angle_total (f : Euclidean 2 → ℝ) :
(∫ u : sphere (0 : Euclidean 2) 1, f u.1 ∂surfaceMeasure 2) =
∫ θ in (-Real.pi)..Real.pi,
f (WithLp.toLp 2 ![Real.cos θ, Real.sin θ]) := by
sorrySource
The P01 sphere measure is volume.toSphere. Combining Mathlib's generalized sphere-radial measure-preserving decomposition with planar polar coordinates gives this equality for arbitrary totalized integrals. This stronger form directly supports the directional kernels in the diagonal perpendicular-rank-one restriction of RybinAI2026.P01.matrix_integral_inequality.