Rational tangent bounds for sibling incidences

This file proves the two-point tangent inequality used by the rational cells in the complete sibling-incidence ledger. Its endpoint checks use only rational arithmetic and the certified isolation interval for barC.

theorem LeanPool.Besicovitch.separableQuadratic_le_radial_vertices {a₁ a₂ b₁ b₂ d c t₁ t₂ : ℝ} (ha₁ : 0 ≤ a₁) (ha₂ : 0 ≤ a₂) (ht₁ : t₁ ≤ 1) (ht₂ : t₂ ≤ 1) (hsum : c ≤ t₁ + t₂) : a₁ * t₁ ^ 2 + b₁ * t₁ + a₂ * t₂ ^ 2 + b₂ * t₂ + d ≤ max (a₁ + b₁ + a₂ + b₂ + d) (max (a₁ + b₁ + a₂ * (c - 1) ^ 2 + b₂ * (c - 1) + d) (a₁ * (c - 1) ^ 2 + b₁ * (c - 1) + a₂ + b₂ + d))

A separable convex quadratic on the radial triangle is bounded at its three vertices.

noncomputable def LeanPool.Besicovitch.gramPairValue (c u₁ u₂ g₁ g₂ d₁ d₂ off sigma t₁ t₂ : ℝ) : ℝ

The scalar upper function for a two-point Gram estimate.

Equations

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

noncomputable def LeanPool.Besicovitch.gramPairMaximum (c u₁ u₂ g₁ g₂ d₁ d₂ off sigma : ℝ) : ℝ

The largest radial-vertex value in a two-point Gram estimate.

Equations

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

theorem LeanPool.Besicovitch.gramPairCore_le_vertices {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e x₁ x₂ : E) (c u₁ u₂ g₁ g₂ d₁ d₂ off sigma : ℝ) (he : ‖e‖ = 1) (hx₁ : ‖x₁‖ ≤ 1) (hx₂ : ‖x₂‖ ≤ 1) (hseparation : c ≤ ‖x₁ - x₂‖) (hc : 0 ≤ c) (hu₁ : 0 ≤ u₁) (hu₂ : 0 ≤ u₂) (hg₁ : 0 ≤ g₁) (hg₂ : 0 ≤ g₂) (hsigma : 0 < sigma) : u₁ * ‖x₁‖ ^ 2 + u₂ * ‖x₂‖ ^ 2 - 2 * inner ℝ e (g₁ • x₁ + g₂ • x₂) - d₁ * ‖x₁‖ - d₂ * ‖x₂‖ - off * c ^ 2 ≤ gramPairMaximum c u₁ u₂ g₁ g₂ d₁ d₂ off sigma

A separated pair in the unit ball is controlled by the three radial vertices.

noncomputable def LeanPool.Besicovitch.pairTangentValue (c A₁ A₂ d₁ d₂ rho₁ rho₂ sigma t₁ t₂ : ℝ) : ℝ

The quadratic upper function in the two-point tangent estimate.

Equations

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

noncomputable def LeanPool.Besicovitch.pairTangentMaximum (c A₁ A₂ d₁ d₂ rho₁ rho₂ sigma : ℝ) : ℝ

The largest of the three radial vertex values in the two-point tangent estimate.

Equations

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

theorem LeanPool.Besicovitch.two_mul_crossDistance_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e p w : E) : 2 * ‖e - p - w‖ ≤ ‖e - 2 • p‖ + ‖e - 2 • w‖

Midpoint convexity bounds one cross distance by its two doubled-point distances.

theorem LeanPool.Besicovitch.weightedCrossDistances_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (a₁₁ a₁₂ a₂₁ a₂₂ : ℝ) (ha₁₁ : 0 ≤ a₁₁) (ha₁₂ : 0 ≤ a₁₂) (ha₂₁ : 0 ≤ a₂₁) (ha₂₂ : 0 ≤ a₂₂) : a₁₁ * ‖e - p₁ - w₁‖ + a₁₂ * ‖e - p₁ - w₂‖ + a₂₁ * ‖e - p₂ - w₁‖ + a₂₂ * ‖e - p₂ - w₂‖ ≤ (a₁₁ + a₁₂) / 2 * ‖e - 2 • p₁‖ + (a₂₁ + a₂₂) / 2 * ‖e - 2 • p₂‖ + (a₁₁ + a₂₁) / 2 * ‖e - 2 • w₁‖ + (a₁₂ + a₂₂) / 2 * ‖e - 2 • w₂‖

