Complex powers of positive-valued characters

This file turns a continuous monoid homomorphism to the positive nonnegative reals into a complex-valued character by taking a fixed complex power.

Main definitions

• MonoidHom.cpowCharacter: the character x ↦ (f x) ^ s associated to a continuous homomorphism f : G →* ℝ≥0ˣ and an exponent s : ℂ.
• TauCeti.normCpowCharacter: the character x ↦ ‖x‖ ^ s of the units of a normed division ring.

noncomputable def MonoidHom.cpowCharacter {G : Type u_1} [Monoid G] [TopologicalSpace G] (f : G →* NNRealˣ) (hf : Continuous ⇑f) (s : ℂ) : G →ₜ* ℂˣ

The character x ↦ (f x) ^ s associated to a continuous positive-valued homomorphism f : G →* ℝ≥0ˣ and a complex exponent s.

Equations

• f.cpowCharacter hf s = { toFun := fun (x : G) => Units.mk0 (↑↑↑(f x) ^ s) ⋯, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

@[simp]

theorem MonoidHom.coe_cpowCharacter_apply {G : Type u_1} [Monoid G] [TopologicalSpace G] (f : G →* NNRealˣ) (hf : Continuous ⇑f) (s : ℂ) (x : G) : ↑((f.cpowCharacter hf s) x) = ↑↑↑(f x) ^ s

Evaluating f.cpowCharacter hf s at x gives (f x) ^ s.

theorem MonoidHom.norm_coe_cpowCharacter_apply {G : Type u_1} [Monoid G] [TopologicalSpace G] (f : G →* NNRealˣ) (hf : Continuous ⇑f) (s : ℂ) (x : G) : ‖↑((f.cpowCharacter hf s) x)‖ = ↑↑(f x) ^ s.re

The absolute value of f.cpowCharacter hf s at x is (f x) ^ re s.

@[simp]

theorem MonoidHom.cpowCharacter_zero {G : Type u_1} [Monoid G] [TopologicalSpace G] (f : G →* NNRealˣ) (hf : Continuous ⇑f) : f.cpowCharacter hf 0 = 1

The exponent 0 gives the trivial character.

@[simp]

theorem MonoidHom.cpowCharacter_add {G : Type u_1} [Monoid G] [TopologicalSpace G] (f : G →* NNRealˣ) (hf : Continuous ⇑f) (s t : ℂ) : f.cpowCharacter hf (s + t) = f.cpowCharacter hf s * f.cpowCharacter hf t

Adding exponents multiplies the associated characters.

noncomputable def TauCeti.normCpowCharacter (𝕜 : Type u_2) [NormedDivisionRing 𝕜] (s : ℂ) : 𝕜ˣ →ₜ* ℂˣ

The character x ↦ ‖x‖ ^ s of the units of a normed division ring, for a complex exponent s.

Equations

• TauCeti.normCpowCharacter 𝕜 s = (Units.map ↑nnnormHom).cpowCharacter ⋯ s

@[simp]

theorem TauCeti.coe_normCpowCharacter_apply (𝕜 : Type u_2) [NormedDivisionRing 𝕜] (s : ℂ) (x : 𝕜ˣ) : ↑((normCpowCharacter 𝕜 s) x) = ↑‖↑x‖ ^ s

Evaluating normCpowCharacter 𝕜 s at x gives ‖x‖ ^ s.

theorem TauCeti.norm_coe_normCpowCharacter_apply (𝕜 : Type u_2) [NormedDivisionRing 𝕜] (s : ℂ) (x : 𝕜ˣ) : ‖↑((normCpowCharacter 𝕜 s) x)‖ = ‖↑x‖ ^ s.re

The absolute value of normCpowCharacter 𝕜 s at x is ‖x‖ ^ re s.

@[simp]

theorem TauCeti.normCpowCharacter_zero (𝕜 : Type u_2) [NormedDivisionRing 𝕜] : normCpowCharacter 𝕜 0 = 1

The exponent 0 gives the trivial character.

@[simp]

theorem TauCeti.normCpowCharacter_add (𝕜 : Type u_2) [NormedDivisionRing 𝕜] (s t : ℂ) : normCpowCharacter 𝕜 (s + t) = normCpowCharacter 𝕜 s * normCpowCharacter 𝕜 t

Adding exponents multiplies the characters.