BimoduleDerivedInterval.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BimoduleTotal.intervalDegrees line 12
Source documentation
A finite interval of actual right-complex degrees, including both endpoints.
```
def intervalDegrees (lo hi : ℤ) (i : Fin ((hi-lo).toNat+1)) : ℤ := lo + i.val
```
theorem OAI.LittleFinitistic.BimoduleTotal.intervalDegrees_strictMono line 14
theorem OAI.LittleFinitistic.BimoduleTotal.intervalDegrees_covers line 21
Source documentation
Every degree in the support interval really occurs in the finite total.
```
theorem intervalDegrees_covers (lo hi n : ℤ) (hn : lo ≤ n ∧ n ≤ hi) :
    ∃ i, intervalDegrees lo hi i = n := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.intervalDegrees
abbrev OAI.LittleFinitistic.BimoduleTotal.derivedInterval line 33
Source documentation
The native B-valued derived tensor total on a chosen support interval.
```
abbrev derivedInterval (lo hi : ℤ) :=
…
```
theorem OAI.LittleFinitistic.BimoduleTotal.outside_interval_isZero line 39
Source documentation
Boundedness ensures this finite total contains every nonzero right degree.
```
theorem outside_interval_isZero (lo hi : ℤ)
    (hP : ∀ n, n < lo ∨ hi < n → IsZero (P.X n)) (n : ℤ)
    (hn : ∀ i, intervalDegrees lo hi i ≠ n) : IsZero (P.X n) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.intervalDegrees