Planar P01 surface integral as an angle integral
ProvedRybinAI2026.P01.surface_integral_two_eq_angleintegral-inequalitymeasure-theorypolar-coordinatessurface-measure
For the P01 unnormalized surfaceMeasure on the unit circle in Euclidean 2-space, integrating a continuous ambient function equals its angle integral along (cos θ, sin θ) over [-π,π].
Preamble
import Mathlib import Definitions.Def_rybin2026_p01_matrix_integral open Matrix MeasureTheory Metric RybinAI2026.P01
Formal statement
theorem RybinAI2026.P01.surface_integral_two_eq_angle (f : Euclidean 2 → ℝ) (hf : Continuous f) :
(∫ u : sphere (0 : Euclidean 2) 1, f u.1 ∂surfaceMeasure 2) =
∫ θ in (-Real.pi)..Real.pi,
f (WithLp.toLp 2 (fun i : Fin 2 => if i = 0 then Real.cos θ else Real.sin θ)) := by
sorrySource
Source-faithful geometric bridge for RybinAI2026.P01.matrix_integral_inequality_diagonal_perpendicular_rankone. It identifies the dimension-two P01 surface measure, defined as volume.toSphere, with the standard angular parameter measure. Mathlib's pinned-revision generalized polar decomposition MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd and planar polar-coordinate change formula provide the two measure decompositions; this child turns the coordinate-integral target into a one-variable interval calculation.