A nonnegative four-entry cross-distance sum splits into two colorwise sums.

theorem LeanPool.Besicovitch.twoPointTangent_le_vertices {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e x₁ x₂ : E) (c A₁ A₂ d₁ d₂ rho₁ rho₂ sigma : ℝ) (he : ‖e‖ = 1) (hx₁ : ‖x₁‖ ≤ 1) (hx₂ : ‖x₂‖ ≤ 1) (hseparation : c ≤ ‖x₁ - x₂‖) (hc : 0 ≤ c) (hA₁ : 0 ≤ A₁) (hA₂ : 0 ≤ A₂) (hrho₁ : 0 < rho₁) (hrho₂ : 0 < rho₂) (hsigma : 0 < sigma) : A₁ * ‖e - 2 • x₁‖ + A₂ * ‖e - 2 • x₂‖ - d₁ * ‖x₁‖ - d₂ * ‖x₂‖ ≤ pairTangentMaximum c A₁ A₂ d₁ d₂ rho₁ rho₂ sigma

Rational two-point tangent estimate on two separated points of the unit ball.

theorem LeanPool.Besicovitch.tangentCertificate_e0s1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 29 / 2 * ‖e - p₁ - w₁‖ + 15 / 2 * ‖e - p₂ - w₂‖ - 13 * barC / 2 * ‖p₁‖ - 13 * barC / 2 * ‖p₂‖ - 7 * (barC - 1) / 2 * ‖w₁‖ - 7 * (barC + 1) / 2 * ‖w₂‖ - 7 + 51 / 2 * barC - 34 * barC ^ 2 < 0

The rational tangent separator for the E0/S1 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_e0s2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 3 * ‖e - p₁ - w₁‖ + 3 / 2 * ‖e - p₁ - w₂‖ + 3 / 2 * ‖e - p₂ - w₁‖ + ‖e - p₂ - w₂‖ - 3 * barC / 2 * ‖p₁‖ - 3 * barC / 2 * ‖p₂‖ - (barC - 1) * ‖w₁‖ - (barC + 1) * ‖w₂‖ - 2 + 8 * barC - 23 / 2 * barC ^ 2 < 0

The rational tangent separator for the E0/S2 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_e0s3 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 46 * ‖e - p₁ - w₁‖ + 27 * ‖e - p₂ - w₁‖ + 32 * ‖e - p₂ - w₂‖ - 27 * (barC + 1) * ‖p₁‖ - 27 * (barC - 1) * ‖p₂‖ - 41 * (barC - 1) / 2 * ‖w₁‖ - 41 * (barC + 1) / 2 * ‖w₂‖ - 41 + 251 / 2 * barC - 325 / 2 * barC ^ 2 < 0

The rational tangent separator for the E0/S3 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_e1s1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 7 * ‖e - p₁ - w₁‖ + 7 * ‖e - p₁ - w₂‖ + 7 * ‖e - p₂ - w₂‖ - 6 * barC * ‖p₁‖ - 6 * barC * ‖p₂‖ - 7 * (barC + 1) / 2 * ‖w₁‖ - 7 * (barC - 1) / 2 * ‖w₂‖ - 7 + 49 / 2 * barC - 65 / 2 * barC ^ 2 < 0

The rational tangent separator for the E1/S1 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_e1s3 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 3 * ‖e - p₁ - w₁‖ + 11 * ‖e - p₁ - w₂‖ + 8 * ‖e - p₂ - w₁‖ + 11 * ‖e - p₂ - w₂‖ - 8 * (barC + 1) * ‖p₁‖ - 8 * (barC - 1) * ‖p₂‖ - 11 * (barC + 1) / 2 * ‖w₁‖ - 11 * (barC - 1) / 2 * ‖w₂‖ - 11 + 77 / 2 * barC - 105 / 2 * barC ^ 2 < 0

The rational tangent separator for the E1/S3 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_s1s1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 13 * ‖e - p₁ - w₁‖ + 13 * ‖e - p₂ - w₂‖ - 6 * barC * ‖p₁‖ - 6 * barC * ‖p₂‖ - 6 * barC * ‖w₁‖ - 6 * barC * ‖w₂‖ + 26 * barC - 40 * barC ^ 2 < 0

