NRR.ConvexBody — public convex‑body API (unified over the geometry layer)

This module is the public entry point for planar convex bodies. It no longer maintains an independent convex‑body type: everything is a thin wrapper/alias over the implemented geometry layer

NRR.Geometry.ConvexBody (NRR/Geometry/ConvexBody/*)

whose bundled bodies are compact, convex, and solid (nonempty interior) by construction.

Public surface

• NRR.E2 — the Euclidean plane, an alias of Geometry.Plane.
• NRR.Body — planar convex bodies, an alias of Geometry.ConvexBody E2.
• Area API in NRR.Geometry.ConvexBody: area, IsSolid, isSolid, area_nonneg, area_lt_top, and the robust positivity lemma area_pos_of_contains_closedBall.
• NRR.SolidConvexBody — a bundled solid body wrapping Geometry.ConvexBody, with ofConvexBody, coe_ofConvexBody, and the derived positivity area_pos_of_solid (also exposed as area_pos).

Every geometry ConvexBody is already solid, so IsSolid/SolidConvexBody are provided for downstream compatibility rather than as genuine extra data.

@[reducible, inline]

abbrev NRR.E2 : Type

The Euclidean plane ℝ², the ambient space fixed throughout the development. Definitional alias of NRR.Geometry.Plane.

Equations

• NRR.E2 = NRR.Geometry.Plane

@[reducible, inline]

abbrev NRR.Body : Type

Planar convex bodies. Definitional alias of the implemented geometry convex‑body type NRR.Geometry.ConvexBody E2.

Equations

• NRR.Body = NRR.Geometry.ConvexBody NRR.E2

def NRR.Geometry.ConvexBody.toMathlib {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) : _root_.ConvexBody E

The forgetful map from a solid geometry convex body to Mathlib's root ConvexBody, dropping the solidity (nonempty-interior) witness and keeping only compactness, convexity, and nonemptiness. This names the map inducing the Hausdorff-metric topology below.

Equations

• K.toMathlib = { carrier := K.carrier, convex' := ⋯, isCompact' := ⋯, nonempty' := ⋯ }

@[simp]

theorem NRR.Geometry.ConvexBody.toMathlib_carrier {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ConvexBody E) : ↑K.toMathlib = K.carrier

@[instance_reducible]

noncomputable instance instTopologicalSpaceGeometryConvexBody {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] : TopologicalSpace (NRR.Geometry.ConvexBody E)

The Hausdorff‑metric topology on geometry convex bodies, induced from Mathlib's ConvexBody metric via the named forgetful map Geometry.ConvexBody.toMathlib that drops the solidity witness. This lets the public API speak about Hausdorff continuity of body‑valued and body‑indexed functionals.

Equations

• instTopologicalSpaceGeometryConvexBody = TopologicalSpace.induced NRR.Geometry.ConvexBody.toMathlib inferInstance

noncomputable def NRR.Geometry.ConvexBody.area (K : ConvexBody Plane) : ℝ

Area of a planar convex body: the (real‑valued) Lebesgue measure of its carrier.

Equations

• K.area = (MeasureTheory.volume K.carrier).toReal

def NRR.Geometry.ConvexBody.IsSolid (K : ConvexBody Plane) : Prop

Solidity: the body has nonempty interior. Every geometry convex body satisfies this by construction (see isSolid); the predicate is kept for downstream compatibility.

Equations

• K.IsSolid = (interior K.carrier).Nonempty

theorem NRR.Geometry.ConvexBody.isSolid (K : ConvexBody Plane) : K.IsSolid

Every geometry convex body is solid: it has nonempty interior by construction.

theorem NRR.Geometry.ConvexBody.area_lt_top (K : ConvexBody Plane) : MeasureTheory.volume K.carrier < ⊤

The Lebesgue measure of a convex body is finite (its carrier is compact).

theorem NRR.Geometry.ConvexBody.area_nonneg (K : ConvexBody Plane) : 0 ≤ K.area

The area of a convex body is nonnegative.

theorem NRR.Geometry.ConvexBody.area_pos_of_contains_closedBall (K : ConvexBody Plane) {x : Plane} {r : ℝ} (hr : 0 < r) (hball : Metric.closedBall x r ⊆ K.carrier) : 0 < K.area

Robust positivity. If a convex body contains a closed ball of positive radius then it has strictly positive area.

structure NRR.SolidConvexBody : Type

A solid convex body: a bundled Geometry.ConvexBody Geometry.Plane together with the (automatic) solidity witness. This is the input type of the fair‑partition theorem.

• toConvexBody : Geometry.ConvexBody Geometry.Plane

  The underlying convex body.

• isSolid : self.toConvexBody.IsSolid

  The body has nonempty interior.

def NRR.SolidConvexBody.ofConvexBody (K : Geometry.ConvexBody Geometry.Plane) : SolidConvexBody

Bundle any geometry convex body as a SolidConvexBody: geometry bodies are always solid.

Equations

• NRR.SolidConvexBody.ofConvexBody K = { toConvexBody := K, isSolid := ⋯ }

@[simp]

theorem NRR.SolidConvexBody.coe_ofConvexBody (K : Geometry.ConvexBody Geometry.Plane) : (ofConvexBody K).toConvexBody = K

theorem NRR.SolidConvexBody.area_pos_of_solid (K : SolidConvexBody) : 0 < K.toConvexBody.area

A solid convex body has strictly positive area, derived from the interior closed‑ball theorem of the geometry layer (exists_closedBall_subset) and area_pos_of_contains_closedBall.

theorem NRR.SolidConvexBody.area_pos (K : SolidConvexBody) : 0 < K.toConvexBody.area

A solid convex body has strictly positive area. (Alias of area_pos_of_solid.)