TotalAtomUnits.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The actual unit condition on every current atom at every frequency

def OAI.Ostmann.totalAtomUnitRanges line 12
theorem OAI.Ostmann.totalAtomUnitRanges_iff line 18
Source documentation
A unit product is exactly the original assertion that every current atom is a unit. The dummy interval endpoints play no part in this test.
```
theorem totalAtomUnitRanges_iff {I : Type*} [Fintype I] (role : I → CopyScheduleRole)
    (n : ℕ) (x : CopyScheduleAtoms role n → ℕ) (s : ℤ) :
    (∀ r ∈ totalAtomUnitRanges role n, ((r.atoms.map x).prod).Coprime s.natAbs) ↔
      ∀ i, (x i).Coprime s.natAbs := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.totalAtomUnitRanges
theorem OAI.Ostmann.WordRangeDecoration.wordsBounded_mono line 26
theorem OAI.Ostmann.copyScheduleAtoms_card_le line 32
theorem OAI.Ostmann.totalAtomUnits_count line 39
Source documentation
The complete inherited unit family has at most one test per tree node.
```
theorem totalAtomUnits_count {I V : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (n : ℕ) (words : CopyScheduleAtoms role n → List V) :
    (expandedRootRanges role n words (totalAtomUnitRanges role)).count ≤ 2 ^ (n + 1) - 1 := by
…
```
Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.expandedRootRanges, OAI.Ostmann.totalAtomUnitRanges

theorem OAI.Ostmann.totalAtomUnits_words_bounded line 48

Source documentation

Its product words fit the same concrete bound as the Fourier template.

theorem totalAtomUnits_words_bounded {I V : Type*} [Fintype I]
    (role : I → CopyScheduleRole) (n : ℕ) (words : CopyScheduleAtoms role n → List V)
    (M : ℕ) (hM : 1 ≤ M) (hwords : ∀ i, (words i).length ≤ M) :
    (expandedRootRanges role n words (totalAtomUnitRanges role)).WordsBounded
      (2 * 3 ^ n * Fintype.card I * M + 4) := by
…

Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.expandedRootRanges, OAI.Ostmann.totalAtomUnitRanges