The rational tangent separator for the S1/S1 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_s2s2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : ‖e - p₁ - w₁‖ + 8 * ‖e - p₁ - w₂‖ + 8 * ‖e - p₂ - w₁‖ + ‖e - p₂ - w₂‖ - 4 * barC * ‖p₁‖ - 4 * barC * ‖p₂‖ - 4 * barC * ‖w₁‖ - 4 * barC * ‖w₂‖ + 18 * barC - 28 * barC ^ 2 < 0

The rational tangent separator for the S2/S2 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_e1s2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 13 / 2 * ‖e - p₁ - w₂‖ + 7 / 2 * ‖e - p₂ - w₁‖ - 7 * barC / 2 * ‖p₁‖ - 7 * barC / 2 * ‖p₂‖ - 3 * (barC + 1) / 2 * ‖w₁‖ - 3 * (barC - 1) / 2 * ‖w₂‖ - 3 + 23 / 2 * barC - 15 * barC ^ 2 < 0

The rational tangent separator for the E1/S2 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_s0s1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 7 / 2 * ‖e - p₁ - w₁‖ + ‖e - p₂ - w₁‖ + 5 / 2 * ‖e - p₂ - w₂‖ - 5 * barC / 2 * ‖p₁‖ - 5 * barC / 2 * ‖p₂‖ - (barC - 1) * ‖w₁‖ - (barC + 1) * ‖w₂‖ + 7 * barC - 21 / 2 * barC ^ 2 < 0

The rational tangent separator for the S0/S1 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_s0s2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : ‖e - p₁ - w₁‖ + 5 / 2 * ‖e - p₁ - w₂‖ + 7 / 2 * ‖e - p₂ - w₁‖ - 5 * barC / 2 * ‖p₁‖ - 5 * barC / 2 * ‖p₂‖ - (barC - 1) * ‖w₁‖ - (barC + 1) * ‖w₂‖ + 7 * barC - 21 / 2 * barC ^ 2 < 0

The rational tangent separator for the S0/S2 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_s1s2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : ‖e - p₁ - w₁‖ + 5 / 2 * ‖e - p₁ - w₂‖ + 5 / 2 * ‖e - p₂ - w₁‖ + ‖e - p₂ - w₂‖ - 5 * barC / 2 * ‖p₁‖ - 5 * barC / 2 * ‖p₂‖ - barC * ‖w₁‖ - barC * ‖w₂‖ + 7 * barC - 21 / 2 * barC ^ 2 < 0

The rational tangent separator for the S1/S2 incidence representative.

theorem LeanPool.Besicovitch.tangentCertificate_adjacentFirst {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 11 / 4 * ‖e - p₁ - w₁‖ + 7 / 4 * ‖e - p₁ - w₂‖ + ‖e - p₂ - w₂‖ - 7 * (barC - 1) / 8 * ‖p₁‖ - 7 * (barC + 1) / 8 * ‖p₂‖ - 7 * (barC - 1) / 8 * ‖w₁‖ - 7 * (barC + 1) / 8 * ‖w₂‖ - 7 / 2 + 29 / 4 * barC - 37 / 4 * barC ^ 2 < 0

The rational tangent separator for the first adjacent endpoint orbit.

theorem LeanPool.Besicovitch.tangentCertificate_adjacentSecond {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (e p₁ p₂ w₁ w₂ : E) (he : ‖e‖ = 1) (hp₁ : ‖p₁‖ ≤ 1) (hp₂ : ‖p₂‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hw₂ : ‖w₂‖ ≤ 1) (hpsep : barC ≤ ‖p₁ - p₂‖) (hwsep : barC ≤ ‖w₁ - w₂‖) : 11 / 4 * ‖e - p₁ - w₁‖ + 7 / 4 * ‖e - p₂ - w₁‖ + ‖e - p₂ - w₂‖ - 7 * (barC + 1) / 8 * ‖p₁‖ - 7 * (barC - 1) / 8 * ‖p₂‖ - 7 * (barC - 1) / 8 * ‖w₁‖ - 7 * (barC + 1) / 8 * ‖w₂‖ - 7 / 2 + 29 / 4 * barC - 37 / 4 * barC ^ 2 < 0

The rational tangent separator for the second adjacent endpoint orbit.