Isolation of the six-point endpoint

This file encodes the two polynomial equations in centered coordinates. All numbers in the preconditioner are rational, and the coefficient-norm estimates are checked by the kernel.

def LeanPool.Besicovitch.DenseEndpoint.scaledS : DenseBivariatePolynomial

The centered half-coordinate as a transparent dense polynomial.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Besicovitch.DenseEndpoint.scaledB : DenseBivariatePolynomial

The centered distance coordinate as a transparent dense polynomial.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Besicovitch.DenseEndpoint.balance : DenseBivariatePolynomial

The cleared balance polynomial in transparent dense form.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Besicovitch.DenseEndpoint.gram : DenseBivariatePolynomial

The cleared Gram polynomial in transparent dense form.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Besicovitch.DenseEndpoint.fixedMap : Fin 2 → DenseBivariatePolynomial

The preconditioned fixed-point map in transparent dense form.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Besicovitch.endpointMapPolynomial_coefficientL1Norm_lt_one (i : Fin 2) : (DenseEndpoint.fixedMap i).coefficientL1Norm < 1

theorem LeanPool.Besicovitch.endpointMapPolynomial_derivative_coefficientL1Norm_lt (i : Fin 2) : (DenseEndpoint.fixedMap i).derivFirst.coefficientL1Norm + (DenseEndpoint.fixedMap i).derivSecond.coefficientL1Norm < 1 / 10 ^ 9

@[reducible, inline]

abbrev LeanPool.Besicovitch.EndpointCertificateSpace : Type

The two normalized coordinates used by the endpoint certificate.

Equations

• LeanPool.Besicovitch.EndpointCertificateSpace = (Fin 2 → ℝ)

noncomputable def LeanPool.Besicovitch.endpointCertificateSystem (x : EndpointCertificateSpace) : EndpointCertificateSpace

The cleared endpoint equations evaluated in normalized coordinates.

Equations

• LeanPool.Besicovitch.endpointCertificateSystem x = ![LeanPool.Besicovitch.DenseEndpoint.balance.eval (x 0) (x 1), LeanPool.Besicovitch.DenseEndpoint.gram.eval (x 0) (x 1)]

noncomputable def LeanPool.Besicovitch.endpointCertificateMap (x : EndpointCertificateSpace) : EndpointCertificateSpace

The preconditioned endpoint fixed-point map in normalized coordinates.

Equations

• LeanPool.Besicovitch.endpointCertificateMap x i = (LeanPool.Besicovitch.DenseEndpoint.fixedMap i).eval (x 0) (x 1)

def LeanPool.Besicovitch.endpointCertificateBox : Set EndpointCertificateSpace

The closed unit box in the normalized coordinates.

Equations

• LeanPool.Besicovitch.endpointCertificateBox = Metric.closedBall 0 1

noncomputable def LeanPool.Besicovitch.endpointCertificateS (u : EndpointCertificateSpace) : ℝ

Decode the normalized first coordinate into the half-coordinate s.

Equations

• LeanPool.Besicovitch.endpointCertificateS u = 6933064218259049 / 10 ^ 16 + 1 / 10 ^ 16 * u 0

noncomputable def LeanPool.Besicovitch.endpointCertificateB (u : EndpointCertificateSpace) : ℝ

Decode the normalized second coordinate into the distance coordinate B.

Equations

• LeanPool.Besicovitch.endpointCertificateB u = 5747488323603321 / (2 * 10 ^ 15) + 3 / (2 * 10 ^ 15) * u 1

noncomputable def LeanPool.Besicovitch.endpointBalanceCleared (s B : ℝ) : ℝ

The endpoint balance residual with its denominator cleared in half-coordinates.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Besicovitch.endpointGramCleared (s B : ℝ) : ℝ

The endpoint Gram residual with its denominator cleared in half-coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Besicovitch.DenseEndpoint.eval_scaledS (u : EndpointCertificateSpace) : scaledS.eval (u 0) (u 1) = endpointCertificateS u

theorem LeanPool.Besicovitch.DenseEndpoint.eval_scaledB (u : EndpointCertificateSpace) : scaledB.eval (u 0) (u 1) = endpointCertificateB u

