NRR.Geometry.ConvexBody — the angle parameterization of the unit circle

This module sets up a deterministic angle-parameterization of the planar unit circle, to be used as the integration domain for Cauchy's perimeter formula. Instead of introducing a measure on the unit circle (Haar measure, quotient-circle measure, or a measure on a unit-sphere subtype), we parameterize directions by the interval [0, 2π] via the map

θ ↦ (cos θ, sin θ).

Design notes

• The plane is fixed as Plane := EuclideanSpace ℝ (Fin 2). This is definitionally equal to the project's NRR.E2 abbreviation. The local name keeps this module focused on width continuity and uses the standard Euclidean additive, normed, and inner-product instances.
• circleVec θ is built with the Euclidean vector notation !₂[cos θ, sin θ], so its coordinates are circleVec θ 0 = cos θ and circleVec θ 1 = sin θ. Both coordinate projections are exposed as @[simp] lemmas, since later perimeter proofs rewrite through them.
• The width function widthFunction K (from Width.lean) is continuous in the direction (continuous_widthFunction from WidthContinuity.lean); composing with the continuous circleVec and restricting to the compact interval [0, 2π] gives interval integrability.

Import policy

The width-function continuity API and interval-integrability lemmas are imported directly.

@[reducible, inline]

abbrev NRR.Geometry.Plane : Type

The Euclidean plane ℝ². Definitionally equal to NRR.E2; reintroduced here to keep this module independent of the area API.

Equations

• NRR.Geometry.Plane = EuclideanSpace ℝ (Fin 2)

noncomputable def NRR.Geometry.circleVec (θ : ℝ) : Plane

The angle parameterization of the unit circle: circleVec θ = (cos θ, sin θ) as a point of the Euclidean plane.

Equations

• NRR.Geometry.circleVec θ = !₂[Real.cos θ, Real.sin θ]

@[simp]

theorem NRR.Geometry.circleVec_zero_coord (θ : ℝ) : (circleVec θ).ofLp 0 = Real.cos θ

First coordinate of circleVec θ is cos θ.

@[simp]

theorem NRR.Geometry.circleVec_one_coord (θ : ℝ) : (circleVec θ).ofLp 1 = Real.sin θ

Second coordinate of circleVec θ is sin θ.

@[simp]

theorem NRR.Geometry.norm_circleVec (θ : ℝ) : ‖circleVec θ‖ = 1

circleVec θ is a unit vector: ‖circleVec θ‖ = 1.

theorem NRR.Geometry.circleVec_mem_unitSphere (θ : ℝ) : circleVec θ ∈ Metric.sphere 0 1

circleVec θ lies on the unit sphere centered at the origin.

theorem NRR.Geometry.continuous_circleVec : Continuous circleVec

The angle parameterization is continuous.

theorem NRR.Geometry.circleVec_periodic : Function.Periodic circleVec (2 * Real.pi)

The angle parameterization is 2π-periodic.

theorem NRR.Geometry.circleVec_add_pi (θ : ℝ) : circleVec (θ + Real.pi) = -circleVec θ

Antipodal shift: circleVec (θ + π) = - circleVec θ. Useful for width symmetry.

theorem NRR.Geometry.intervalIntegrable_comp_circleVec {f : Plane → ℝ} (hf : Continuous f) : IntervalIntegrable (fun (θ : ℝ) => f (circleVec θ)) MeasureTheory.volume 0 (2 * Real.pi)

Any continuous scalar field on the plane, composed with circleVec, is interval-integrable on [0, 2π].

theorem NRR.Geometry.intervalIntegrable_width_circleVec (K : ConvexBody Plane) : IntervalIntegrable (fun (θ : ℝ) => K.widthFunction (circleVec θ)) MeasureTheory.volume 0 (2 * Real.pi)

The width of a convex body along circleVec is interval-integrable on [0, 2π]; this is the integrand of Cauchy's perimeter formula.