ExponentSets.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Finite exponent sets for theta coefficient spaces

def OAI.Nagata.FiniteExponents.openIntegerInterval line 20
Source documentation
Every integer strictly between two real endpoints, including integral endpoints.
```
noncomputable def openIntegerInterval (U V : ℝ) : Finset ℤ :=
…
```
theorem OAI.Nagata.FiniteExponents.mem_openIntegerInterval line 23
def OAI.Nagata.FiniteExponents.commonDegree line 28
Source documentation
Common degree of the first coefficient blocks.
```
def commonDegree (d m : ℤ) : ℤ := 3 * (d - 3 * m)
```
def OAI.Nagata.FiniteExponents.sourceDegree line 31
Source documentation
Source degree in a second coefficient block.
```
def sourceDegree (d j : ℤ) : ℤ := 3 * (d - 3 * j)
```
def OAI.Nagata.FiniteExponents.firstLower line 34
Source documentation
The first branch's lower interval endpoint.
```
noncomputable def firstLower (d m j : ℤ) (a Δ : ℝ) : ℝ :=
…
```
def OAI.Nagata.FiniteExponents.secondLower line 38
Source documentation
The second branch's lower interval endpoint.
```
noncomputable def secondLower (d j : ℤ) (a Δ : ℝ) : ℝ :=
…
```
def OAI.Nagata.FiniteExponents.liftRow line 42
Source documentation
Lift a finite set of second coordinates to one fixed first coordinate.
```
def liftRow (j : ℤ) (s : Finset ℤ) : Finset (ℤ × ℤ) :=
…
```
theorem OAI.Nagata.FiniteExponents.mem_liftRow line 45
def OAI.Nagata.FiniteExponents.exponentSet line 58
Source documentation
The complete finite exponent set: positive first blocks, positive-degree second blocks, and the possible single degree-zero block.
```
noncomputable def exponentSet (d m : ℤ) (a Δ : ℝ) : Finset (ℤ × ℤ) :=
…
```

theorem OAI.Nagata.FiniteExponents.mem_exponentSet_iff line 70

Source documentation

Source-faithful membership, using integer floor division for u₀.

theorem mem_exponentSet_iff {d m j K : ℤ} {a Δ : ℝ} :
    (j, K) ∈ exponentSet d m a Δ ↔
      (0 ≤ j ∧ j ≤ m ∧ firstLower d m j a Δ < (K : ℝ) ∧
        (K : ℝ) < firstLower d m j a Δ + (commonDegree d m : ℝ)) ∨
      (m < j ∧ j ≤ d / 3 ∧ 0 < d - 3 * j ∧
        secondLower d j a Δ < (K : ℝ) ∧
        (K : ℝ) < secondLower d j a Δ + (sourceDegree d j : ℝ)) ∨
      (m < j ∧ j ≤ d / 3 ∧ d - 3 * j = 0 ∧ K = 0) := by
…

Mentions: OAI.Nagata.FiniteExponents.exponentSet, OAI.Nagata.FiniteExponents.firstLower, OAI.Nagata.FiniteExponents.commonDegree, OAI.Nagata.FiniteExponents.secondLower, OAI.Nagata.FiniteExponents.sourceDegree

theorem OAI.Nagata.FiniteExponents.integer_degree_bound line 104
Source documentation
The integer floor bound is exactly the real bound used by the enclosure.
```
theorem integer_degree_bound (d j : ℤ) :
    j ≤ d / 3 ↔ (j : ℝ) ≤ (d : ℝ) / 3 := by
…
```
theorem OAI.Nagata.FiniteExponents.mem_exponentSet_iff_raw line 115
theorem OAI.Nagata.FiniteExponents.degree_zero_mem line 133
Source documentation
The source's degree-zero block is retained in the actual finite set.
```
theorem degree_zero_mem {d m j : ℤ} {a Δ : ℝ}
    (hjm : m < j) (hz : d - 3 * j = 0) :
    (j, 0) ∈ exponentSet d m a Δ := by
…
```
Mentions: OAI.Nagata.FiniteExponents.exponentSet
theorem OAI.Nagata.FiniteExponents.exponentSet_nonempty line 143
Source documentation
Positive common degree and the manuscript's nonintegrality condition make S nonempty; the construction has not substituted an empty column domain.
```
theorem exponentSet_nonempty {d m : ℤ} {a Δ : ℝ}
    (hm : 0 ≤ m) (hd : 3 * m < d)
    (hU : firstLower d m 0 a Δ ∉ Set.range (Int.cast : ℤ → ℝ)) :
    (exponentSet d m a Δ).Nonempty := by
…
```
Mentions: OAI.Nagata.FiniteExponents.firstLower, OAI.Nagata.FiniteExponents.exponentSet
def OAI.Nagata.FiniteExponents.Column line 165
Source documentation
The actual column type supplied to interpolation is finite by construction.
```
noncomputable def Column (d m : ℤ) (a Δ : ℝ) :=
…
```
instance OAI.Nagata.FiniteExponents.columnFintype line 168
theorem OAI.Nagata.FiniteExponents.openIntegerInterval_eq_thetaIndices line 183
Source documentation
This general endpoint enumeration agrees with the theta indices whenever that lemma's nonintegrality hypothesis holds.
```
theorem openIntegerInterval_eq_thetaIndices (U : ℝ) (n : ℤ)
    (hU : U ∉ Set.range (Int.cast : ℤ → ℝ)) :
    openIntegerInterval U (U + (n : ℝ)) = Nagata.W09.thetaIndices U n := by
…
```
Mentions: OAI.Nagata.FiniteExponents.openIntegerInterval, OAI.Nagata.W09.thetaIndices