Documentation

LeanPool.Besicovitch.SixPoint.AlgebraicBasic

Basic properties of the six-point endpoint #

This file records the rational bounds built into IsEndpointPair and the order-theoretic consequences of defining cStar as an infimum. The strict lower bound for sStar requires uniqueness of the isolated first coordinate.

source
noncomputable def LeanPool.Besicovitch.endpointBalanceResidual (c B : ℝ) :
ℝ

The polynomial residual obtained by squaring the endpoint balance equation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def LeanPool.Besicovitch.endpointGramResidual (c B : ℝ) :
    ℝ

    The residual of the endpoint Gram equation.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def LeanPool.Besicovitch.IsEndpointPolynomialPair (c B : ℝ) :
      Prop

      The signed polynomial system used to isolate the exact endpoint pair.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem LeanPool.Besicovitch.IsEndpointPair.c_mem_isolation_box {c B : ℝ} (h : IsEndpointPair c B) :
        13866128436518096 / 10 ^ 16 < c ∧ c < 13866128436518100 / 10 ^ 16

        The first coordinate of an endpoint pair lies in its rational isolation box.

        source
        theorem LeanPool.Besicovitch.IsEndpointPair.second_mem_isolation_box {c B : ℝ} (h : IsEndpointPair c B) :
        2873744161801659 / 10 ^ 15 < B ∧ B < 2873744161801662 / 10 ^ 15

        The second coordinate of an endpoint pair lies in its rational isolation box.

        source
        theorem LeanPool.Besicovitch.IsEndpointPair.radicands_pos {c B : ℝ} (h : IsEndpointPair c B) :
        0 < (B ^ 2 - 1) / 2 ∧ 0 < (B ^ 2 + (4 * c ^ 2 - 2 * c - B) ^ 2) / 2 - c ^ 2

        Both radicands in an endpoint pair are strictly positive.

        source
        theorem LeanPool.Besicovitch.IsEndpointPair.endpointBalanceResidual_eq_zero {c B : ℝ} (h : IsEndpointPair c B) :
        endpointBalanceResidual c B = 0

        The radical balance equation implies its exact polynomial equation.

        source
        theorem LeanPool.Besicovitch.IsEndpointPair.endpointGramResidual_eq_zero {c B : ℝ} (h : IsEndpointPair c B) :
        endpointGramResidual c B = 0

        The Gram equation says exactly that its residual vanishes.

        source
        theorem LeanPool.Besicovitch.IsEndpointPair.isEndpointPolynomialPair {c B : ℝ} (h : IsEndpointPair c B) :
        IsEndpointPolynomialPair c B

        An endpoint pair satisfies the signed polynomial isolation system.

        source
        theorem LeanPool.Besicovitch.isEndpointPair_of_isEndpointPolynomialPair {c B : ℝ} (h : IsEndpointPolynomialPair c B) :
        IsEndpointPair c B

        The sign conditions in the polynomial system undo both squaring steps.

        source
        theorem LeanPool.Besicovitch.endpoint_first_coordinates_bddBelow :
        BddBelow {c : ℝ | ∃ (B : ℝ), IsEndpointPair c B}

        The first coordinates of endpoint pairs have a uniform rational lower bound.

        source
        theorem LeanPool.Besicovitch.c_lower_le_cStar (h : ∃ (c : ℝ) (B : ℝ), IsEndpointPair c B) :
        13866128436518096 / 10 ^ 16 ≤ cStar

        The lower endpoint of the isolation box is a lower bound for cStar.

        source
        theorem LeanPool.Besicovitch.cStar_lt_c_upper (h : ∃ (c : ℝ) (B : ℝ), IsEndpointPair c B) :
        cStar < 13866128436518100 / 10 ^ 16

        If an endpoint pair exists, cStar lies below the upper edge of its box.

        source
        theorem LeanPool.Besicovitch.sStar_mem_closedOpen_isolation_box (h : ∃ (c : ℝ) (B : ℝ), IsEndpointPair c B) :
        6933064218259048 / 10 ^ 16 ≤ sStar ∧ sStar < 6933064218259050 / 10 ^ 16

        Existence of an endpoint pair places sStar in a closed-open rational interval.

        source
        theorem LeanPool.Besicovitch.half_lt_sStar_and_sStar_lt_one (h : ∃ (c : ℝ) (B : ℝ), IsEndpointPair c B) :
        1 / 2 < sStar ∧ sStar < 1

        Existence of an endpoint pair gives the elementary bounds used later.

        source
        theorem LeanPool.Besicovitch.cStar_eq_of_isEndpointPair_of_unique {c B : ℝ} (h : IsEndpointPair c B) (h_unique : ∀ ⦃c' B' : ℝ⦄, IsEndpointPair c' B' → c' = c) :
        cStar = c

        A unique first coordinate of an endpoint pair is the infimum cStar.

        source
        theorem LeanPool.Besicovitch.sStar_eq_of_isEndpointPair_of_unique {c B : ℝ} (h : IsEndpointPair c B) (h_unique : ∀ ⦃c' B' : ℝ⦄, IsEndpointPair c' B' → c' = c) :
        sStar = c / 2

        A uniquely isolated endpoint pair identifies sStar exactly.

        source
        theorem LeanPool.Besicovitch.sStar_mem_isolation_box_of_unique {c B : ℝ} (h : IsEndpointPair c B) (h_unique : ∀ ⦃c' B' : ℝ⦄, IsEndpointPair c' B' → c' = c) :
        6933064218259048 / 10 ^ 16 < sStar ∧ sStar < 6933064218259050 / 10 ^ 16

        Uniqueness upgrades the lower endpoint bound from weak to strict.