NormBands.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.QuantitativeVanDerWaerden.Vec line 19
def OAI.QuantitativeVanDerWaerden.normSq line 21
def OAI.QuantitativeVanDerWaerden.distSq line 23
theorem OAI.QuantitativeVanDerWaerden.normSq_nonneg line 25

theorem OAI.QuantitativeVanDerWaerden.weighted_nonneg_band_sq_dist_lt_one line 30

Source documentation

On either nonnegative ray, squared separation is strictly less than the width of a common half-open quadratic band.

theorem weighted_nonneg_band_sq_dist_lt_one (a C m x y : ℝ)
    (ha : 0 ≤ a) (hx : 0 ≤ x) (hy : 0 ≤ y)
    (hxb : m ≤ a * x ^ 2 + C ∧ a * x ^ 2 + C < m + 1)
    (hyb : m ≤ a * y ^ 2 + C ∧ a * y ^ 2 + C < m + 1) :
    a * (x - y) ^ 2 < 1 := by
…

theorem OAI.QuantitativeVanDerWaerden.weighted_scalar_band_card_le_two line 46

Source documentation

Weighted scalar packing, including the zero quadratic coefficient. The parameters may have either sign, and the finite index type is arbitrary.

theorem weighted_scalar_band_card_le_two {ι : Type uIndex} (s : Finset ι)
    (t : ι → ℝ) (a C m : ℝ) (ha : 0 ≤ a)
    (hsep : (s : Set ι).Pairwise fun i j => 1 ≤ a * (t i - t j) ^ 2)
    (hband : ∀ i ∈ s, m ≤ a * (t i) ^ 2 + C ∧
      a * (t i) ^ 2 + C < m + 1) :
    s.card ≤ 2 := by
…

theorem OAI.QuantitativeVanDerWaerden.scalar_band_card_le_two line 89

Source documentation

Unit-separated real parameters in a common scalar squared-norm band.

theorem scalar_band_card_le_two {ι : Type uIndex} (s : Finset ι)
    (t : ι → ℝ) (C m : ℝ)
    (hsep : (s : Set ι).Pairwise fun i j => 1 ≤ |t i - t j|)
    (hband : ∀ i ∈ s, m ≤ (t i) ^ 2 + C ∧ (t i) ^ 2 + C < m + 1) :
    s.card ≤ 2 := by
…

theorem OAI.QuantitativeVanDerWaerden.scalar_band_card_le_four line 103
theorem OAI.QuantitativeVanDerWaerden.distSq_affine line 111
Source documentation
Squared distance on an affine line, without Euclidean projection.
```
theorem distSq_affine {D : ℕ} (A B : Vec D) (u v : ℝ) :
    distSq (fun i => A i + u * B i) (fun i => A i + v * B i) =
      normSq B * (u - v) ^ 2 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Vec, OAI.QuantitativeVanDerWaerden.distSq, OAI.QuantitativeVanDerWaerden.normSq
theorem OAI.QuantitativeVanDerWaerden.normSq_affine line 120
theorem OAI.QuantitativeVanDerWaerden.normSq_affine_complete_square line 132
Source documentation
Completing the scalar quadratic gives the weighted band directly. The constant term need not be assumed positive for the packing lemma.
```
theorem normSq_affine_complete_square {D : ℕ} (A B : Vec D) (t : ℝ)
    (hB : normSq B ≠ 0) :
    normSq (fun i => A i + t * B i) =
      normSq B * (t + (∑ i, A i * B i) / normSq B) ^ 2 +
        (normSq A - (∑ i, A i * B i) ^ 2 / normSq B) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.Vec, OAI.QuantitativeVanDerWaerden.normSq