Intervals.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Counting integers in open intervals; Integral residue classes of theta exponents

theorem OAI.Nagata.W02.card_le_max_sub_min_add_one line 22
Source documentation
A nonempty finite set of integers occupies at least card - 1 units.
```
theorem card_le_max_sub_min_add_one (s : Finset ℤ) (hs : s.Nonempty) :
    (s.card : ℤ) ≤ s.max' hs - s.min' hs + 1 := by
…
```
theorem OAI.Nagata.W02.card_le_interval_length_add_one line 36
Source documentation
A finite set of integers in a nonempty real interval has cardinality at most the interval length plus one. No alignment assumption is needed.
```
theorem card_le_interval_length_add_one (s : Finset ℤ) (a b : ℝ)
    (hab : a ≤ b) (h : ∀ k ∈ s, a ≤ (k : ℝ) ∧ (k : ℝ) ≤ b) :
    (s.card : ℝ) ≤ b - a + 1 := by
…
```
theorem OAI.Nagata.W02.card_le_of_interval_length_lt line 52
Source documentation
If the interval length is strictly less than an integer m, at most m integer positions can occur. This includes empty and singleton rows.
```
theorem card_le_of_interval_length_lt (s : Finset ℤ) (a b : ℝ) (m : ℕ)
    (hab : a ≤ b) (h : ∀ k ∈ s, a ≤ (k : ℝ) ∧ (k : ℝ) ≤ b)
    (hlen : b - a < (m : ℝ)) : s.card ≤ m := by
…
```

theorem OAI.Nagata.W02.sub_one_le_interval_length line 63

Source documentation

At least t integer positions force interval length at least t - 1.

theorem sub_one_le_interval_length (s : Finset ℤ) (a b : ℝ) (t : ℕ)
    (hab : a ≤ b) (h : ∀ k ∈ s, a ≤ (k : ℝ) ∧ (k : ℝ) ≤ b)
    (ht : t ≤ s.card) : (t : ℝ) - 1 ≤ b - a := by
…

theorem OAI.Nagata.W02.card_le_of_interval_length_add_one_le line 72

Source documentation

The translation-independent bound with the spare endpoint absorbed by a unit margin, as in the height count of Lemma integer-rows.

theorem card_le_of_interval_length_add_one_le (s : Finset ℤ) (a b : ℝ) (M : ℕ)
    (hab : a ≤ b) (h : ∀ k ∈ s, a ≤ (k : ℝ) ∧ (k : ℝ) ≤ b)
    (hlen : b - a + 1 ≤ (M : ℝ)) : s.card ≤ M := by
…

theorem OAI.Nagata.W02.card_le_of_open_interval_length_le line 79

Source documentation

Open endpoints permit a non-strict bound on the interval length.

theorem card_le_of_open_interval_length_le (s : Finset ℤ) (a b : ℝ) (m : ℕ)
    (h : ∀ k ∈ s, a < (k : ℝ) ∧ (k : ℝ) < b)
    (hlen : b - a ≤ (m : ℝ)) : s.card ≤ m := by
…

def OAI.Nagata.W09.thetaIndices line 109
Source documentation
The consecutive integers used to index a theta basis.
```
noncomputable def thetaIndices (U : ℝ) (n : ℤ) : Finset ℤ :=
…
```

theorem OAI.Nagata.W09.mem_thetaIndices_iff line 113

Source documentation

For a nonintegral left endpoint, these are exactly the integers in (U,U+n).

theorem mem_thetaIndices_iff {U : ℝ} {n K : ℤ}
    (hU : U ∉ Set.range (Int.cast : ℤ → ℝ)) :
    K ∈ thetaIndices U n ↔ U < (K : ℝ) ∧ (K : ℝ) < U + (n : ℝ) := by
…

Mentions: OAI.Nagata.W09.thetaIndices

theorem OAI.Nagata.W09.card_thetaIndices line 131
Source documentation
An interval with integral positive length has that many integer indices.
```
theorem card_thetaIndices (U : ℝ) (n : ℤ) :
    (thetaIndices U n).card = n.toNat := by
…
```
Mentions: OAI.Nagata.W09.thetaIndices
theorem OAI.Nagata.W09.thetaIndices_residue_injective line 144
Source documentation
Modulo the interval length, two of the chosen consecutive integers cannot agree.
```
theorem thetaIndices_residue_injective {U : ℝ} {n a b : ℤ}
    (ha : a ∈ thetaIndices U n) (hb : b ∈ thetaIndices U n)
    (hab : a % n = b % n) : a = b := by
…
```
Mentions: OAI.Nagata.W09.thetaIndices
theorem OAI.Nagata.W09.exists_thetaIndex_modEq line 160
Source documentation
Every integer residue is represented by one of the chosen indices.
```
theorem exists_thetaIndex_modEq (U : ℝ) {n : ℤ} (hn : 0 < n) (z : ℤ) :
    ∃ K ∈ thetaIndices U n, K % n = z % n := by
…
```
Mentions: OAI.Nagata.W09.thetaIndices
theorem OAI.Nagata.W09.existsUnique_thetaIndex_modEq line 176
Source documentation
Exactly one index represents each residue class; no analytic hypotheses are used.
```
theorem existsUnique_thetaIndex_modEq (U : ℝ) {n : ℤ} (hn : 0 < n) (z : ℤ) :
    ∃! K : ℤ, K ∈ thetaIndices U n ∧ K % n = z % n := by
…
```
Mentions: OAI.Nagata.W09.thetaIndices

theorem OAI.Nagata.W09.existsUnique_integer_in_open_interval_modEq line 184

Source documentation

Source-form statement of existence and uniqueness in the open real interval.

theorem existsUnique_integer_in_open_interval_modEq {U : ℝ} {n : ℤ}
    (hn : 0 < n) (hU : U ∉ Set.range (Int.cast : ℤ → ℝ)) (z : ℤ) :
    ∃! K : ℤ, (U < (K : ℝ) ∧ (K : ℝ) < U + (n : ℝ)) ∧ K % n = z % n := by
…