MovingRestoredMultiplier.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The surviving Fourier factors in the restored compensation coordinates

def OAI.Ostmann.movingRestoredActive line 13
Source documentation
The extracted compensation primes retain their places in every cofactor, but the Cauchy step leaves no Fourier factor at those places.
```
def movingRestoredActive (n r m : ℕ) : MovingRegularSlot n (4 + r) m → Bool :=
…
```
Mentions: OAI.Ostmann.MovingRegularSlot
theorem OAI.Ostmann.movingRestoredActive_compensation line 16
theorem OAI.Ostmann.movingRestoredActive_surviving line 21
theorem OAI.Ostmann.movingRestoredActive_bulk line 27
Source documentation
In particular every protected bulk coordinate remains active.
```
@[simp] theorem movingRestoredActive_bulk (n r m : ℕ) (i : TreeLeafIndex n × Fin m) :
    movingRestoredActive n r m (movingTemplateBulk n (4 + r) m i) = true := by
…
```
Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.movingRestoredActive, OAI.Ostmann.movingTemplateBulk
theorem OAI.Ostmann.movingRestoredActive_inactive_not_bulk line 31
theorem OAI.Ostmann.movingRegularTransform_restored_active line 39
Source documentation
The restored masked transform is exactly the surviving transform, with the same sampled compensation product in its outside denominator.
```
theorem movingRegularTransform_restored_active {A : Type*} (value : A → ℕ)
    (hprime : ∀ a, (value a).Prime) (n r m : ℕ)
    (u : TreeLeafIndex n × Fin 4 → A) (y : MovingRegularSlot n r m → A)
    (g : ∀ q : ℕ, ZMod q → ℂ) (D : ℕ) (s : ℤ) :
    let x := movingRestoreSample n r m u y
…
```
Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingRestoreSample
theorem OAI.Ostmann.naturalRegularMultiplier_restored_active line 97
Source documentation
The arithmetic multiplier with inactive compensation slots gives the same surviving transform, retaining every compensation prime in its denominator.
```
theorem naturalRegularMultiplier_restored_active {A : Type*} (value : A → ℕ)
    (hprime : ∀ a, (value a).Prime) (n r m : ℕ)
    (u : TreeLeafIndex n × Fin 4 → A) (y : MovingRegularSlot n r m → A)
    (g : ∀ q : ℕ, ZMod q → ℂ) (D XL XR : ℕ) (s : ℤ) :
    let x := movingRestoreSample n r m u y
…
```
Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingRestoreSample

theorem OAI.Ostmann.naturalRegularMultiplier_restored_primeProduct line 118

Source documentation

Distinct surviving primes put the same identity in product coordinates.

theorem naturalRegularMultiplier_restored_primeProduct {A : Type*} (value : A → ℕ)
    (hprime : ∀ a, (value a).Prime) (n r m : ℕ)
    (u : TreeLeafIndex n × Fin 4 → A) (y : MovingRegularSlot n r m → A)
    (hy : Function.Injective (value ∘ y))
    (g : ∀ q : ℕ, ZMod q → ℂ) (D XL XR : ℕ) (s : ℤ) :
    let x := movingRestoreSample n r m u y
…

Mentions: OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingRestoreSample