Documentation

LeanPool.NandakumarRamanaRao.HumanVerification.Transfer

Transfer #

theorem NRR.HumanExport.equalAreaEqualPerimeterPartition_of_cauchyCrofton {α : Type} [ConvexFigureModel α] (hcrofton : HumanVerification.CauchyCroftonStatement) (F : α) (n : ℕ) (hn : 0 < n) :
∃ (pieces : Fin n → α), IsConvexPartition F pieces ∧ (∀ (i j : Fin n), area (pieces i) = area (pieces j)) ∧ ∀ (i j : Fin n), perimeter (pieces i) = perimeter (pieces j)

The AAK theorem transferred to an arbitrary human-facing model once the planar Cauchy--Crofton identity has been established.