Exact endpoint weights

This file defines the geometric quantities and Cramer weights in the weighted endpoint argument. Small exact radical certificates prove the numerical inequalities; the stationarity identities are proved symbolically from Cramer's rule.

noncomputable def LeanPool.Besicovitch.endpointOuterRadius (c B : ℝ) : ℝ

The outer radius b in the endpoint configuration.

Equations

• LeanPool.Besicovitch.endpointOuterRadius c B = (2 * B - 3 * c ^ 2 + 2 * c - 1) / (c + 1)

def LeanPool.Besicovitch.endpointSecondDistance (c B : ℝ) : ℝ

The distance D in the endpoint configuration.

Equations

• LeanPool.Besicovitch.endpointSecondDistance c B = 4 * c ^ 2 - 2 * c - B

noncomputable def LeanPool.Besicovitch.endpointFirstAuxiliaryDistance (B : ℝ) : ℝ

The first auxiliary distance A in the endpoint configuration.

Equations

• LeanPool.Besicovitch.endpointFirstAuxiliaryDistance B = √((B ^ 2 - 1) / 2)

noncomputable def LeanPool.Besicovitch.endpointMixedAuxiliaryDistance (c B : ℝ) : ℝ

The mixed auxiliary distance C in the endpoint configuration.

Equations

• LeanPool.Besicovitch.endpointMixedAuxiliaryDistance c B = √((B ^ 2 + LeanPool.Besicovitch.endpointSecondDistance c B ^ 2) / 2 - c ^ 2)

noncomputable def LeanPool.Besicovitch.endpointUnitAbscissa (B : ℝ) : ℝ

The unit-circle abscissa x in the endpoint configuration.

Equations

• LeanPool.Besicovitch.endpointUnitAbscissa B = (5 - B ^ 2) / 4

noncomputable def LeanPool.Besicovitch.endpointOuterAbscissa (c B : ℝ) : ℝ

The outer-circle abscissa z in the endpoint configuration.

Equations

• LeanPool.Besicovitch.endpointOuterAbscissa c B = (1 + 4 * LeanPool.Besicovitch.endpointOuterRadius c B ^ 2 - LeanPool.Besicovitch.endpointSecondDistance c B ^ 2) / 4

noncomputable def LeanPool.Besicovitch.endpointUnitOrdinate (B : ℝ) : ℝ

The positive unit-circle ordinate y in the endpoint configuration.

Equations

• LeanPool.Besicovitch.endpointUnitOrdinate B = √(1 - LeanPool.Besicovitch.endpointUnitAbscissa B ^ 2)

noncomputable def LeanPool.Besicovitch.endpointOuterOrdinate (c B : ℝ) : ℝ

The negative outer-circle ordinate w in the endpoint configuration.

Equations

• LeanPool.Besicovitch.endpointOuterOrdinate c B = -√(LeanPool.Besicovitch.endpointOuterRadius c B ^ 2 - LeanPool.Besicovitch.endpointOuterAbscissa c B ^ 2)

noncomputable def LeanPool.Besicovitch.endpointChordAbscissa (c B : ℝ) : ℝ

The chord abscissa k for the radial endpoint deformation.

Equations

• LeanPool.Besicovitch.endpointChordAbscissa c B = (1 + LeanPool.Besicovitch.endpointOuterRadius c B ^ 2 - c ^ 2) / 2

noncomputable def LeanPool.Besicovitch.endpointChordOrdinate (c B : ℝ) : ℝ

The positive chord ordinate r for the radial endpoint deformation.

Equations

• LeanPool.Besicovitch.endpointChordOrdinate c B = √(LeanPool.Besicovitch.endpointOuterRadius c B ^ 2 - LeanPool.Besicovitch.endpointChordAbscissa c B ^ 2)

noncomputable def LeanPool.Besicovitch.endpointAngularRate (c B : ℝ) : ℝ

The angular rate rho that keeps the endpoint chord length fixed.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointOuterAbscissaDerivative (c B : ℝ) : ℝ

The derivative z_b of the outer abscissa along the radial deformation.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointSecondDistanceDerivative (c B : ℝ) : ℝ

The derivative D_b of the second distance along the radial deformation.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointMixedDistanceDerivative (c B : ℝ) : ℝ

The derivative C_b of the mixed distance along the radial deformation.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointBaseAngularCoefficient (c B : ℝ) : ℝ

