MovingRegularDiagonal.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The common Fourier multiplier on equal-product diagonal fibres

def OAI.Ostmann.primeProductTransform line 14
Source documentation
The cofactor formula written in terms of the integer product, so that the order of the current prime list is absent.
```
noncomputable def primeProductTransform (g : ∀ p : ℕ, ZMod p → ℂ)
    (D H : ℕ) (s : ℤ) : ℂ :=
…
```
theorem OAI.Ostmann.primeTuple_image_factors line 18
theorem OAI.Ostmann.movingRegularTransform_eq_primeProduct line 35
Source documentation
Every distinct-prime arrangement has exactly the same transform on a fixed product/frequency fibre. This justifies extracting it before taking the squared modulus of the sum over arrangements.
```
theorem movingRegularTransform_eq_primeProduct {J : Type*} [Fintype J]
    (p : J → ℕ) [∀ j, Fact (p j).Prime] (hinj : Function.Injective p)
    (g : ∀ q : ℕ, ZMod q → ℂ) (D : ℕ) (s : ℤ) :
    movingRegularTransform p (fun j => g (p j)) D s =
      primeProductTransform g D (∏ j, p j) s := by
…
```
Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.primeProductTransform
theorem OAI.Ostmann.movingRegularTransform_order_independent line 49

theorem OAI.Ostmann.diagonal_common_transform line 61

Source documentation

Grouping precedes the absolute value. The transform is constant on each fibre, so its squared modulus is a nonnegative common multiplier.

theorem diagonal_common_transform {A K : Type*} [Fintype A] [Fintype K]
    (key : A → K) (W : A → ℂ) (G : K → ℂ) :
    (∑ a, ∑ b, if key a = key b then
      (W a * G (key a)) * conj (W b * G (key b)) else 0).re =
      ∑ k, ‖G k‖ ^ 2 * ‖groupedCoefficient key W k‖ ^ 2 := by
…

Mentions: OAI.Ostmann.groupedCoefficient

theorem OAI.Ostmann.diagonal_common_transform_drop_giant line 84

Source documentation

The giant factor can be discarded after fibre grouping. The remaining regular multiplier is retained exactly as required in the diagonal norm.

theorem diagonal_common_transform_drop_giant {A K : Type*} [Fintype A] [Fintype K]
    (key : A → K) (W : A → ℂ) (giant regular : K → ℂ)
    (hgiant : ∀ k, ‖giant k‖ ≤ 1) :
    (∑ a, ∑ b, if key a = key b then
      (W a * (giant (key a) * regular (key a))) *
        conj (W b * (giant (key b) * regular (key b))) else 0).re ≤
      ∑ k, ‖regular k‖ ^ 2 * ‖groupedCoefficient key W k‖ ^ 2 := by
…

Mentions: OAI.Ostmann.groupedCoefficient