Cauchy–Crofton bridge: basic set-up

This module fixes the two perimeter functionals compared by the bridge theorem:

• hPerimeter K = μH[1] (frontier K), the one-dimensional Hausdorff measure of the topological boundary;
• cPerimeter K = ENNReal.ofReal (perimeter K), the project's Cauchy width-integral perimeter, coerced to ℝ≥0∞.

It records their behaviour under translations and positive dilations and an elementary squeeze lemma in ℝ≥0∞.

@[reducible, inline]

abbrev HumanVerification.CauchyCrofton.Point2 : Type

The Euclidean plane used by the Cauchy–Crofton verification interface.

Equations

• HumanVerification.CauchyCrofton.Point2 = NRR.HumanExport.Plane

@[reducible, inline]

abbrev HumanVerification.CauchyCrofton.Body : Type

Compact convex planar bodies with nonempty interior.

Equations

• HumanVerification.CauchyCrofton.Body = NRR.Geometry.ConvexBody HumanVerification.CauchyCrofton.Point2

noncomputable def HumanVerification.CauchyCrofton.hPerimeter (K : Body) : ENNReal

Hausdorff perimeter: the one-dimensional Hausdorff measure of the topological boundary.

Equations

• HumanVerification.CauchyCrofton.hPerimeter K = (MeasureTheory.Measure.hausdorffMeasure 1) (frontier K.carrier)

noncomputable def HumanVerification.CauchyCrofton.cPerimeter (K : Body) : ENNReal

The project's real-valued Cauchy perimeter, coerced to ℝ≥0∞.

Equations

• HumanVerification.CauchyCrofton.cPerimeter K = ENNReal.ofReal (NRR.Geometry.ConvexBody.perimeter K)

theorem HumanVerification.CauchyCrofton.hPerimeter_def (K : Body) : hPerimeter K = (MeasureTheory.Measure.hausdorffMeasure 1) (frontier K.carrier)

theorem HumanVerification.CauchyCrofton.cPerimeter_ne_top (K : Body) : cPerimeter K ≠ ⊤

theorem HumanVerification.CauchyCrofton.cPerimeter_mono {K L : Body} (hKL : K.carrier ⊆ L.carrier) : cPerimeter K ≤ cPerimeter L

Monotonicity of the Cauchy perimeter.

theorem HumanVerification.CauchyCrofton.cPerimeter_scalePos (K : Body) {r : ℝ} (hr : 0 < r) : cPerimeter (NRR.Geometry.ConvexBody.scalePos K r hr) = ENNReal.ofReal r * cPerimeter K

Dilation law for the Cauchy perimeter.

theorem HumanVerification.CauchyCrofton.cPerimeter_translate (K : Body) (a : Point2) : cPerimeter (NRR.Geometry.ConvexBody.translate K a) = cPerimeter K

Translation invariance of the Cauchy perimeter.

theorem HumanVerification.CauchyCrofton.hPerimeter_scalePos (K : Body) {r : ℝ} (hr : 0 < r) : hPerimeter (NRR.Geometry.ConvexBody.scalePos K r hr) = ENNReal.ofReal r * hPerimeter K

Dilation law for the Hausdorff perimeter.

theorem HumanVerification.CauchyCrofton.hPerimeter_translate (K : Body) (a : Point2) : hPerimeter (NRR.Geometry.ConvexBody.translate K a) = hPerimeter K

Translation invariance of the Hausdorff perimeter.

theorem HumanVerification.CauchyCrofton.eq_of_forall_one_lt_mul {a b : ENNReal} (ha : a ≠ ⊤) (hb : b ≠ ⊤) (hab : ∀ (r : ℝ), 1 < r → a ≤ ENNReal.ofReal r * b) (hba : ∀ (r : ℝ), 1 < r → b ≤ ENNReal.ofReal r * a) : a = b

Squeeze lemma: if a ≤ r * b and b ≤ r * a for every r > 1, then a = b.