structure Frourio.ScaleOperator : Type

スケール変換作用素 U_Λ: f(x) ↦ f(Λx)

• scale : ℝ
• scale_pos : 0 < self.scale

theorem Frourio.ScaleOperator.ext (U V : ScaleOperator) (h : U.scale = V.scale) : U = V

スケール変換作用素の拡張性

theorem Frourio.ScaleOperator.ext_iff {U V : ScaleOperator} : U = V ↔ U.scale = V.scale

noncomputable def Frourio.ScaleOperator.act {α : Type u_1} (U : ScaleOperator) (f : ℝ → α) : ℝ → α

スケール変換作用素の関数への作用

Equations

• U.act f x = f (U.scale * x)

noncomputable def Frourio.ScaleOperator.comp (U V : ScaleOperator) : ScaleOperator

スケール変換の合成

Equations

• U.comp V = { scale := U.scale * V.scale, scale_pos := ⋯ }

noncomputable def Frourio.ScaleOperator.inv (U : ScaleOperator) : ScaleOperator

逆スケール変換

Equations

• U.inv = { scale := U.scale⁻¹, scale_pos := ⋯ }

def Frourio.ScaleOperator.id : ScaleOperator

恒等スケール変換

Equations

• Frourio.ScaleOperator.id = { scale := 1, scale_pos := Frourio.ScaleOperator.id._proof_1 }

theorem Frourio.ScaleOperator.comp_assoc (U V W : ScaleOperator) : (U.comp V).comp W = U.comp (V.comp W)

スケール変換の合成は結合的

theorem Frourio.ScaleOperator.id_comp (U : ScaleOperator) : id.comp U = U

恒等スケール変換は単位元

theorem Frourio.ScaleOperator.comp_id (U : ScaleOperator) : U.comp id = U

恒等スケール変換は右単位元

theorem Frourio.ScaleOperator.inv_comp (U : ScaleOperator) : U.inv.comp U = id

逆スケール変換は左逆元

theorem Frourio.ScaleOperator.comp_inv (U : ScaleOperator) : U.comp U.inv = id

逆スケール変換は右逆元

theorem Frourio.ScaleOperator.act_comp {α : Type u_1} (U V : ScaleOperator) (f : ℝ → α) : U.act (V.act f) = (U.comp V).act f

スケール変換作用の合成則

theorem Frourio.ScaleOperator.id_act {α : Type u_1} (f : ℝ → α) : id.act f = f

恒等スケール変換の作用

theorem Frourio.ScaleOperator.inv_act {α : Type u_1} (U : ScaleOperator) (f : ℝ → α) : U.inv.act (U.act f) = f

逆スケール変換の作用

theorem Frourio.ScaleOperator.act_injective {α : Type u_1} (U : ScaleOperator) : Function.Injective U.act

スケール変換は単射

theorem Frourio.ScaleOperator.act_smul (U : ScaleOperator) (c : ℂ) (f : ℝ → ℂ) : (U.act fun (x : ℝ) => c * f x) = fun (x : ℝ) => c * U.act f x

スケール変換の線形性（スカラー倍）

theorem Frourio.ScaleOperator.act_add (U : ScaleOperator) (f g : ℝ → ℂ) : (U.act fun (x : ℝ) => f x + g x) = fun (x : ℝ) => U.act f x + U.act g x

スケール変換の線形性（加法）

theorem Frourio.ScaleOperator.mellin_scale (U : ScaleOperator) (f : ℝ → ℂ) (x : ℝ) : x > 0 → U.act f x = f (U.scale * x)

スケール変換のMellin変換への作用

theorem Frourio.ScaleOperator.pow_scale (U : ScaleOperator) (n : ℕ) : ∃ (V : ScaleOperator), V.scale = U.scale ^ n ∧ ∀ (f : ℝ → ℂ) (x : ℝ), V.act f x = f (U.scale ^ n * x)

スケール変換の冪乗則

noncomputable def Frourio.ScaleOperator.golden : ScaleOperator

黄金比スケール変換

Equations

• Frourio.ScaleOperator.golden = { scale := Frourio.φ, scale_pos := Frourio.ScaleOperator.golden._proof_1 }

theorem Frourio.ScaleOperator.golden_inv : golden.inv.scale = φ⁻¹

黄金比の逆スケール変換

theorem Frourio.ScaleOperator.comm (U V : ScaleOperator) : U.comp V = V.comp U

スケール変換の交換関係

theorem Frourio.ScaleOperator.square_eq_id_iff (U : ScaleOperator) : U.comp U = id ↔ U.scale = 1

スケール変換の冪等性チェック

structure Frourio.InverseMultOperator : Type

逆数乗算作用素 M_{1/x}: f(x) ↦ f(x)/x

• atZero : ℂ

  原点での振る舞いを指定するフラグ（デフォルトは0）

noncomputable def Frourio.InverseMultOperator.act (M : InverseMultOperator) (f : ℝ → ℂ) : ℝ → ℂ

