Main

@[reducible, inline]

abbrev HumanVerification.Plane : Type

The real Euclidean plane, with its standard inner product and measure.

Equations

• HumanVerification.Plane = EuclideanSpace ℝ (Fin 2)

structure HumanVerification.ConvexFigure : Type

A nondegenerate compact convex figure in the Euclidean plane.

• carrier : Set Plane

  The set of points belonging to the figure.

• isConvex : Convex ℝ self.carrier
• isCompact : IsCompact self.carrier
• hasNonemptyInterior : (interior self.carrier).Nonempty

def HumanVerification.ConvexFigure.toBody (F : ConvexFigure) : NRR.Geometry.ConvexBody Plane

Convert a public figure to the solid convex-body type used by the proof.

Equations

• F.toBody = { carrier := F.carrier, convex' := ⋯, isCompact' := ⋯, interior_nonempty' := ⋯ }

def HumanVerification.ConvexFigure.ofBody (K : NRR.Geometry.ConvexBody Plane) : ConvexFigure

Present an internal solid convex body as a public figure.

Equations

• HumanVerification.ConvexFigure.ofBody K = { carrier := K.carrier, isConvex := ⋯, isCompact := ⋯, hasNonemptyInterior := ⋯ }

@[simp]

theorem HumanVerification.ConvexFigure.toBody_carrier (F : ConvexFigure) : F.toBody.carrier = F.carrier

@[simp]

theorem HumanVerification.ConvexFigure.ofBody_carrier (K : NRR.Geometry.ConvexBody Plane) : (ofBody K).carrier = K.carrier

@[simp]

theorem HumanVerification.ConvexFigure.ofBody_toBody (F : ConvexFigure) : ofBody F.toBody = F

@[simp]

theorem HumanVerification.ConvexFigure.toBody_ofBody (K : NRR.Geometry.ConvexBody Plane) : (ofBody K).toBody = K

def HumanVerification.ConvexFigure.equivBody : ConvexFigure ≃ NRR.Geometry.ConvexBody Plane

Public figures and internal solid convex bodies carry exactly the same data.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance HumanVerification.ConvexFigure.instConvexFigureModel : NRR.HumanExport.ConvexFigureModel ConvexFigure

The reusable proof-export model induced by the public body conversion.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HumanVerification.ConvexFigure.area (F : ConvexFigure) : ENNReal

Lebesgue area of the figure's carrier.

Equations

• F.area = MeasureTheory.volume F.carrier

noncomputable def HumanVerification.ConvexFigure.perimeter (F : ConvexFigure) : ENNReal

One-dimensional Hausdorff measure of the figure's boundary.

Equations

• F.perimeter = (MeasureTheory.Measure.hausdorffMeasure 1) (frontier F.carrier)

def HumanVerification.IsConvexPartition {n : ℕ} (F : ConvexFigure) (pieces : Fin n → ConvexFigure) : Prop

A finite family covers the figure and has pairwise disjoint interiors.

Equations

• HumanVerification.IsConvexPartition F pieces = (F.carrier = ⋃ (i : Fin n), (pieces i).carrier ∧ ∀ (i j : Fin n), i ≠ j → Disjoint (interior (pieces i).carrier) (interior (pieces j).carrier))

theorem HumanVerification.equalAreaEqualPerimeterPartition (F : ConvexFigure) (n : ℕ) (hn : 0 < n) : ∃ (pieces : Fin n → ConvexFigure), IsConvexPartition F pieces ∧ (∀ (i j : Fin n), (pieces i).area = (pieces j).area) ∧ ∀ (i j : Fin n), (pieces i).perimeter = (pieces j).perimeter

Every nondegenerate compact convex figure can be partitioned into n > 0 compact convex figures having equal areas and equal perimeters.