InitialOutsideTransform.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The outside spectator factors in the initial Poisson coefficient

theorem OAI.Ostmann.initial_outside_transform line 13

Source documentation

The outside cofactor units are exactly the ones used by the initial full-tuple Fourier transform.

theorem initial_outside_transform {I : Type*} [Fintype I]
    (q : I → ℕ) [∀ i, Fact (q i).Prime]
    (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ)
    (hDq : ∀ i, (Dq i : ZMod (q i)) = (tupleCofactor q i : ℕ))
    (R : ℕ) (s : ℤ) :
    (∏ i, g i ((s : ZMod (q i)) / ((Dq i : ZMod (q i)) * (R : ZMod (q i))))) =
      movingRegularTransform q g R s := by
…

Mentions: OAI.Ostmann.tupleCofactor, OAI.Ostmann.movingRegularTransform

theorem OAI.Ostmann.normalizedFourierProfile_outside_scale line 28
Source documentation
Rescaling the parameter by the outside product preserves precisely the dR/X argument and hence the square-root normalization in (7.9).
```
theorem normalizedFourierProfile_outside_scale (ψ : ℝ → ℂ) (s X d R : ℝ) :
    normalizedFourierProfile ψ s (R / (X / d)) =
      normalizedFourierProfile ψ s (d * R / X) := by
…
```
Mentions: OAI.Ostmann.normalizedFourierProfile
theorem OAI.Ostmann.movingFourierLeaf_outside_scale line 35