noncomputable def Frourio.mellinSymbol {m : ℕ} (op : FrourioOperator m) (s : ℂ) : ℂ

Mellin記号の定義（形式的）

Equations

• Frourio.mellinSymbol op s = ∑ i : Fin m, op.α i * ↑(op.χ i).toInt * ↑(op.Λ i) ^ (-s)

def Frourio.satisfiesMomentCondition {m : ℕ} (op : FrourioOperator m) (r : ℕ) : Prop

モーメント条件：設計パラメータが満たすべき条件（複素に埋め込んで定義）

Equations

• One or more equations did not get rendered due to their size.

theorem Frourio.frourio_zero_not_moment0 (op : FrourioOperator 0) : ¬satisfiesMomentCondition op 0

基本的な補題：m=0の場合は退化

theorem Frourio.frourio_one_insufficient (op : FrourioOperator 1) : ¬satisfiesMomentCondition op 2

基本的な補題：m=1は差分として不適切（定数項が消えない）