Canonical tangent radii for a triangle

The three radii are the half-perimeter differences, indexed by the six-point labels.

noncomputable def LeanPool.Besicovitch.canonicalTriangleRadius {X : Type u_1} [PseudoMetricSpace X] (root left right : X) : SixPointLabel → ℝ

The canonical mutually tangent radii attached to a labelled triangle.

Equations

• LeanPool.Besicovitch.canonicalTriangleRadius root left right LeanPool.Besicovitch.SixPointLabel.root = (dist root left + dist root right - dist left right) / 2
• LeanPool.Besicovitch.canonicalTriangleRadius root left right LeanPool.Besicovitch.SixPointLabel.left = (dist root left + dist left right - dist root right) / 2
• LeanPool.Besicovitch.canonicalTriangleRadius root left right LeanPool.Besicovitch.SixPointLabel.right = (dist root right + dist left right - dist root left) / 2

theorem LeanPool.Besicovitch.canonicalTriangleRadius_root_add_left {X : Type u_1} [PseudoMetricSpace X] (root left right : X) : canonicalTriangleRadius root left right SixPointLabel.root + canonicalTriangleRadius root left right SixPointLabel.left = dist root left

The root and left canonical radii sum to their center distance.

theorem LeanPool.Besicovitch.canonicalTriangleRadius_root_add_right {X : Type u_1} [PseudoMetricSpace X] (root left right : X) : canonicalTriangleRadius root left right SixPointLabel.root + canonicalTriangleRadius root left right SixPointLabel.right = dist root right

The root and right canonical radii sum to their center distance.

theorem LeanPool.Besicovitch.canonicalTriangleRadius_left_add_right {X : Type u_1} [PseudoMetricSpace X] (root left right : X) : canonicalTriangleRadius root left right SixPointLabel.left + canonicalTriangleRadius root left right SixPointLabel.right = dist left right

The left and right canonical radii sum to their center distance.

theorem LeanPool.Besicovitch.canonicalTriangleRadius_nonneg {X : Type u_1} [PseudoMetricSpace X] (root left right : X) (label : SixPointLabel) : 0 ≤ canonicalTriangleRadius root left right label

Every canonical triangle radius is nonnegative.

theorem LeanPool.Besicovitch.canonicalTriangleRadius_root_le_average {X : Type u_1} [PseudoMetricSpace X] (root left right : X) : canonicalTriangleRadius root left right SixPointLabel.root ≤ (dist root left + dist root right) / 2

The root radius is at most the average root-to-child distance.

theorem LeanPool.Besicovitch.canonicalTriangleRadius_left_le_dist {X : Type u_1} [PseudoMetricSpace X] (root left right : X) : canonicalTriangleRadius root left right SixPointLabel.left ≤ dist root left

The left radius is at most the root-to-left distance.

theorem LeanPool.Besicovitch.canonicalTriangleRadius_right_le_dist {X : Type u_1} [PseudoMetricSpace X] (root left right : X) : canonicalTriangleRadius root left right SixPointLabel.right ≤ dist root right

The right radius is at most the root-to-right distance.

theorem LeanPool.Besicovitch.canonicalTriangleRadius_le_one {X : Type u_1} [PseudoMetricSpace X] (root left right : X) (hleft : dist root left ≤ 1) (hright : dist root right ≤ 1) (label : SixPointLabel) : canonicalTriangleRadius root left right label ≤ 1

Unit root-to-child distances place every canonical radius in the unit interval.