Radial reduction for the weighted six-point inequality

This file records the exact weighted score and proves that its two second children may be moved inward until both sibling distances equal the endpoint chord length.

noncomputable def LeanPool.Besicovitch.weightedFirstPenalty (c lambda mu : ℝ) : ℝ

The coefficient penalizing the first child radii in the weighted score.

Equations

• LeanPool.Besicovitch.weightedFirstPenalty c lambda mu = (c - 1) * (lambda / 2 + mu)

noncomputable def LeanPool.Besicovitch.weightedSecondPenalty (c lambda mu : ℝ) : ℝ

The coefficient penalizing the second child radii in the weighted score.

Equations

• LeanPool.Besicovitch.weightedSecondPenalty c lambda mu = (c + 1) * lambda / 2 + 3 * c * mu

noncomputable def LeanPool.Besicovitch.weightedConstantTerm (c lambda mu : ℝ) : ℝ

The constant term in the weighted combination of the three failure slacks.

Equations

• LeanPool.Besicovitch.weightedConstantTerm c lambda mu = 2 * c * (2 * c - 1) + lambda * (3 * c ^ 2 - 3 * c + 2) / 2 + mu * (c ^ 2 - c)

noncomputable def LeanPool.Besicovitch.weightedPairScore {E : Type u_1} [NormedAddCommGroup E] (e : E) (c lambda mu : ℝ) (p₁ p₂ w₁ w₂ : E) : ℝ

The weighted failure score for two ordered sibling pairs relative to a unit root vector.

Equations

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

theorem LeanPool.Besicovitch.exists_norm_sub_smul_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {p q : E} {c : ℝ} (hp : ‖p‖ < c) (hpq : c ≤ ‖p - q‖) : ∃ a ∈ Set.Icc 0 1, ‖p - a • q‖ = c

Scaling a point inward reaches every intermediate distance from another point.

theorem LeanPool.Besicovitch.weightedPairScore_le_smul_second_left {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E) (c lambda mu : ℝ) (p₁ p₂ w₁ w₂ : E) {a : ℝ} (ha_zero : 0 ≤ a) (ha_one : a ≤ 1) (hmu : 0 ≤ mu) (hpenalty : 2 + mu ≤ weightedSecondPenalty c lambda mu) : weightedPairScore e c lambda mu p₁ p₂ w₁ w₂ ≤ weightedPairScore e c lambda mu p₁ (a • p₂) w₁ w₂

Moving the second child of the first pair inward cannot decrease the weighted score.

theorem LeanPool.Besicovitch.weightedPairScore_swap {E : Type u_1} [NormedAddCommGroup E] (e : E) (c lambda mu : ℝ) (p₁ p₂ w₁ w₂ : E) : weightedPairScore e c lambda mu p₁ p₂ w₁ w₂ = weightedPairScore e c lambda mu w₁ w₂ p₁ p₂

The weighted score is symmetric in its two sibling pairs.

theorem LeanPool.Besicovitch.weightedPairScore_le_smul_second_right {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E) (c lambda mu : ℝ) (p₁ p₂ w₁ w₂ : E) {a : ℝ} (ha_zero : 0 ≤ a) (ha_one : a ≤ 1) (hmu : 0 ≤ mu) (hpenalty : 2 + mu ≤ weightedSecondPenalty c lambda mu) : weightedPairScore e c lambda mu p₁ p₂ w₁ w₂ ≤ weightedPairScore e c lambda mu p₁ p₂ w₁ (a • w₂)

Moving the second child of the second pair inward cannot decrease the weighted score.

theorem LeanPool.Besicovitch.exists_weightedPairScore_chord_reduction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (e : E) {c lambda mu : ℝ} {p₁ p₂ w₁ w₂ : E} (hc : 1 < c) (hp₁ : ‖p₁‖ ≤ 1) (hw₁ : ‖w₁‖ ≤ 1) (hp : c ≤ ‖p₁ - p₂‖) (hw : c ≤ ‖w₁ - w₂‖) (hmu : 0 ≤ mu) (hpenalty : 2 + mu ≤ weightedSecondPenalty c lambda mu) : ∃ (p₂' : E) (w₂' : E), ‖p₁ - p₂'‖ = c ∧ ‖w₁ - w₂'‖ = c ∧ ‖p₂'‖ ≤ ‖p₂‖ ∧ ‖w₂'‖ ≤ ‖w₂‖ ∧ weightedPairScore e c lambda mu p₁ p₂ w₁ w₂ ≤ weightedPairScore e c lambda mu p₁ p₂' w₁ w₂'

Both sibling pairs reduce to endpoint-length chords without lowering the weighted score.