The constant coefficient in the angular stationarity equation.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointLambdaAngularCoefficient (B : ℝ) : ℝ

The coefficient of lambda in the angular stationarity equation.

Equations

• LeanPool.Besicovitch.endpointLambdaAngularCoefficient B = 2 * LeanPool.Besicovitch.endpointUnitOrdinate B / B

noncomputable def LeanPool.Besicovitch.endpointMuAngularCoefficient (c B : ℝ) : ℝ

The coefficient of mu in the angular stationarity equation.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointLambdaRadialCoefficient (c : ℝ) : ℝ

The coefficient of lambda in the radial stationarity equation.

Equations

• LeanPool.Besicovitch.endpointLambdaRadialCoefficient c = -(c + 1) / 2

noncomputable def LeanPool.Besicovitch.endpointMuRadialCoefficient (c B : ℝ) : ℝ

The coefficient of mu in the radial stationarity equation.

Equations

• LeanPool.Besicovitch.endpointMuRadialCoefficient c B = LeanPool.Besicovitch.endpointMixedDistanceDerivative c B - 3 * c

noncomputable def LeanPool.Besicovitch.endpointStationarityDeterminant (c B : ℝ) : ℝ

The determinant of the two endpoint stationarity equations.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointCramerLambda (c B : ℝ) : ℝ

Cramer's first weight for the two endpoint stationarity equations.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointCramerMu (c B : ℝ) : ℝ

Cramer's second weight for the two endpoint stationarity equations.

Equations

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

noncomputable def LeanPool.Besicovitch.endpointLambda : ℝ

The exact positive multiplier of the second failure slack.

Equations

• LeanPool.Besicovitch.endpointLambda = LeanPool.Besicovitch.endpointCramerLambda LeanPool.Besicovitch.cStar LeanPool.Besicovitch.certifiedEndpointPair.2

noncomputable def LeanPool.Besicovitch.endpointMu : ℝ

The exact positive multiplier of the third failure slack.

Equations

• LeanPool.Besicovitch.endpointMu = LeanPool.Besicovitch.endpointCramerMu LeanPool.Besicovitch.cStar LeanPool.Besicovitch.certifiedEndpointPair.2

theorem LeanPool.Besicovitch.endpointLambda_mem_interval : 2 / 25 ≤ endpointLambda ∧ endpointLambda ≤ 1 / 10

The first endpoint weight lies between 0.08 and 0.1.

theorem LeanPool.Besicovitch.endpointMu_mem_interval : 23 / 25 ≤ endpointMu ∧ endpointMu ≤ 47 / 50

The second endpoint weight lies between 0.92 and 0.94.

theorem LeanPool.Besicovitch.endpointLambda_pos : 0 < endpointLambda

The first endpoint weight is positive.

theorem LeanPool.Besicovitch.endpointMu_pos : 0 < endpointMu

The second endpoint weight is positive.

theorem LeanPool.Besicovitch.endpointStationarityDeterminant_ne_zero : endpointStationarityDeterminant cStar certifiedEndpointPair.2 ≠ 0

The endpoint stationarity system has nonzero determinant.

theorem LeanPool.Besicovitch.endpoint_angular_stationarity : endpointBaseAngularCoefficient cStar certifiedEndpointPair.2 + endpointLambda * endpointLambdaAngularCoefficient certifiedEndpointPair.2 + endpointMu * endpointMuAngularCoefficient cStar certifiedEndpointPair.2 = 0

Cramer's endpoint weights satisfy angular stationarity exactly.

theorem LeanPool.Besicovitch.endpoint_radial_stationarity : endpointSecondDistanceDerivative cStar certifiedEndpointPair.2 + endpointLambda * endpointLambdaRadialCoefficient cStar + endpointMu * endpointMuRadialCoefficient cStar certifiedEndpointPair.2 = 0

Cramer's endpoint weights satisfy radial stationarity exactly.

theorem LeanPool.Besicovitch.one_lt_endpoint_weight_penalty_margin : 1 < weightedSecondPenalty cStar endpointLambda endpointMu - (2 + endpointMu)

Radial shrinkage gains more than one unit beyond both Lipschitz losses.

theorem LeanPool.Besicovitch.endpoint_weight_reduction_margin : 2 + endpointMu ≤ weightedSecondPenalty cStar endpointLambda endpointMu

The endpoint weights meet the non-strict hypothesis of radial chord reduction.