UniformMesh.lean`

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QuantitativeVanDerWaerden.UniformMesh.left line 13
Source documentation
The left endpoint of a literal interval in [0,1).
```
def left (n : ℕ) (i : Fin n) : ℝ := (i.val : ℝ) / n
```
def OAI.QuantitativeVanDerWaerden.UniformMesh.right line 16
Source documentation
The upper endpoint is excluded.
```
def right (n : ℕ) (i : Fin n) : ℝ := ((i.val : ℝ) + 1) / n
```
def OAI.QuantitativeVanDerWaerden.UniformMesh.Contains line 18
def OAI.QuantitativeVanDerWaerden.UniformMesh.label line 21
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.label_val line 27
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.left_nonneg line 30
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.right_le_one line 34
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.left_lt_right line 39
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.width_eq line 43
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.label_mem line 49
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.label_mem_iff line 60
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.existsUnique_contains line 75
Source documentation
The literal half-open intervals cover [0,1) exactly once.
```
theorem existsUnique_contains (n : ℕ) (hn : 0 < n) (x : ℝ)
    (hx : 0 ≤ x ∧ x < 1) : ∃! i : Fin n, Contains n i x := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.UniformMesh.Contains
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.label_add_int line 83
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.label_eq_of_integer_difference line 88
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.label_cast_eq_emod line 94
Source documentation
Integer floor modulo n recovers the literal fractional-part label.
```
theorem label_cast_eq_emod (n : ℕ) (hn : 0 < n) (x : ℝ) :
    ((label n hn x).val : ℤ) = ⌊(n : ℝ) * x⌋ % (n : ℤ) := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.UniformMesh.label
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.label_eq_of_floor_eq line 111
def OAI.QuantitativeVanDerWaerden.UniformMesh.liftedEndpoints line 119
Source documentation
Precisely the lifted lattice endpoints lying in a closed target interval.
```
def liftedEndpoints (n : ℕ) (a b : ℝ) : Finset ℤ :=
…
```
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.mem_liftedEndpoints line 122
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.card_liftedEndpoints_le_four line 135
Source documentation
The closed interval may meet both extreme endpoints; hence four, not three.
```
theorem card_liftedEndpoints_le_four (n : ℕ) (hn : 0 < n) (a b : ℝ)
    (hwidth : b - a ≤ 3 / (n : ℝ)) : (liftedEndpoints n a b).card ≤ 4 := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.UniformMesh.liftedEndpoints
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.floor_le_of_signs_eq line 147
theorem OAI.QuantitativeVanDerWaerden.UniformMesh.label_eq_of_signs_eq line 173
Source documentation
Literal-label factorization through finitely many ternary comparisons. No width or counting premise is needed for this determination statement.
```
theorem label_eq_of_signs_eq (n : ℕ) (hn : 0 < n) (a b x y : ℝ)
    (hx : x ∈ Set.Icc a b) (hy : y ∈ Set.Icc a b)
    (hsign : ∀ j ∈ liftedEndpoints n a b,
      ternarySign (x - (j : ℝ) / n) = ternarySign (y - (j : ℝ) / n)) :
    label n hn x = label n hn y := by
…
```
Mentions: OAI.QuantitativeVanDerWaerden.UniformMesh.liftedEndpoints, OAI.QuantitativeVanDerWaerden.ternarySign, OAI.QuantitativeVanDerWaerden.UniformMesh.label