Documentation

LeanPool.Besicovitch.SixPoint.SiblingTriangle

Sibling-pair versus rooted-triangle packings #

This file constructs supports 67 and 76 and proves their one-dimensional routing algebra.

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

The canonical triangle's total radius is its semiperimeter.

source
noncomputable def LeanPool.Besicovitch.redSiblingBlueTrianglePacking (configuration : SixPointConfiguration) {L x : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) :
SixPointPacking configuration

Support 67: the red sibling pair against the canonical blue triangle.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem LeanPool.Besicovitch.redSiblingBlueTrianglePacking_radius_left (configuration : SixPointConfiguration) {L x : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) (hmem : (SixPointColor.red, SixPointLabel.left) ∈ (redSiblingBlueTrianglePacking configuration hLdist hL hx_lower hx_upper hblueLeft hblueRight).support) :
    ↑((redSiblingBlueTrianglePacking configuration hLdist hL hx_lower hx_upper hblueLeft hblueRight).radius ⟨(SixPointColor.red, SixPointLabel.left), hmem⟩) = x

    The left red radius in support 67 is the split variable.

    source
    @[simp]
    theorem LeanPool.Besicovitch.redSiblingBlueTrianglePacking_radius_right (configuration : SixPointConfiguration) {L x : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) (hmem : (SixPointColor.red, SixPointLabel.right) ∈ (redSiblingBlueTrianglePacking configuration hLdist hL hx_lower hx_upper hblueLeft hblueRight).support) :
    ↑((redSiblingBlueTrianglePacking configuration hLdist hL hx_lower hx_upper hblueLeft hblueRight).radius ⟨(SixPointColor.red, SixPointLabel.right), hmem⟩) = L - x

    The right red radius in support 67 is the complementary split.

    source
    @[simp]
    theorem LeanPool.Besicovitch.redSiblingBlueTrianglePacking_radius_blue (configuration : SixPointConfiguration) {L x : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) (label : SixPointLabel) (hmem : (SixPointColor.blue, label) ∈ (redSiblingBlueTrianglePacking configuration hLdist hL hx_lower hx_upper hblueLeft hblueRight).support) :
    ↑((redSiblingBlueTrianglePacking configuration hLdist hL hx_lower hx_upper hblueLeft hblueRight).radius ⟨(SixPointColor.blue, label), hmem⟩) = canonicalTriangleRadius (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) label

    Blue radii in support 67 are the canonical triangle radii.

    source
    theorem LeanPool.Besicovitch.redSiblingBlueTrianglePacking_totalRadius (configuration : SixPointConfiguration) {L x : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hL : 1 ≤ L) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) :
    (redSiblingBlueTrianglePacking configuration hLdist hL hx_lower hx_upper hblueLeft hblueRight).totalRadius = L + (dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) + dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) + dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right)) / 2

    The total radius of support 67 is the sibling length plus blue semiperimeter.

    source
    noncomputable def LeanPool.Besicovitch.blueSiblingRedTrianglePacking (configuration : SixPointConfiguration) {M y : ℝ} (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hM : 1 ≤ M) (hy_lower : M - 1 ≤ y) (hy_upper : y ≤ 1) (hredLeft : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) ≤ 1) (hredRight : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) ≤ 1) :
    SixPointPacking configuration

    Support 76: the blue sibling pair against the canonical red triangle.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LeanPool.Besicovitch.blueSiblingRedTrianglePacking_totalRadius (configuration : SixPointConfiguration) {M y : ℝ} (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hM : 1 ≤ M) (hy_lower : M - 1 ≤ y) (hy_upper : y ≤ 1) (hredLeft : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) ≤ 1) (hredRight : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) ≤ 1) :
      (blueSiblingRedTrianglePacking configuration hMdist hM hy_lower hy_upper hredLeft hredRight).totalRadius = M + (dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) + dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) + dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right)) / 2

      The total radius of support 76 is the sibling length plus red semiperimeter.

      source
      noncomputable def LeanPool.Besicovitch.redSiblingBlueTriangleReach (configuration : SixPointConfiguration) (redLabel blueLabel : SixPointLabel) :
      ℝ

      Cross reach from a red point to a blue point carrying its canonical radius.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def LeanPool.Besicovitch.blueSiblingRedTriangleReach (configuration : SixPointConfiguration) (blueLabel redLabel : SixPointLabel) :
        ℝ

        Cross reach from a blue point to a red point carrying its canonical radius.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def LeanPool.Besicovitch.triangleMaximum (value : SixPointLabel → ℝ) :
          ℝ

          The largest of three labelled real values.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem LeanPool.Besicovitch.le_triangleMaximum (value : SixPointLabel → ℝ) (label : SixPointLabel) :
            value label ≤ triangleMaximum value

            Every labelled value is bounded by its triangle maximum.

            source
            theorem LeanPool.Besicovitch.exists_triangleMaximum_eq (value : SixPointLabel → ℝ) :
            ∃ (label : SixPointLabel), triangleMaximum value = value label

            A triangle maximum is attained at one of its three labels.

            source
            def LeanPool.Besicovitch.siblingTriangleSplitDiameter (L M x : ℝ) (leftReach rightReach : SixPointLabel → ℝ) :
            ℝ

            Diameter of a sibling split against a tangent triangle with fixed cross reaches.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem LeanPool.Besicovitch.redSiblingBlueTrianglePacking_virtualDiameter (configuration : SixPointConfiguration) {L M x : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hL : 1 ≤ L) (hM : 1 ≤ M) (hx_lower : L - 1 ≤ x) (hx_upper : x ≤ 1) (hblueLeft : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.left) ≤ 1) (hblueRight : dist (configuration SixPointColor.blue SixPointLabel.root) (configuration SixPointColor.blue SixPointLabel.right) ≤ 1) :
              (redSiblingBlueTrianglePacking configuration hLdist hL hx_lower hx_upper hblueLeft hblueRight).virtualDiameter = siblingTriangleSplitDiameter L M x (redSiblingBlueTriangleReach configuration SixPointLabel.left) (redSiblingBlueTriangleReach configuration SixPointLabel.right)

              The virtual diameter of support 67 is its explicit one-dimensional diameter.

              source
              theorem LeanPool.Besicovitch.blueSiblingRedTrianglePacking_virtualDiameter (configuration : SixPointConfiguration) {L M y : ℝ} (hLdist : dist (configuration SixPointColor.red SixPointLabel.left) (configuration SixPointColor.red SixPointLabel.right) = L) (hMdist : dist (configuration SixPointColor.blue SixPointLabel.left) (configuration SixPointColor.blue SixPointLabel.right) = M) (hL : 1 ≤ L) (hM : 1 ≤ M) (hy_lower : M - 1 ≤ y) (hy_upper : y ≤ 1) (hredLeft : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.left) ≤ 1) (hredRight : dist (configuration SixPointColor.red SixPointLabel.root) (configuration SixPointColor.red SixPointLabel.right) ≤ 1) :
              (blueSiblingRedTrianglePacking configuration hMdist hM hy_lower hy_upper hredLeft hredRight).virtualDiameter = siblingTriangleSplitDiameter M L y (blueSiblingRedTriangleReach configuration SixPointLabel.left) (blueSiblingRedTriangleReach configuration SixPointLabel.right)

              The virtual diameter of support 76 is its explicit one-dimensional diameter.

              source
              theorem LeanPool.Besicovitch.exists_siblingTriangle_split_iff {L M T : ℝ} {leftReach rightReach : SixPointLabel → ℝ} (hL : L ≤ 2) :
              (∃ (x : ℝ), L - 1 ≤ x ∧ x ≤ 1 ∧ siblingTriangleSplitDiameter L M x leftReach rightReach ≤ T) ↔ 2 * L ≤ T ∧ 2 * M ≤ T ∧ (∀ (label : SixPointLabel), L - 1 + leftReach label ≤ T) ∧ (∀ (label : SixPointLabel), L - 1 + rightReach label ≤ T) ∧ ∀ (leftLabel rightLabel : SixPointLabel), L + leftReach leftLabel + rightReach rightLabel ≤ 2 * T

              Exact threshold form of the one-dimensional sibling-triangle minimax.

              source
              theorem LeanPool.Besicovitch.siblingTriangle_failure_routing {L M T : ℝ} {leftReach rightReach : SixPointLabel → ℝ} (hL : L ≤ 2) (hsameL : 2 * L ≤ T) (hsameM : 2 * M ≤ T) (hfail : ∀ (x : ℝ), L - 1 ≤ x → x ≤ 1 → T < siblingTriangleSplitDiameter L M x leftReach rightReach) :
              (∃ (label : SixPointLabel), T < L - 1 + leftReach label) ∨ (∃ (label : SixPointLabel), T < L - 1 + rightReach label) ∨ ∃ (leftLabel : SixPointLabel) (rightLabel : SixPointLabel), 2 * T < L + leftReach leftLabel + rightReach rightLabel

              If every feasible split fails, an endpoint or balanced cross term exceeds the target.