theorem LeanPool.Besicovitch.DenseEndpoint.eval_balance (u : EndpointCertificateSpace) : balance.eval (u 0) (u 1) = endpointBalanceCleared (endpointCertificateS u) (endpointCertificateB u)

theorem LeanPool.Besicovitch.DenseEndpoint.eval_gram (u : EndpointCertificateSpace) : gram.eval (u 0) (u 1) = endpointGramCleared (endpointCertificateS u) (endpointCertificateB u)

theorem LeanPool.Besicovitch.endpointBalanceCleared_eq (s B : ℝ) (hq : 2 * s + 1 ≠ 0) : endpointBalanceCleared s B = (2 * s + 1) ^ 4 * endpointBalanceResidual (2 * s) B

theorem LeanPool.Besicovitch.endpointGramCleared_eq (s B : ℝ) (hq : 2 * s + 1 ≠ 0) : endpointGramCleared s B = 4 * (2 * s + 1) ^ 4 * endpointGramResidual (2 * s) B

theorem LeanPool.Besicovitch.endpointCertificateMap_mapsTo : Set.MapsTo endpointCertificateMap endpointCertificateBox endpointCertificateBox

The exact coefficient enclosure makes the certificate map preserve its unit box.

theorem LeanPool.Besicovitch.endpointCertificateMap_lipschitzOn : LipschitzOnWith (1 / 10 ^ 9) endpointCertificateMap endpointCertificateBox

The normalized fixed-point map is Lipschitz with exact constant 10⁻⁹.

theorem LeanPool.Besicovitch.endpointCertificateMap_contracting : ContractingWith (1 / 10 ^ 9) (Set.MapsTo.restrict endpointCertificateMap endpointCertificateBox endpointCertificateBox endpointCertificateMap_mapsTo)

The normalized fixed-point map is a certified strict contraction.

def LeanPool.Besicovitch.endpointCertificatePreconditioner : EndpointCertificateSpace →ₗ[ℝ] EndpointCertificateSpace

The rational preconditioner as a real linear map.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.Besicovitch.endpointCertificateMap_eq_update (x : EndpointCertificateSpace) : endpointCertificateMap x = x - endpointCertificatePreconditioner (endpointCertificateSystem x)

theorem LeanPool.Besicovitch.endpointCertificatePreconditioner_injective : Function.Injective ⇑endpointCertificatePreconditioner

theorem LeanPool.Besicovitch.existsUnique_endpointCertificate_fixedPoint : ∃! x : EndpointCertificateSpace, x ∈ endpointCertificateBox ∧ Function.IsFixedPt endpointCertificateMap x

The exact contraction certificate isolates a unique normalized fixed point.

theorem LeanPool.Besicovitch.existsUnique_endpointCertificate_zero : ∃! x : EndpointCertificateSpace, x ∈ endpointCertificateBox ∧ endpointCertificateSystem x = 0

The exact certificate isolates a unique zero of the cleared endpoint system.

theorem LeanPool.Besicovitch.exists_isEndpointPolynomialPair : ∃ (c : ℝ) (B : ℝ), IsEndpointPolynomialPair c B

There exists an endpoint polynomial pair in the stated strict rational box.

noncomputable def LeanPool.Besicovitch.endpointCertificateCoordinates (c B : ℝ) : EndpointCertificateSpace

Normalize a pair (c, B) into the centered certificate coordinates.

Equations

• LeanPool.Besicovitch.endpointCertificateCoordinates c B = ![10 ^ 16 * (c / 2 - 6933064218259049 / 10 ^ 16), 2 * 10 ^ 15 / 3 * (B - 5747488323603321 / (2 * 10 ^ 15))]

@[simp]

theorem LeanPool.Besicovitch.endpointCertificateS_coordinates (c B : ℝ) : endpointCertificateS (endpointCertificateCoordinates c B) = c / 2

@[simp]

theorem LeanPool.Besicovitch.endpointCertificateB_coordinates (c B : ℝ) : endpointCertificateB (endpointCertificateCoordinates c B) = B

theorem LeanPool.Besicovitch.existsUnique_isEndpointPolynomialPair : ∃! p : ℝ × ℝ, IsEndpointPolynomialPair p.1 p.2

The signed polynomial endpoint system has exactly one solution in its stated box.