逆数乗算作用素の関数への作用

Equations

• M.act f x = if x ≠ 0 then f x / ↑x else M.atZero

def Frourio.InverseMultOperator.standard : InverseMultOperator

標準的な逆数乗算作用素（原点で0）

Equations

• Frourio.InverseMultOperator.standard = { }

noncomputable def Frourio.InverseMultOperator.square (M : InverseMultOperator) : InverseMultOperator

逆数乗算作用素の合成則 M_{1/x} ∘ M_{1/x} = M_{1/x²}

Equations

• M.square = M

theorem Frourio.InverseMultOperator.act_eq_div (M : InverseMultOperator) (f : ℝ → ℂ) (x : ℝ) : x ≠ 0 → M.act f x = f x / ↑x

逆数乗算作用素の基本性質

theorem Frourio.InverseMultOperator.act_smul_standard (c : ℂ) (f : ℝ → ℂ) : (standard.act fun (x : ℝ) => c * f x) = fun (x : ℝ) => c * standard.act f x

逆数乗算作用素の線形性（スカラー倍、原点で0の場合）

theorem Frourio.InverseMultOperator.act_add_standard (f g : ℝ → ℂ) : (standard.act fun (x : ℝ) => f x + g x) = fun (x : ℝ) => standard.act f x + standard.act g x

逆数乗算作用素の加法性（原点で0の場合）

structure Frourio.FrourioParams (m : ℕ) : Type

m点Frourio作用素のパラメータ

• α : Fin m → ℂ
• χ : Fin m → Sign
• Λ : Fin m → ℝ
• Λ_pos (i : Fin m) : 0 < self.Λ i

structure Frourio.FrourioOperator (m : ℕ) extends Frourio.FrourioParams m : Type

m点Frourio作用素の定義 Δ^⟨m⟩ = M_{1/x} (Σ_{i=1}^m α_i χ_i U_{Λ_i}) ここではパラメータを束ねた構造として与える。

• α : Fin m → ℂ
• χ : Fin m → Sign
• Λ : Fin m → ℝ
• Λ_pos (i : Fin m) : 0 < self.Λ i

noncomputable def Frourio.BasicFrourioOperator (a : ℝ) (ha : 0 < a) : FrourioOperator 2

2点Frourio作用素（基本ケース）

Equations

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

noncomputable def Frourio.GoldenFrourioOperator : FrourioOperator 2

黄金Frourio作用素（φに特化）

Equations

• Frourio.GoldenFrourioOperator = Frourio.BasicFrourioOperator Frourio.φ Frourio.ScaleOperator.golden._proof_1

noncomputable def Frourio.FrourioOperator.act {m : ℕ} (op : FrourioOperator m) (f : ℝ → ℂ) : ℝ → ℂ

m点Frourio作用素の関数への作用 Δ^⟨m⟩f = (1/x) Σ_{i=1}^m α_i χ_i f(Λ_i x)

Equations

• op.act f x = if x ≠ 0 then (∑ i : Fin m, op.α i * ↑(op.χ i).toInt * f (op.Λ i * x)) / ↑x else 0

noncomputable def Frourio.FrourioOperator.toScaleOperator {m : ℕ} (op : FrourioOperator m) (i : Fin m) : ScaleOperator

スケール作用素を個別に取り出す

Equations

• op.toScaleOperator i = { scale := op.Λ i, scale_pos := ⋯ }

noncomputable def Frourio.FrourioOperator.toInverseMult {m : ℕ} (_op : FrourioOperator m) : InverseMultOperator

逆数乗算作用素の取得（すべてのm点作用素で共通）

Equations

• _op.toInverseMult = { }

noncomputable def Frourio.FrourioOperator.linearCombination {m : ℕ} (op : FrourioOperator m) (f : ℝ → ℂ) : ℝ → ℂ

作用素の線形結合部分（M_{1/x}を除く）

Equations

• op.linearCombination f x = ∑ i : Fin m, op.α i * ↑(op.χ i).toInt * f (op.Λ i * x)

theorem Frourio.FrourioOperator.act_eq_inverseMult_linearComb {m : ℕ} (op : FrourioOperator m) (f : ℝ → ℂ) (x : ℝ) (hx : x ≠ 0) : op.act f x = op.linearCombination f x / ↑x

作用の分解表現：Δ^⟨m⟩ = M_{1/x} ∘ linearCombination

theorem Frourio.InverseMultOperator.mellin_shift (M : InverseMultOperator) (f : ℝ → ℂ) (x : ℝ) : x > 0 → M.act f x = f x / ↑x

逆数乗算作用素のMellin変換への作用 MM_{1/x} f = Mf

theorem Frourio.FrourioOperator.mellin_compatible {m : ℕ} (op : FrourioOperator m) : ∃ (S : ℂ → ℂ), ∀ (s : ℂ), S s = ∑ i : Fin m, op.α i * ↑(op.χ i).toInt * ↑(op.Λ i) ^ (-s)

FrourioOperatorのMellin記号との整合性