ProductMellinParseval.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Parseval for the independent moving coordinates on a cycle

The tensor products of unit characters form an orthogonal basis. This finite identity makes the cycle projection energy a sum of products of squared Mellin coefficients, with its exact probability normalization.

def OAI.Ostmann.productCharacter line 23
theorem OAI.Ostmann.productCharacter_orthogonality line 26

theorem OAI.Ostmann.product_mellin_synthesis_parseval line 44

Source documentation

Probability-normalized Parseval for a finite product of unit groups.

theorem product_mellin_synthesis_parseval {p : ℕ} [Fact p.Prime]
    {I : Type*} [Fintype I] [DecidableEq I]
    (c : (I → MulChar (ZMod p) ℂ) → ℂ) :
    ((Fintype.card (ZMod p)ˣ : ℝ) ^ Fintype.card I)⁻¹ *
      (∑ m : I → (ZMod p)ˣ,
        ‖∑ ρ : I → MulChar (ZMod p) ℂ, c ρ * productCharacter ρ m‖ ^ 2) =
      ∑ ρ : I → MulChar (ZMod p) ℂ, ‖c ρ‖ ^ 2 := by
…

Mentions: OAI.Ostmann.productCharacter

theorem OAI.Ostmann.cycleAverage_product_energy line 86

Source documentation

The projected energy is the sum over the surviving cycle-character tuples.

theorem cycleAverage_product_energy {p : ℕ} [Fact p.Prime]
    {I : Type*} [Fintype I] [DecidableEq I]
    (f : I → (ZMod p)ˣ → ℂ) (sign : I → ℤ) :
    ((Fintype.card (ZMod p)ˣ : ℝ) ^ Fintype.card I)⁻¹ *
      (∑ m : I → (ZMod p)ˣ, ‖cycleAverage sign (fun m => ∏ i : I, f i (m i)) m‖ ^ 2) =
      ∑ ρ : I → MulChar (ZMod p) ℂ,
        if (∏ i : I, (ρ i) ^ sign i) = 1 then
          ∏ i : I, ‖mellinCoefficient (f i) (ρ i)‖ ^ 2 else 0 := by
…

Mentions: OAI.Ostmann.cycleAverage, OAI.Ostmann.mellinCoefficient