OAI/NumberTheory/JointDickman/Probability/FiniteKernelOrthogonality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact Fourier representation of the finite equation a-b=jc

  1. theorem OAI.JointDickman.integral_additive_triple line 10
  2. theorem OAI.JointDickman.finiteKernel_orthogonality line 38

    Source documentation

    The finite sum and integral are identical, before any arc is discarded.

    theorem finiteKernel_orthogonality (A B C : Finset ℕ) (u v w : ℕ → ℂ) (j : ℕ) :
    (∫ θ in (0 : ℝ)..1,
      finiteAdditiveSum A u θ * finiteAdditiveSum B v (-θ) *
        finiteAdditiveSum C w (-(j : ℝ)*θ)) =
      ∑ c ∈ C, ∑ b ∈ B, ∑ a ∈ A, if a = b+j*c then u a*v b*w c else 0 := by
…

    Mentions: OAI.JointDickman.finiteAdditiveSum