SmallChord.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The small-chord contradiction

The scalar estimates imply nonnegative coefficients in two exact identities between the actual chord vectors. Applying the norm triangle inequality to those identities contradicts preservation of the distance between the base point and the opposite endpoint. No convexity or monotonicity property of an abstract auxiliary function is assumed.

theorem OAI.Tingley.smallChord_epsilon_lt_half line 21

Source documentation

The two small-regime estimates and the strict chord imbalance force the radial deficit to be strictly below one half.

theorem smallChord_epsilon_lt_half {A B d ε : ℝ}
    (hA : 0 < A) (hB : 0 < B) (hAB : A + B < 1) (hd : d ≤ 2)
    (heA : ε ≤ d * A * (1 - B)) (heB : ε ≤ d * B * (1 - A)) :
    ε < 1 / 2 := by
…

theorem OAI.Tingley.smallChord_coefficients line 45

Source documentation

The scalar conclusions needed by the two actual vector identities. The second coefficient is permitted to vanish.

theorem smallChord_coefficients {A B d ε t p r s u : ℝ}
    (hA : 0 < A) (hB : 0 < B) (hAB : A + B < 1)
    (hd : 0 < d) (hd2 : d ≤ 2) (hεt : ε + t = 1)
    (hdr : d = p + r) (hds : d = s + u)
    (hpA : p = d * A) (huB : u = d * B)
    (hAe : A ≤ ε) (hBe : B ≤ ε)
    (heA : ε ≤ d * A * (1 - B)) (heB : ε ≤ d * B * (1 - A)) :
    ε < 1 / 2 ∧ 0 < r * t - p * ε ∧ 0 ≤ s * ε - u * t ∧ p < s := by
…

theorem OAI.Tingley.smallChord_norm_contradiction line 80

Source documentation

Two norm triangle inequalities on the actual chord vectors are incompatible with the chord imbalance and the preserved base-to-endpoint distance.

theorem smallChord_norm_contradiction
    {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y]
    (y v : X) (b w : Y) {t ε p r s u d : ℝ}
    (hεt : ε + t = 1) (hε : 0 < ε) (hd : 0 < d)
    (hp : 0 < p) (hr : 0 < r) (hs : 0 < s) (hu : 0 < u)
    (hdr : d = p + r) (hds : d = s + u) (hps : p < s)
    (hy : ‖y‖ = 1) (hb : ‖b‖ = 1)
    (hx : ‖t • y + p • v‖ = 1) (hfx : ‖t • b + s • w‖ = 1)
    (hα : 0 ≤ r * t - p * ε) (hβ : 0 ≤ s * ε - u * t)
    (hiso : ‖ε • y + r • v‖ = ‖ε • b + u • w‖) : False := by
…

theorem OAI.Tingley.smallChord_contradiction line 134

Source documentation

The small regime contradicts preservation of the actual opposite-endpoint distance. All scalar guards of the norm argument are derived here.

theorem smallChord_contradiction
    {X Y : Type*} [NormedAddCommGroup X] [NormedSpace ℝ X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y]
    (y v : X) (b w : Y) {t ε p r s u d A B : ℝ}
    (ht1 : t < 1) (he : ε = 1 - t)
    (hp : 0 < p) (hr : 0 < r) (hs : 0 < s) (hu : 0 < u)
    (hdr : d = p + r) (hds : d = s + u) (hd2 : d ≤ 2)
    (hA : A = p / d) (hB : B = u / d) (hAB : A + B < 1)
    (hAe : A ≤ ε) (hBe : B ≤ ε)
    (heA : ε ≤ d * A * (1 - B)) (heB : ε ≤ d * B * (1 - A))
    (hy : ‖y‖ = 1) (hb : ‖b‖ = 1)
    (hx : ‖t • y + p • v‖ = 1) (hfx : ‖t • b + s • w‖ = 1)
…