QuartetParseval.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The exact Parseval reduction for quartet averages

Two independent unit parameters are separated by Mellin Parseval. The remaining difference convolution is diagonalized by additive Parseval. All normalizations are the probability normalizations of Section 6.

def OAI.Ostmann.additiveDifferenceConvolution line 21
theorem OAI.Ostmann.additiveFourier_reflection line 25
theorem OAI.Ostmann.additiveFourier_differenceConvolution line 36
theorem OAI.Ostmann.differenceConvolution_parseval line 46

theorem OAI.Ostmann.mellin_synthesis_parseval line 54

Source documentation

Parseval for coefficients given by an explicit Mellin synthesis.

theorem mellin_synthesis_parseval {p : ℕ} [Fact p.Prime]
    (c : MulChar (ZMod p) ℂ → ℂ) :
    (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ *
      (∑ z : (ZMod p)ˣ, ‖∑ χ : MulChar (ZMod p) ℂ, c χ * χ z‖ ^ 2) =
        ∑ χ : MulChar (ZMod p) ℂ, ‖c χ‖ ^ 2 := by
…

theorem OAI.Ostmann.mellin_product_synthesis_parseval line 65

Source documentation

Two independent held parameters separate both Mellin indices.

theorem mellin_product_synthesis_parseval {p : ℕ} [Fact p.Prime]
    (c : MulChar (ZMod p) ℂ → MulChar (ZMod p) ℂ → ℂ) :
    (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ *
      (∑ z : (ZMod p)ˣ, (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ *
        ∑ t : (ZMod p)ˣ,
          ‖∑ χ : MulChar (ZMod p) ℂ, ∑ ψ : MulChar (ZMod p) ℂ,
            c χ ψ * χ z * ψ t‖ ^ 2) =
      ∑ χ : MulChar (ZMod p) ℂ, ∑ ψ : MulChar (ZMod p) ℂ, ‖c χ ψ‖ ^ 2 := by
…

def OAI.Ostmann.quartetSynthesis line 83

theorem OAI.Ostmann.quartetSynthesis_parseval line 92

Source documentation

Exact reduction to the Fourier sum used for all four quartet orientations.

theorem quartetSynthesis_parseval {p : ℕ} [Fact p.Prime]
    (f g : MulChar (ZMod p) ℂ → ZMod p → ℂ)
    (α β : MulChar (ZMod p) ℂ → MulChar (ZMod p) ℂ → MulChar (ZMod p) ℂ) :
    (p : ℝ)⁻¹ * (∑ y : ZMod p,
      (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ * (∑ z : (ZMod p)ˣ,
        (Fintype.card (ZMod p)ˣ : ℝ)⁻¹ *
          ∑ t : (ZMod p)ˣ, ‖quartetSynthesis f g α β y z t‖ ^ 2)) =
      ∑ χ : MulChar (ZMod p) ℂ, ∑ ψ : MulChar (ZMod p) ℂ, ∑ a : ZMod p,
        ‖additiveFourier (fun d => f χ d * α χ ψ d) a‖ ^ 2 *
          ‖additiveFourier (fun e => g ψ e * β χ ψ e) (-a)‖ ^ 2 := by
…

Mentions: OAI.Ostmann.quartetSynthesis, OAI.Ostmann.additiveFourier