IntegerIterateAmplitude.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DerivedBar.IterateSupport.resolvedModel line 17
theorem OAI.DerivedBar.IterateSupport.tensor_exact_above line 23
Source documentation
A bounded input remains cohomologically bounded after actual derived tensor. The input is resolved by its genuine projective bar total.
```
theorem tensor_exact_above (Z : ChainComplex (ModuleCat.{u} D) ℕ) (m : ℕ)
    (hZ : ∀ i, m < i → Z.ExactAt i) (n : ℕ) (hn : m+g+2 < n) :
    ((tensorTotalFunctor k D X).obj Z).ExactAt n := by
…
```
Mentions: OAI.DerivedBar.tensorTotalFunctor
theorem OAI.DerivedBar.IterateSupport.resolvedModel_exact_above line 37
Source documentation
The actual finite iteration has an explicit finite homological support bound. This bound has a two-degree allowance per step; no optimal upper bound is claimed.
```
theorem resolvedModel_exact_above (r n : ℕ) (hn : r*(g+2) < n) :
    (resolvedModel k D X N r).ExactAt n := by
…
```
Mentions: OAI.DerivedBar.IterateSupport.resolvedModel
def OAI.DerivedBar.IterateSupport.resolvedModelIso line 48
theorem OAI.DerivedBar.IterateSupport.isGE_bound line 57
Source documentation
Actual derived tensor iterates have finite lower cohomological support over any ring with the supplied genuine global projective-dimension bound.
```
theorem isGE_bound (r : ℕ) : (object k D X N r).IsGE (-((r*(g+2) : ℕ) : ℤ)) := by
…
```
Mentions: OAI.DerivedBar.IterateSupport.object
theorem OAI.DerivedBar.IterateSupport.bounded_amplitude line 71