QuartetExpansion.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact Mellin expansion of the two-bad quartet term

The pair function is zero at a zero difference or ratio. The extra multiplicative character also kills zero differences, so the full-field convolution and the valid-pair formula agree exactly.

def OAI.Ostmann.fieldBottomPairValue line 21
theorem OAI.Ostmann.fieldBottomPairValue_expansion line 26
def OAI.Ostmann.twoBadQuartetValue line 37
theorem OAI.Ostmann.twoBadQuartetValue_eq_synthesis line 44

theorem OAI.Ostmann.twoBadQuartetValue_parseval line 74

Source documentation

The valid two-bad local average is exactly the Fourier expression already bounded.

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

Mentions: OAI.Ostmann.twoBadQuartetValue, OAI.Ostmann.additiveFourier, OAI.Ostmann.pairAutocorrelation