Homomorphisms from C-star to C-star

This note collects the Cauchy functional equations used when a determinant argument leaves a one-variable group homomorphism

g:\mathbb C^*\to\mathbb C^*, \qquad g(zw)=g(z)g(w).

(1)

Without regularity assumptions such homomorphisms can be highly nonconstructive. With continuity, or even Borel measurability, they have one simple form.

Lean formalization

The proofs in this note are formalized in Lean 4 + Mathlib in CstarHomomorphismFlow.lean, which reproduces the note’s derivations in order (re-deriving the additive measurable-implies-continuous step from the Steinhaus theorem), together with the general automatic-continuity lemmas in AutomaticContinuity.lean. Each Lean proof dropdown below includes the corresponding declaration verbatim from the compiled source, so the displayed code cannot drift from what is actually checked. Continuous integration runs lake build (which fails on any error or sorry), so every displayed proof is guaranteed to type-check.

Lean’s kernel guarantees each proof is correct. Whether a Lean statement faithfully captures the informal claim is a human judgement, so each dropdown is placed next to the statement it formalizes, for direct comparison.

Cauchy’s Additive Functional Equation¶

Cauchy’s functional equation (Wikipedia (2025)) usually means the additive equation

a(x+y)=a(x)+a(y).

(2)

There are other related equations, such as Cauchy’s multiplicative functional equation in the next section.

For an integer $n>0$ ,

a(nx) =a(\underbrace{x+x+\dots+x}_{n}) =\underbrace{a(x)+a(x)+\dots+a(x)}_{n} =na(x).

(3)

Also $a(0)=a(0)+a(0)$ , so $a(0)=0$ , and

0=a(0)=a(x-x)=a(x)+a(-x),

(4)

so $a(-x)=-a(x)$ . Thus $a(nx)=na(x)$ for all integers $n$ .

By substituting $y=nx$ , we get $a(y)=na(y/n)$ , hence

a(y/n)={1\over n}a(y).

(5)

Combining multiplication and division by integers gives, for any rational $q=p/n$ ,

a(qx)=a\left({p\over n}x\right) =p\,a\left({x\over n}\right) ={p\over n}a(x) =q\,a(x).

(6)

Setting $x=1$ , every additive solution satisfies

a(q)=q\,a(1)=cq

(7)

for rational $q$ , where $c=a(1)$ .

CstarHomomorphismFlow.lean

/-- An additive map `ℝ → ℝ` is homogeneous for rational scalars. -/
theorem cauchy_additive_rat_homogeneous (a : ℝ → ℝ)
    (hadd : ∀ x y, a (x + y) = a x + a y) (q : ℚ) (x : ℝ) :
    a ((q : ℝ) * x) = (q : ℝ) * a x := by
  let f : ℝ →+ ℝ := AddMonoidHom.mk' a hadd
  simpa [f, smul_eq_mul] using map_ratCast_smul f ℝ ℝ q x

CstarHomomorphismFlow.lean

/--
If `c ≠ 0`, the rational-agreement example is not additive: adding a nonzero rational to an
irrational gives an explicit failure of Cauchy's equation.
-/
theorem rationalAgreementExample_not_additive {c α : ℝ} {q : ℚ}
    (hc : c ≠ 0) (hq : q ≠ 0) (hα : ¬ IsRatReal α) :
    rationalAgreementExample c (α + q) ≠
      rationalAgreementExample c α + rationalAgreementExample c (q : ℝ) := by
  have hαq : ¬ IsRatReal (α + q) := not_isRatReal_add_rat hα
  rw [rationalAgreementExample_irrational c hαq, rationalAgreementExample_irrational c hα,
    rationalAgreementExample_rat]
  simp only [zero_add]
  exact (mul_ne_zero hc (Rat.cast_ne_zero.mpr hq)).symm

The function is also measurable (measurable_rationalAgreementExample) and agrees with c·x on the rationals (rationalAgreementExample_rat), matching the note.

Proof

Let $b(x)=a(x)-a(1)x$ . Then $b$ is additive, measurable, and $b(q)=0$ for all rational $q$ . It is enough to prove that $b=0$ .

Since

[-1,1]=\bigcup_{m=1}^{\infty}\{x\in[-1,1]: |b(x)|\le m\},

(11)

one of these measurable sets has positive measure. Let

E=\{x\in[-1,1]: |b(x)|\le m\}

(12)

be such a set. By the Steinhaus theorem, the difference set

E-E=\{u-v:u,v\in E\}

(13)

contains an open interval around 0: there is $\epsilon>0$ such that $(-\epsilon,\epsilon)\subset E-E$ . Thus, if $|t|<\epsilon$ , then $t=u-v$ for some $u,v\in E$ . By additivity,

b(t)=b(u-v)=b(u)-b(v),

(14)

|b(t)|\le |b(u)|+|b(v)|\le 2m.

(15)

Therefore $b$ is bounded on an interval around 0. Taking $\delta=\epsilon/2$ and $M=2m$ , we have

|b(t)|\le M \qquad\text{whenever}\qquad |t|\le\delta.

(16)

Additivity then implies continuity at 0. Indeed, let $x_j\to0$ . For $x_j\ne0$ , choose, for all large $j$ ,

n_j=\left\lfloor {\delta\over 2|x_j|}\right\rfloor.

(17)

Then $n_j\to\infty$ and $|n_jx_j|\le\delta$ , so $n_jx_j$ lies in the interval where $b$ is bounded. Since $b$ is additive,

b(n_jx_j)=n_jb(x_j),

(18)

and therefore

|b(x_j)|={|b(n_jx_j)|\over n_j}\to0.

(19)

The last limit follows from $|b(n_jx_j)|\le M$ and $n_j\to\infty$ . Hence $b$ is continuous at 0.

An additive function continuous at 0 is continuous everywhere. To see this, fix $x_0\in\mathbb R$ and let $x\to x_0$ . Then $x-x_0\to0$ , and additivity gives

b(x)-b(x_0)=b(x-x_0).

(20)

Since $b$ is continuous at 0, the right-hand side tends to 0. Therefore $b(x)\to b(x_0)$ , so $b$ is continuous at $x_0$ . Since $x_0$ was arbitrary, $b$ is continuous everywhere. Since $b$ vanishes on the dense set $\mathbb Q$ , continuity gives $b(x)=0$ for every real $x$ .

The flow-faithful formalization in CstarHomomorphismFlow.lean writes out the argument above using only the Steinhaus theorem (MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos) as its measure-theoretic input, rather than calling Mathlib’s packaged MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable.

Step 1 — Steinhaus gives boundedness on a neighbourhood of 0:

CstarHomomorphismFlow.lean

/-- **Step 1 (Steinhaus).** A measurable additive `a : ℝ → ℝ` is bounded on a neighbourhood of
`0`.  The level sets `{x | |a x| ≤ m}` cover `ℝ`, so one has positive measure; by the Steinhaus
theorem its difference set is a neighbourhood of `0`, on which additivity bounds `a` by `2 m`. -/
theorem bounded_nhds_zero_of_additive_measurable (a : ℝ → ℝ)
    (hadd : ∀ x y, a (x + y) = a x + a y) (hmeas : Measurable a) :
    ∃ ε > 0, ∃ M : ℝ, ∀ t : ℝ, |t| < ε → |a t| ≤ M := by
  classical
  let f : ℝ →+ ℝ := AddMonoidHom.mk' a hadd
  set S : ℕ → Set ℝ := fun m => {x : ℝ | |a x| ≤ (m : ℝ)} with hS
  have hSmeas : ∀ m, MeasurableSet (S m) := fun m => hmeas.abs measurableSet_Iic
  have hcover : ⋃ m, S m = Set.univ := by
    rw [Set.eq_univ_iff_forall]; intro x
    obtain ⟨m, hm⟩ := exists_nat_ge |a x|
    exact Set.mem_iUnion.2 ⟨m, hm⟩
  have hpos : ∃ m, 0 < volume (S m) := by
    by_contra h
    have hall : ∀ m, volume (S m) = 0 := by
      intro m
      by_contra hm
      exact h ⟨m, pos_iff_ne_zero.mpr hm⟩
    have huniv : volume (Set.univ : Set ℝ) = 0 := by
      rw [← hcover]; exact measure_iUnion_null hall
    rw [Real.volume_univ] at huniv
    exact ENNReal.top_ne_zero huniv
  obtain ⟨m, hmpos⟩ := hpos
  have hstein : S m - S m ∈ 𝓝 (0 : ℝ) :=
    MeasureTheory.Measure.sub_mem_nhds_zero_of_addHaar_pos volume (S m) (hSmeas m) hmpos
  obtain ⟨ε, hε, hball⟩ := Metric.mem_nhds_iff.1 hstein
  refine ⟨ε, hε, 2 * m, ?_⟩
  intro t ht
  have htmem : t ∈ S m - S m :=
    hball (by simpa [Metric.mem_ball, Real.dist_eq, sub_zero] using ht)
  obtain ⟨u, hu, v, hv, rfl⟩ := htmem
  have hauv : a (u - v) = a u - a v := map_sub f u v
  rw [hauv]
  simp only [S, Set.mem_setOf_eq] at hu hv
  have htri : |a u - a v| ≤ |a u| + |a v| := abs_sub (a u) (a v)
  linarith

Step 2 — the n·x scaling upgrades boundedness near 0 to a Lipschitz bound at 0:

CstarHomomorphismFlow.lean

/-- **Step 2 (integer scaling).** If `a` is additive and bounded by `M` on `(-ε, ε)`, then near
`0` it obeys the linear bound `|a x| ≤ (4 M / ε) |x|`.  This is the note's `n • x` argument:
choosing `n = ⌊ε / (2 |x|)⌋` makes `|n • x| < ε`, and `a (n • x) = n • a x` gives
`|a x| ≤ M / n`. -/
theorem lipschitzAt_zero_of_bounded (a : ℝ → ℝ) (hadd : ∀ x y, a (x + y) = a x + a y)
    (ε : ℝ) (hε : 0 < ε) (M : ℝ) (hbound : ∀ t, |t| < ε → |a t| ≤ M) :
    ∀ x : ℝ, |x| < ε / 4 → |a x| ≤ (4 * M / ε) * |x| := by
  classical
  let f : ℝ →+ ℝ := AddMonoidHom.mk' a hadd
  have hmul : ∀ (n : ℕ) (x : ℝ), a ((n : ℝ) * x) = (n : ℝ) * a x := by
    intro n x
    have h : f (n • x) = n • f x := map_nsmul f n x
    simp only [nsmul_eq_mul] at h; exact h
  intro x hx
  rcases eq_or_ne x 0 with hx0 | hx0
  · subst hx0
    have ha0 : a 0 = 0 := map_zero f
    rw [ha0]; simp
  · have hxpos : 0 < |x| := abs_pos.2 hx0
    have h2x : (0 : ℝ) < 2 * |x| := by positivity
    set N : ℕ := ⌊ε / (2 * |x|)⌋₊ with hN
    have hNle : (N : ℝ) ≤ ε / (2 * |x|) := Nat.floor_le (by positivity)
    have hNgt : ε / (2 * |x|) - 1 < (N : ℝ) := Nat.sub_one_lt_floor _
    have h1 : 2 * |x| * (N : ℝ) ≤ ε := by
      rw [le_div_iff₀ h2x] at hNle; nlinarith [hNle]
    have hAux : ε / (2 * |x|) < (N : ℝ) + 1 := by linarith
    have h2b : ε < 2 * |x| * ((N : ℝ) + 1) := by
      rw [div_lt_iff₀ h2x] at hAux; nlinarith [hAux]
    have hX4 : 4 * |x| < ε := by linarith [hx]
    have h2 : ε < 4 * |x| * (N : ℝ) := by nlinarith [h2b, hX4]
    have hNpos : 0 < (N : ℝ) := by nlinarith [h2, hX4, hxpos]
    have hbnd : (N : ℝ) * |a x| ≤ M := by
      have hlt : |(N : ℝ) * x| < ε := by
        rw [abs_mul, Nat.abs_cast]; nlinarith [h1, hxpos]
      have hb := hbound ((N : ℝ) * x) hlt
      rw [hmul N x, abs_mul, Nat.abs_cast] at hb
      exact hb
    have hAxnn : 0 ≤ |a x| := abs_nonneg _
    rw [div_mul_eq_mul_div, le_div_iff₀ hε]
    nlinarith [hbnd, h2, hAxnn, hxpos, mul_nonneg hAxnn (le_of_lt hxpos)]

Step 3 — continuity at 0, propagated everywhere by additivity:

CstarHomomorphismFlow.lean

/-- **Steps 1–3 combined.** A measurable additive `a : ℝ → ℝ` is continuous.  The Lipschitz bound
at `0` gives continuity at `0`; additivity (`continuous_of_continuousAt_zero`) propagates it
everywhere.  This re-derives `MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable` from the
Steinhaus theorem alone. -/
theorem continuous_of_additive_measurable (a : ℝ → ℝ)
    (hadd : ∀ x y, a (x + y) = a x + a y) (hmeas : Measurable a) : Continuous a := by
  let f : ℝ →+ ℝ := AddMonoidHom.mk' a hadd
  obtain ⟨ε, hε, M, hbound⟩ := bounded_nhds_zero_of_additive_measurable a hadd hmeas
  have hlip := lipschitzAt_zero_of_bounded a hadd ε hε M hbound
  have ha0 : a 0 = 0 := map_zero f
  have hg : Tendsto (fun x : ℝ => (4 * M / ε) * |x|) (𝓝 0) (𝓝 0) := by
    have : Tendsto (fun x : ℝ => |x|) (𝓝 0) (𝓝 0) := by
      simpa using (continuous_abs.tendsto (0 : ℝ))
    simpa using this.const_mul (4 * M / ε)
  have hev : ∀ᶠ x in 𝓝 (0 : ℝ), ‖a x‖ ≤ (4 * M / ε) * |x| := by
    have hb : Metric.ball (0 : ℝ) (ε / 4) ∈ 𝓝 (0 : ℝ) := Metric.ball_mem_nhds _ (by positivity)
    filter_upwards [hb] with x hxb
    rw [Real.norm_eq_abs]
    exact hlip x (by simpa [Metric.mem_ball, Real.dist_eq, sub_zero] using hxb)
  have htend : Tendsto a (𝓝 0) (𝓝 0) := squeeze_zero_norm' hev hg
  have hcontAt : ContinuousAt a 0 := by rw [ContinuousAt, ha0]; exact htend
  exact continuous_of_continuousAt_zero f hcontAt

Conclusion — linearity a(x)=a(1)·x (and the existence form cauchy_additive_measurable_exists):

CstarHomomorphismFlow.lean

/-- **The note's additive theorem, re-derived.** A measurable solution of Cauchy's additive
equation on `ℝ` is linear, `a x = a 1 * x`.  Continuity comes from
`continuous_of_additive_measurable` above (the Steinhaus re-derivation), not from the library
black box `MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable`. -/
theorem cauchy_additive_measurable_linear (a : ℝ → ℝ)
    (hadd : ∀ x y, a (x + y) = a x + a y) (hmeas : Measurable a) :
    ∀ x : ℝ, a x = a 1 * x := by
  let f : ℝ →+ ℝ := AddMonoidHom.mk' a hadd
  have hcont : Continuous f := continuous_of_additive_measurable a hadd hmeas
  intro x
  have hsmul : f (x • (1 : ℝ)) = x • f (1 : ℝ) := map_real_smul f hcont x 1
  simpa [f, smul_eq_mul, mul_comm] using hsmul

/-- Existence form of the measurable additive Cauchy equation. -/
theorem cauchy_additive_measurable_exists (a : ℝ → ℝ)
    (hadd : ∀ x y, a (x + y) = a x + a y) (hmeas : Measurable a) :
    ∃ c : ℝ, ∀ x : ℝ, a x = c * x :=
  ⟨a 1, cauchy_additive_measurable_linear a hadd hmeas⟩

CstarHomomorphismFlow.lean

/--
**Measurability is essential.** Without a regularity hypothesis, Cauchy's additive equation has
nonlinear solutions: there is an additive map `a : ℝ → ℝ` that is not of the form `a x = c * x` for
any constant `c`. By `cauchy_additive_measurable_linear` any such `a` is necessarily non-measurable.
The construction picks out one coordinate of a Hamel basis of `ℝ` over `ℚ`, so it depends on the
axiom of choice.
-/
theorem exists_additive_not_linear :
    ∃ a : ℝ → ℝ, (∀ x y, a (x + y) = a x + a y) ∧ ¬ ∃ c : ℝ, ∀ x, a x = c * x := by
  classical
  let B : Module.Basis (Module.Basis.ofVectorSpaceIndex ℚ ℝ) ℚ ℝ := Module.Basis.ofVectorSpace ℚ ℝ
  haveI hnt : Nontrivial (Module.Basis.ofVectorSpaceIndex ℚ ℝ) := by
    rw [← Cardinal.one_lt_iff_nontrivial]
    have hmk := B.mk_eq_rank
    rw [Real.rank_rat_real] at hmk
    simp only [Cardinal.lift_id] at hmk
    rw [hmk]
    exact_mod_cast Cardinal.nat_lt_continuum 1
  obtain ⟨i, j, hij⟩ := exists_pair_ne (Module.Basis.ofVectorSpaceIndex ℚ ℝ)
  refine ⟨fun x => ((B.repr x i : ℚ) : ℝ), ?_, ?_⟩
  · intro x y
    simp only [map_add, Finsupp.add_apply, Rat.cast_add]
  · rintro ⟨c, hc⟩
    have hBi : ((B.repr (B i) i : ℚ) : ℝ) = 1 := by
      rw [Module.Basis.repr_self, Finsupp.single_eq_same, Rat.cast_one]
    have hBj : ((B.repr (B j) i : ℚ) : ℝ) = 0 := by
      rw [Module.Basis.repr_self, Finsupp.single_apply, if_neg (Ne.symm hij), Rat.cast_zero]
    have hci : ((B.repr (B i) i : ℚ) : ℝ) = c * B i := hc (B i)
    have hcj : ((B.repr (B j) i : ℚ) : ℝ) = c * B j := hc (B j)
    rw [hBi] at hci
    rw [hBj] at hcj
    have hc0 : c = 0 := by
      rcases mul_eq_zero.mp hcj.symm with h | h
      · exact h
      · exact absurd h (B.ne_zero j)
    rw [hc0, zero_mul] at hci
    exact one_ne_zero hci

The Hamel basis is Module.Basis.ofVectorSpace ℚ ℝ; Real.rank_rat_real (rank = 𝔠 > 1) provides two distinct basis indices, and the additive-but-nonlinear map is the coordinate at one of them. #print axioms exists_additive_not_linear confirms the expected dependence on Classical.choice.

Cauchy’s Multiplicative Functional Equation¶

Cauchy’s multiplicative functional equation is

m(xy)=m(x)m(y).

(21)

For a real-valued measurable function on $\mathbb R$ , the nonzero, nonconstant-one solutions are most cleanly written on $\mathbb R^*$ by the single formula

m(x)=\operatorname{sgn}(x)^\epsilon |x|^c, \qquad x\in\mathbb R^*, \qquad \epsilon\in\{0,1\},\quad c\in\mathbb R.

(22)

They extend to $\mathbb R$ by setting $m(0)=0$ . In addition, there are the two degenerate solutions $m\equiv0$ and $m\equiv1$ on all of $\mathbb R$ .

Here is the derivation. If $m\not\equiv0$ , then $m(1)=1$ . On positive numbers, $m(x)>0$ , because $x=(\sqrt x)^2$ and $m(x)=m(\sqrt x)^2$ , and also $m(x)\ne0$ , because $m(x)m(x^{-1})=m(1)=1$ . Define

b(t)=\log m(e^t).

(23)

Then

b(t+u)=\log m(e^{t+u}) =\log m(e^t e^u) =\log(m(e^t)m(e^u)) =b(t)+b(u).

(24)

If $m$ is measurable, then $b$ is measurable, so by the additive theorem

b(t)=ct,

(25)

and therefore

m(x)=x^c,\qquad x>0.

(26)

Finally, $m(-1)^2=m(1)=1$ , so $m(-1)=1$ or $m(-1)=-1$ . Hence

m(x)=m(\operatorname{sgn}(x))m(|x|) =\operatorname{sgn}(x)^\epsilon |x|^c, \qquad x\in\mathbb R^*,

(27)

with $\epsilon=0$ in the even case and $\epsilon=1$ in the odd case.

CstarHomomorphismFlow.lean

/--
The nondegenerate measurable real multiplicative Cauchy equation on `ℝˣ`: away from zero the
solution is a power of `|x|`, with the independent sign `m (-1) = ±1`.
-/
theorem cauchy_multiplicative_eq_sign_rpow_on_nonzero (m : ℝ → ℝ)
    (hm : ∀ x y : ℝ, m (x * y) = m x * m y) (h1 : m 1 = 1) (hmeas : Measurable m) :
    ∃ c : ℝ,
      (m (-1) = 1 ∨ m (-1) = -1) ∧
        ∀ {x : ℝ}, x ≠ 0 → m x = (if x < 0 then m (-1) else 1) * |x| ^ c := by
  obtain ⟨c, hc⟩ := cauchy_multiplicative_eq_rpow_on_pos m hm h1 hmeas
  refine ⟨c, cauchy_multiplicative_neg_one_cases m hm h1, ?_⟩
  intro x hx
  by_cases hneg : x < 0
  · have habs_pos : 0 < |x| := abs_pos.mpr hx
    have hx_eq : x = (-1) * |x| := by
      rw [abs_of_neg hneg]
      ring
    calc
      m x = m ((-1) * |x|) := congrArg m hx_eq
      _ = m (-1) * m |x| := hm (-1) |x|
      _ = m (-1) * |x| ^ c := by rw [hc habs_pos]
      _ = (if x < 0 then m (-1) else 1) * |x| ^ c := by simp [hneg]
  · have hx_pos : 0 < x := lt_of_le_of_ne' (not_lt.mp hneg) hx
    have habs : |x| = x := abs_of_nonneg (not_lt.mp hneg)
    calc
      m x = x ^ c := hc hx_pos
      _ = (if x < 0 then m (-1) else 1) * |x| ^ c := by simp [hneg, habs]

The supporting steps m(x)>0 on positives, m(-1)²=1, and b(t)=log m(eᵗ) additive are cauchy_multiplicative_pos_of_pos, cauchy_multiplicative_neg_one_sq, and cauchy_multiplicative_log_exp_additive.

Measurable Homomorphisms $\mathbb C^\to\mathbb C^$ ¶

Let $g:\mathbb C^*\to\mathbb C^*$ be a group homomorphism. If $g$ is continuous, or merely Borel measurable, then

\boxed{\; g(w)=|w|^s\left({w\over |w|}\right)^k, \qquad s\in\mathbb C,\quad k\in\mathbb Z. \;}

(28)

Here $|w|^s=\exp(s\log |w|)$ , using the real logarithm of the positive number $|w|$ , so there is no branch choice.

Conversely, every formula in (28) defines a continuous homomorphism $\mathbb C^*\to\mathbb C^*$ .

CstarHomomorphismFlow.lean

/--
Every expression `w ↦ |w|^s (w/|w|)^k` defines a multiplicative homomorphism
`ℂˣ → ℂˣ`.
-/
def cstarFormulaHom (s : ℂ) (k : ℤ) : ℂˣ →* ℂˣ where
  toFun w := cstarNormCPow s w * cstarCircleUnit w ^ k
  map_one' := by simp
  map_mul' w z := by
    rw [cstarNormCPow_mul, cstarCircleUnit_mul, mul_zpow]
    ac_rfl

Continuity of this formula is continuous_cstarFormulaHom, bundled as the ContinuousMonoidHom named cstarFormulaContinuousHom; the special case cstarFormulaHom 1 1 = id is cstarFormulaHom_one_one.

Derivation

A Borel measurable homomorphism between these locally compact groups is automatically continuous (proved below in Borel measurability implies continuity), so it suffices to classify continuous homomorphisms. Every $w\in\mathbb C^*$ decomposes uniquely as

w=r\zeta,\qquad r=|w|\in\mathbb R_{>0},\qquad \zeta={w\over |w|}\in S^1.

(29)

Since these two factors commute,

g(w)=g(r)g(\zeta).

(30)

For the positive factor, set $G(t)=g(e^t)$ . This is a continuous homomorphism $(\mathbb R,+)\to\mathbb C^*$ . Because $\mathbb R$ is simply connected, it lifts through the exponential map to an additive continuous function $\ell:\mathbb R\to\mathbb C$ with

G(t)=\exp(\ell(t)).

(31)

Thus $\ell(t)=st$ for some $s\in\mathbb C$ , and

g(r)=r^s.

(32)

For the unit-circle factor, the image of $S^1$ is compact. Its modulus is a compact subgroup of $\mathbb R_{>0}$ , hence trivial, so $g(S^1)\subset S^1$ . Continuous characters of $S^1$ are exactly

\zeta\mapsto \zeta^k,\qquad k\in\mathbb Z.

(33)

Therefore

g(\zeta)=\zeta^k.

(34)

Multiplying the positive and unit-circle parts gives (28).

The Lean formalization of this derivation is split into the steps below.

CstarHomomorphismFlow.lean

/--
Every homomorphism `ℂˣ → ℂˣ` factors across the radial and unit-circle polar factors of its
argument.
-/
theorem cstar_homomorphism_polar_factorization (g : ℂˣ →* ℂˣ) (w : ℂˣ) :
    g w = g (cstarNormUnit w) * g (cstarCircleUnit w) := by
  have hw : w = cstarNormUnit w * cstarCircleUnit w := by
    ext
    exact (cstar_norm_mul_circle w).symm
  exact (congrArg g hw).trans (map_mul g (cstarNormUnit w) (cstarCircleUnit w))

CstarHomomorphismFlow.lean

/--
If a continuous additive-parameter homomorphism `ℝ → ℂˣ` has a continuous additive logarithmic
lift, then it has the form `t ↦ exp (s t)`.
-/
theorem real_to_cstar_exp_linear_of_lift (G : ℝ →+ Additive ℂˣ) (ell : ℝ → ℂ)
    (hell_add : ∀ x y, ell (x + y) = ell x + ell y) (hell_cont : Continuous ell)
    (hG : ∀ t,
      (Additive.toMul (G t) : ℂˣ) = Units.mk0 (Complex.exp (ell t)) (Complex.exp_ne_zero _)) :
    ∃ s : ℂ, ∀ t : ℝ,
      (Additive.toMul (G t) : ℂˣ) =
        Units.mk0 (Complex.exp (s * (t : ℂ))) (Complex.exp_ne_zero _) := by
  refine ⟨ell 1, ?_⟩
  intro t
  rw [hG]
  congr 1
  rw [cauchy_additive_continuous_complex_linear ell hell_add hell_cont t]
  ring_nf

/-- The map from `ℂˣ` to the nonzero complex subtype used by `Complex.isCoveringMap_exp`. -/
def additiveCstarToNonzero (G : ℝ →+ Additive ℂˣ) : ℝ → {z : ℂ // z ≠ 0} :=
  fun t => ⟨(Additive.toMul (α := ℂˣ) (G t) : ℂ), (Additive.toMul (α := ℂˣ) (G t)).ne_zero⟩

/--
Every continuous additive-parameter homomorphism `ℝ → ℂˣ` has a continuous logarithmic lift
through the complex exponential, normalized to vanish at `0`.
-/
theorem exists_continuous_log_lift_additive_cstar (G : ℝ →+ Additive ℂˣ)
    (hG : Continuous fun t => Additive.toMul (α := ℂˣ) (G t)) :
    ∃ ell : C(ℝ, ℂ), ell 0 = 0 ∧
      (fun z : ℂ => (⟨Complex.exp z, Complex.exp_ne_zero z⟩ : {z : ℂ // z ≠ 0})) ∘ ell =
        additiveCstarToNonzero G := by
  haveI : SimplyConnectedSpace ℝ := SimplyConnectedSpace.ofContractible ℝ
  let f : C(ℝ, {z : ℂ // z ≠ 0}) := {
    toFun := additiveCstarToNonzero G
    continuous_toFun := by
      dsimp [additiveCstarToNonzero]
      apply Continuous.subtype_mk
      exact Units.continuous_val.comp hG }
  have he0 : (fun z : ℂ => (⟨Complex.exp z, Complex.exp_ne_zero z⟩ : {z : ℂ // z ≠ 0})) 0 =
      f 0 := by
    ext
    simp [f, additiveCstarToNonzero]
  rcases Complex.isCoveringMap_exp.existsUnique_continuousMap_lifts f (0 : ℝ) (0 : ℂ) he0 with
    ⟨ell, hell0, _unique⟩
  exact ⟨ell, hell0.1, hell0.2⟩

/-- The normalized continuous logarithmic lift of an additive-parameter homomorphism is additive. -/
theorem continuous_log_lift_additive (G : ℝ →+ Additive ℂˣ)
    (_hG : Continuous fun t => Additive.toMul (α := ℂˣ) (G t))
    {ell : C(ℝ, ℂ)} (hell0 : ell 0 = 0)
    (hell_lift : (fun z : ℂ => (⟨Complex.exp z, Complex.exp_ne_zero z⟩ : {z : ℂ // z ≠ 0})) ∘ ell =
        additiveCstarToNonzero G) :
    ∀ x y : ℝ, ell (x + y) = ell x + ell y := by
  let p : ℂ → {z : ℂ // z ≠ 0} := fun z => ⟨Complex.exp z, Complex.exp_ne_zero z⟩
  let F₁ : ℝ × ℝ → ℂ := fun xy => ell (xy.1 + xy.2)
  let F₂ : ℝ × ℝ → ℂ := fun xy => ell xy.1 + ell xy.2
  have hcont₁ : Continuous F₁ := ell.continuous.comp (continuous_fst.add continuous_snd)
  have hcont₂ : Continuous F₂ :=
    (ell.continuous.comp continuous_fst).add (ell.continuous.comp continuous_snd)
  have hcomp : p ∘ F₁ = p ∘ F₂ := by
    ext xy
    change Complex.exp (ell (xy.1 + xy.2)) = Complex.exp (ell xy.1 + ell xy.2)
    have h₁ := congr_fun hell_lift (xy.1 + xy.2)
    have hx := congr_fun hell_lift xy.1
    have hy := congr_fun hell_lift xy.2
    change (⟨Complex.exp (ell (xy.1 + xy.2)), Complex.exp_ne_zero _⟩ : {z : ℂ // z ≠ 0}) =
      additiveCstarToNonzero G (xy.1 + xy.2) at h₁
    change (⟨Complex.exp (ell xy.1), Complex.exp_ne_zero _⟩ : {z : ℂ // z ≠ 0}) =
      additiveCstarToNonzero G xy.1 at hx
    change (⟨Complex.exp (ell xy.2), Complex.exp_ne_zero _⟩ : {z : ℂ // z ≠ 0}) =
      additiveCstarToNonzero G xy.2 at hy
    have hmul : Additive.toMul (α := ℂˣ) (G (xy.1 + xy.2)) =
        Additive.toMul (α := ℂˣ) (G xy.1) * Additive.toMul (α := ℂˣ) (G xy.2) := by
      rw [map_add]
      rfl
    have hxv : Complex.exp (ell xy.1) = (Additive.toMul (α := ℂˣ) (G xy.1) : ℂ) :=
      congrArg Subtype.val hx
    have hyv : Complex.exp (ell xy.2) = (Additive.toMul (α := ℂˣ) (G xy.2) : ℂ) :=
      congrArg Subtype.val hy
    calc
      Complex.exp (ell (xy.1 + xy.2)) =
          (Additive.toMul (α := ℂˣ) (G (xy.1 + xy.2)) : ℂ) :=
        congrArg Subtype.val h₁
      _ = (Additive.toMul (α := ℂˣ) (G xy.1) : ℂ) *
          (Additive.toMul (α := ℂˣ) (G xy.2) : ℂ) := by
        rw [hmul]
        rfl
      _ = Complex.exp (ell xy.1) * Complex.exp (ell xy.2) := by
        rw [hxv, hyv]
      _ = Complex.exp (ell xy.1 + ell xy.2) := (Complex.exp_add _ _).symm
  have h00 : F₁ (0, 0) = F₂ (0, 0) := by simp [F₁, F₂, hell0]
  have heq := Complex.isCoveringMap_exp.eq_of_comp_eq hcont₁ hcont₂ hcomp (0, 0) h00
  intro x y
  exact congr_fun heq (x, y)

/-- A continuous additive-parameter homomorphism `ℝ → ℂˣ` has the form `t ↦ exp (s t)`. -/
theorem additive_cstar_exp_linear (G : ℝ →+ Additive ℂˣ)
    (hG : Continuous fun t => Additive.toMul (α := ℂˣ) (G t)) :
    ∃ s : ℂ, ∀ t : ℝ,
      (Additive.toMul (G t) : ℂˣ) =
        Units.mk0 (Complex.exp (s * (t : ℂ))) (Complex.exp_ne_zero _) := by
  rcases exists_continuous_log_lift_additive_cstar G hG with ⟨ell, hell0, hell_lift⟩
  have hell_add := continuous_log_lift_additive G hG hell0 hell_lift
  refine real_to_cstar_exp_linear_of_lift G ell hell_add ell.continuous ?_
  intro t
  apply Units.ext
  exact (congrArg Subtype.val (congr_fun hell_lift t)).symm

This takes the additive logarithmic lift ell as a hypothesis (the “ℝ is simply connected, so it lifts through exp” step) and concludes the exponent form; the linear part ℓ(t)=s·t is cauchy_additive_continuous_complex_linear.

CstarHomomorphismFlow.lean

/--
Every continuous endomorphism of the unit circle has an integer slope in exponential coordinates.
-/
theorem circle_endomorphism_exp_int_slope (h : Circle →* Circle) (hh : Continuous h) :
    ∃ k : ℤ, ∀ t : ℝ, h (Circle.exp t) = Circle.exp ((k : ℝ) * t) := by
  haveI : Fact (0 < 2 * Real.pi) := ⟨by positivity⟩
  have hψcont : Continuous (circleEndomorphismAddChar h) :=
    continuous_circleEndomorphismAddChar h hh
  obtain ⟨k, hk⟩ :=
    continuous_addCircle_char_eq_fourier (circleEndomorphismAddChar h) hψcont
  refine ⟨k, ?_⟩
  intro t
  apply Circle.ext
  rw [Circle.coe_exp]
  have hk' := hk (t : AddCircle (2 * Real.pi))
  convert hk' using 1
  · simp [circleEndomorphismAddChar, AddCircle.toCircle_apply_mk]
  · rw [fourier_coe_apply]
    congr 1
    field_simp [Real.pi_ne_zero]
    push_cast
    ring

The “compact subgroup of ℝ_{>0} is trivial” argument is compact_additive_hom_to_real_eq_zero, applied via circle_hom_log_norm_eq_zero.

CstarHomomorphismFlow.lean

/--
If a circle endomorphism has the exponential-coordinate formula `exp t ↦ exp (k t)`, then it is
the power character `z ↦ z^k`.
-/
theorem circle_endomorphism_eq_zpow_of_exp_lift (h : Circle →* Circle) (k : ℤ)
    (h_exp : ∀ t : ℝ, h (Circle.exp t) = Circle.exp ((k : ℝ) * t)) :
    ∀ z : Circle, h z = z ^ k := by
  intro z
  rcases Circle.exp_surjective z with ⟨t, rfl⟩
  rw [h_exp]
  exact Circle.exp_intCast_mul t k

/--
**Continuous characters of the unit circle are exactly the integer power maps.** Every continuous
endomorphism of the circle has the form `z ↦ z ^ k` for some `k : ℤ`. (The converse, that each
`z ↦ z ^ k` is a continuous endomorphism, is `circlePowerContinuousHom`.)
-/
theorem continuous_circle_endomorphism_eq_zpow (h : Circle →* Circle) (hh : Continuous h) :
    ∃ k : ℤ, ∀ z : Circle, h z = z ^ k := by
  obtain ⟨k, hk⟩ := circle_endomorphism_exp_int_slope h hh
  exact ⟨k, circle_endomorphism_eq_zpow_of_exp_lift h k hk⟩

/--
The same statement for a continuous homomorphism `Circle → ℂˣ`, after restricting its codomain to
`Circle`.
-/
theorem circle_to_cstar_hom_eq_zpow_of_exp_lift (g : Circle →* ℂˣ) (hg : Continuous g) (k : ℤ)
    (h_exp : ∀ t : ℝ, circleHomToCircle g hg (Circle.exp t) = Circle.exp ((k : ℝ) * t)) :
    ∀ z : Circle, g z = Circle.toUnits (z ^ k) := by
  intro z
  rw [← circleHomToCircle_toUnits g hg z]
  congr 1
  exact circle_endomorphism_eq_zpow_of_exp_lift (circleHomToCircle g hg) k h_exp z

continuous_circle_endomorphism_eq_zpow is the unconditional statement, combining the integer-slope result below with circle_endomorphism_eq_zpow_of_exp_lift (which turns the exponential-coordinate formula exp t ↦ exp (k·t) into z ↦ zᵏ); circle_to_cstar_hom_eq_zpow_of_exp_lift is the Circle → ℂˣ variant used by the assembly. The converse ζ ↦ ζᵏ direction is circlePowerContinuousHom.

CstarHomomorphismFlow.lean

/--
Every continuous endomorphism of the unit circle has an integer slope in exponential coordinates.
-/
theorem circle_endomorphism_exp_int_slope (h : Circle →* Circle) (hh : Continuous h) :
    ∃ k : ℤ, ∀ t : ℝ, h (Circle.exp t) = Circle.exp ((k : ℝ) * t) := by
  haveI : Fact (0 < 2 * Real.pi) := ⟨by positivity⟩
  have hψcont : Continuous (circleEndomorphismAddChar h) :=
    continuous_circleEndomorphismAddChar h hh
  obtain ⟨k, hk⟩ :=
    continuous_addCircle_char_eq_fourier (circleEndomorphismAddChar h) hψcont
  refine ⟨k, ?_⟩
  intro t
  apply Circle.ext
  rw [Circle.coe_exp]
  have hk' := hk (t : AddCircle (2 * Real.pi))
  convert hk' using 1
  · simp [circleEndomorphismAddChar, AddCircle.toCircle_apply_mk]
  · rw [fourier_coe_apply]
    congr 1
    field_simp [Real.pi_ne_zero]
    push_cast
    ring

This is the analytic heart of “continuous characters of $S^1$ are $\zeta\mapsto\zeta^k$ ”: the character is identified with a nonzero Fourier mode on the additive circle. The supporting Fourier lemmas are circleValuedContinuousMap, exists_nonzero_fourierCoeff_circleValued, fourierCoeff_eigen, and continuous_addCircle_char_eq_fourier.

CstarHomomorphismFlow.lean

/--
The final algebraic assembly step in the `ℂˣ` homomorphism formula: once the positive-real factor
has exponent `s` and the circle factor has winding number `k`, the homomorphism has the advertised
polar form.
-/
theorem cstar_homomorphism_formula_of_radial_and_circle (g : ℂˣ →* ℂˣ) (s : ℂ) (k : ℤ)
    (hradial : ∀ t : ℝ,
      g (cstarPositivePath t) = Units.mk0 (Complex.exp (s * (t : ℂ))) (Complex.exp_ne_zero _))
    (hcircle : ∀ z : ℂˣ, ‖(z : ℂ)‖ = 1 → g z = z ^ k) :
    ∀ w : ℂˣ, g w = cstarNormCPow s w * cstarCircleUnit w ^ k := by
  intro w
  rw [cstar_homomorphism_polar_factorization g w]
  rw [cstarNormUnit_eq_positivePath_log_norm, hradial,
    hcircle (cstarCircleUnit w) (norm_cstarCircleUnit w)]
  ext
  simp [cstarNormCPow]

/--
The C-star formula from the radial exponential formula and an integer-slope exponential-coordinate
formula for the circle factor.
-/
theorem cstar_homomorphism_formula_of_radial_and_circle_lift (g : ℂˣ →* ℂˣ) (hg : Continuous g)
    (s : ℂ) (k : ℤ)
    (hradial : ∀ t : ℝ,
      g (cstarPositivePath t) = Units.mk0 (Complex.exp (s * (t : ℂ))) (Complex.exp_ne_zero _))
    (hcircle_exp : ∀ t : ℝ,
      circleHomToCircle (g.comp Circle.toUnits) (hg.comp continuous_circle_toUnits) (Circle.exp t) =
        Circle.exp ((k : ℝ) * t)) :
    ∀ w : ℂˣ, g w = cstarNormCPow s w * cstarCircleUnit w ^ k := by
  apply cstar_homomorphism_formula_of_radial_and_circle g s k hradial
  intro z hz
  have hpow := circle_to_cstar_hom_eq_zpow_of_exp_lift (g.comp Circle.toUnits)
    (hg.comp continuous_circle_toUnits) k hcircle_exp (cstarUnitToCircle z hz)
  change g (Circle.toUnits (cstarUnitToCircle z hz)) =
    Circle.toUnits (cstarUnitToCircle z hz ^ k) at hpow
  rw [cstarUnitToCircle_toUnits] at hpow
  have hright : Circle.toUnits (cstarUnitToCircle z hz ^ k) = z ^ k := by
    rw [map_zpow, cstarUnitToCircle_toUnits]
  rwa [hright] at hpow

/--
The C-star formula with the circle factor classified automatically. It remains only to supply the
positive-real radial exponential formula.
-/
theorem cstar_homomorphism_formula_of_radial (g : ℂˣ →* ℂˣ) (hg : Continuous g) (s : ℂ)
    (hradial : ∀ t : ℝ,
      g (cstarPositivePath t) = Units.mk0 (Complex.exp (s * (t : ℂ))) (Complex.exp_ne_zero _)) :
    ∃ k : ℤ, ∀ w : ℂˣ, g w = cstarNormCPow s w * cstarCircleUnit w ^ k := by
  obtain ⟨k, hk⟩ := circle_endomorphism_exp_int_slope
    (circleHomToCircle (g.comp Circle.toUnits) (hg.comp continuous_circle_toUnits))
    (continuous_circleHomToCircle _ _)
  refine ⟨k, ?_⟩
  exact cstar_homomorphism_formula_of_radial_and_circle_lift g hg s k hradial hk

/-- The positive-real factor of a `ℂˣ` homomorphism, as an additive-parameter homomorphism. -/
def cstarPositiveFactorAddHom (g : ℂˣ →* ℂˣ) : ℝ →+ Additive ℂˣ where
  toFun t := Additive.ofMul (g (cstarPositivePath t))
  map_zero' := by
    change Additive.ofMul (g (cstarPositivePath 0)) = Additive.ofMul 1
    congr
    simp [cstarPositivePath]
  map_add' t u := by
    rw [cstarPositivePath_add, map_mul]
    rfl

theorem continuous_cstarPositiveFactorAddHom (g : ℂˣ →* ℂˣ) (hg : Continuous g) :
    Continuous fun t => Additive.toMul (α := ℂˣ) (cstarPositiveFactorAddHom g t) := by
  change Continuous fun t => g (cstarPositivePath t)
  exact hg.comp continuous_cstarPositivePath

/-- Every continuous homomorphism `ℂˣ → ℂˣ` has the classified polar form. -/
theorem cstar_homomorphism_formula_continuous (g : ℂˣ →* ℂˣ) (hg : Continuous g) :
    ∃ s : ℂ, ∃ k : ℤ, ∀ w : ℂˣ, g w = cstarNormCPow s w * cstarCircleUnit w ^ k := by
  obtain ⟨s, hs⟩ := additive_cstar_exp_linear (cstarPositiveFactorAddHom g)
    (continuous_cstarPositiveFactorAddHom g hg)
  obtain ⟨k, hk⟩ := cstar_homomorphism_formula_of_radial g hg s hs
  exact ⟨s, k, hk⟩

Three layers are shown: cstar_homomorphism_formula_of_radial_and_circle assembles the boxed formula from both factor classifications; ..._lift discharges the circle factor from its exponential-coordinate slope; and cstar_homomorphism_formula_of_radial classifies the circle automatically (via circle_endomorphism_exp_int_slope), so only the radial hypothesis hradial remains.

Borel measurability implies continuity¶

The boxed formula was derived assuming continuity, but the same conclusion holds for any Borel measurable homomorphism, because such a homomorphism is automatically continuous.

The analytic heart is automatic continuity for the one-parameter factors $(\mathbb R,+)\to\mathbb C^*$ . Let $f:\mathbb R\to\mathbb C^*$ be measurable with $f(t+s)=f(t)f(s)$ , and write $\Phi(t)=f(t)\in\mathbb C$ .

Modulus. $\rho(t)=|\Phi(t)|$ satisfies $\rho(t+s)=\rho(t)\rho(s)$ , so $t\mapsto\log\rho(t)$ is additive and measurable, hence linear by the additive measurable Cauchy theorem; thus $\rho(t)=e^{ct}$ is continuous. In particular $\Phi$ is locally bounded, so it is integrable on every bounded interval.
Phase, by the integration trick. The primitive $F(y)=\int_0^y\Phi$ is continuous. The Lebesgue differentiation theorem forces $F(a)\neq0$ for some $a$ (otherwise $\Phi=0$ almost everywhere, impossible since $\Phi$ never vanishes). The homomorphism property gives the sliding-window identity
$\Phi(s)\,F(a)=\int_0^a\Phi(s+u)\,du=\int_s^{s+a}\Phi=F(s+a)-F(s),$
(35)
so $\Phi(s)=\dfrac{F(s+a)-F(s)}{F(a)}$ is continuous in $s$ . Hence $f$ is continuous.

Applying this to the radial path $t\mapsto g(e^t)$ and, after pulling back through the covering quotient map $\mathtt{Circle.exp}:\mathbb R\to S^1$ , to the unit circle, both polar factors of $g$ are continuous, so $g$ is continuous everywhere.

This automatic-continuity step is proved in AutomaticContinuity.lean not just for $\mathbb C$ but for any field with RCLike 𝕜 (so for both $\mathbb R$ and $\mathbb C$ ): it is the multiplicative companion of Mathlib’s additive automatic-continuity theorem MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable. The flow-faithful file imports and uses it directly.

AutomaticContinuity.lean

/--
**Automatic continuity for the multiplicative Cauchy equation.** A Borel-measurable
`f : ℝ → 𝕜` (`RCLike 𝕜`, e.g. `ℝ` or `ℂ`) with `f (x + y) = f x * f y` and `f 0 ≠ 0` is
continuous. This is the multiplicative companion of
`MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable`.
-/
theorem continuous_of_measurable_of_mul {f : ℝ → 𝕜} (hmeas : Measurable f)
    (hmul : ∀ x y, f (x + y) = f x * f y) (h0 : f 0 ≠ 0) : Continuous f := by
  -- The hypotheses force `f` to vanish nowhere.
  have hne : ∀ x, f x ≠ 0 := by
    intro x hx
    apply h0
    have hfac : f 0 = f x * f (-x) := by rw [← hmul x (-x), add_neg_cancel]
    rw [hfac, hx, zero_mul]
  -- Modulus continuity via the additive automatic-continuity theorem.
  set ρ : ℝ → ℝ := fun t => ‖f t‖ with hρdef
  have hρpos : ∀ t, 0 < ρ t := fun t => norm_pos_iff.mpr (hne t)
  have hbadd : ∀ x y, Real.log (ρ (x + y)) = Real.log (ρ x) + Real.log (ρ y) := by
    intro x y
    rw [hρdef]
    simp only [hmul x y, norm_mul,
      Real.log_mul (ne_of_gt (norm_pos_iff.mpr (hne x))) (ne_of_gt (norm_pos_iff.mpr (hne y)))]
  have hbmeas : Measurable fun t => Real.log (ρ t) :=
    Real.measurable_log.comp (continuous_norm.measurable.comp hmeas)
  have hbcont : Continuous fun t => Real.log (ρ t) :=
    MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable
      (AddMonoidHom.mk' (fun t => Real.log (ρ t)) hbadd) hbmeas
  have hρcont : Continuous ρ := by
    have hrw : ρ = fun t => Real.exp (Real.log (ρ t)) := by
      funext t; rw [Real.exp_log (hρpos t)]
    rw [hrw]; exact Real.continuous_exp.comp hbcont
  -- `f` is interval integrable on every interval, dominated by the continuous modulus.
  have haesm : AEStronglyMeasurable f volume := hmeas.aestronglyMeasurable
  have hii : ∀ a b : ℝ, IntervalIntegrable f volume a b := by
    intro a b
    rw [intervalIntegrable_iff]
    exact Integrable.mono' (intervalIntegrable_iff.mp (hρcont.intervalIntegrable a b))
      haesm.restrict (ae_of_all _ fun x => (congrFun hρdef x).ge)
  -- The primitive of `f` is continuous.
  set F : ℝ → 𝕜 := fun y => ∫ t in (0:ℝ)..y, f t with hFdef
  have hFcont : Continuous F := intervalIntegral.continuous_primitive hii 0
  -- Some window `[0, a]` has nonzero integral, by the Lebesgue differentiation theorem.
  have hExists : ∃ a : ℝ, F a ≠ 0 := by
    by_contra hcon
    simp only [not_exists, not_ne_iff] at hcon
    have hReloc : LocallyIntegrable (fun t => RCLike.re (f t)) volume :=
      hρcont.locallyIntegrable.mono
        (RCLike.continuous_re.measurable.comp hmeas).aestronglyMeasurable
        (ae_of_all _ fun x => by
          rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (hρpos x)]
          exact (RCLike.abs_re_le_norm (f x)).trans_eq (congrFun hρdef x).symm)
    have hImloc : LocallyIntegrable (fun t => RCLike.im (f t)) volume :=
      hρcont.locallyIntegrable.mono
        (RCLike.continuous_im.measurable.comp hmeas).aestronglyMeasurable
        (ae_of_all _ fun x => by
          rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (hρpos x)]
          exact (RCLike.abs_im_le_norm (f x)).trans_eq (congrFun hρdef x).symm)
    have hReprim : ∀ y : ℝ, (∫ t in (0:ℝ)..y, RCLike.re (f t)) = 0 := by
      intro y
      have h := RCLike.reCLM.intervalIntegral_comp_comm (hii 0 y)
      simp only [RCLike.reCLM_apply] at h
      rw [h]
      have hFy : (∫ t in (0:ℝ)..y, f t) = F y := rfl
      rw [hFy, hcon y, RCLike.zero_re]
    have hImprim : ∀ y : ℝ, (∫ t in (0:ℝ)..y, RCLike.im (f t)) = 0 := by
      intro y
      have h := RCLike.imCLM.intervalIntegral_comp_comm (hii 0 y)
      simp only [RCLike.imCLM_apply] at h
      rw [h]
      have hFy : (∫ t in (0:ℝ)..y, f t) = F y := rfl
      rw [hFy, hcon y, RCLike.zero_im]
    have hzeroRe : ∀ᵐ x : ℝ, RCLike.re (f x) = 0 := by
      filter_upwards [LocallyIntegrable.ae_hasDerivAt_integral hReloc] with x hx
      have hd := hx 0
      rw [funext hReprim] at hd
      exact ((hasDerivAt_const x (0:ℝ)).unique hd).symm
    have hzeroIm : ∀ᵐ x : ℝ, RCLike.im (f x) = 0 := by
      filter_upwards [LocallyIntegrable.ae_hasDerivAt_integral hImloc] with x hx
      have hd := hx 0
      rw [funext hImprim] at hd
      exact ((hasDerivAt_const x (0:ℝ)).unique hd).symm
    have hzero : ∀ᵐ x : ℝ, f x = 0 := by
      filter_upwards [hzeroRe, hzeroIm] with x hxre hxim
      exact RCLike.ext (by rw [hxre, RCLike.zero_re]) (by rw [hxim, RCLike.zero_im])
    rw [ae_iff] at hzero
    have huniv : {x : ℝ | ¬ f x = 0} = Set.univ := by
      ext x; simpa using hne x
    rw [huniv, Real.volume_univ] at hzero
    exact ENNReal.top_ne_zero hzero
  -- The sliding-window identity recovers `f` from the continuous primitive.
  obtain ⟨a, ha⟩ := hExists
  have hwindow : ∀ s : ℝ, f s = (F (s + a) - F s) / F a := by
    intro s
    have h2 : (∫ u in (0:ℝ)..a, f (s + u)) = f s * ∫ u in (0:ℝ)..a, f u := by
      have hfun : (fun u => f (s + u)) = fun u => f s * f u := by
        funext u; rw [hmul s u]
      rw [hfun, intervalIntegral.integral_const_mul]
    have hsub : f s * F a = ∫ t in s..(s + a), f t := by
      have hFa : F a = ∫ u in (0:ℝ)..a, f u := rfl
      rw [hFa, ← h2, intervalIntegral.integral_comp_add_left f s, add_zero]
    have hadj : F (s + a) - F s = ∫ t in s..(s + a), f t := by
      have h := intervalIntegral.integral_add_adjacent_intervals (hii 0 s) (hii s (s + a))
      have hFsa : F (s + a) = ∫ t in (0:ℝ)..(s + a), f t := rfl
      have hFs : F s = ∫ t in (0:ℝ)..s, f t := rfl
      rw [hFsa, hFs, ← h]; ring
    rw [eq_div_iff ha, hsub, hadj]
  exact ((((hFcont.comp (continuous_id.add continuous_const)).sub hFcont)).div_const (F a)).congr
    fun s => (hwindow s).symm

The modulus step calls Mathlib’s additive theorem MeasureTheory.Measure.AddMonoidHom.continuous_of_measurable; the nonvanishing window is supplied by the interval form of the Lebesgue differentiation theorem (LocallyIntegrable.ae_hasDerivAt_integral); the primitive’s continuity is intervalIntegral.continuous_primitive.

AutomaticContinuity.lean

/--
**Automatic continuity for measurable homomorphisms `(ℝ, +) → 𝕜ˣ`.** A Borel-measurable
`f : ℝ → 𝕜ˣ` (`RCLike 𝕜`) with `f (x + y) = f x * f y` is continuous. This specializes at `𝕜 = ℂ`
to the automatic continuity of measurable group homomorphisms `(ℝ, +) → ℂ*`.
-/
theorem continuous_of_measurable_of_mul_units {f : ℝ → 𝕜ˣ} (hmeas : Measurable f)
    (hmul : ∀ x y, f (x + y) = f x * f y) : Continuous f := by
  have hval : Measurable fun x => (f x : 𝕜) := (comap_measurable Units.val).comp hmeas
  have hmulval : ∀ x y, ((f (x + y) : 𝕜)) = (f x : 𝕜) * (f y : 𝕜) := by
    intro x y; rw [hmul, Units.val_mul]
  have hcont : Continuous fun x => (f x : 𝕜) :=
    continuous_of_measurable_of_mul hval hmulval (f 0).ne_zero
  rw [Units.continuous_iff]
  exact ⟨hcont, by simpa [Units.inv_eq_val_inv] using hcont.inv₀ fun x => (f x).ne_zero⟩

The unit-circle factor of $g$ descends through the quotient map Circle.exp in continuous_cstar_on_circle, and the radial factor uses this lemma directly.

CstarHomomorphismFlow.lean

/--
**Automatic continuity.** A Borel-measurable group homomorphism `ℂˣ → ℂˣ` is continuous. The polar
factorization splits `g` into a radial part `t ↦ g (exp t)` and a unit-circle part, each continuous
by `continuous_of_measurable_of_mul_units`.
-/
theorem cstar_homomorphism_continuous_of_measurable (g : ℂˣ →* ℂˣ) (hg : Measurable g) :
    Continuous g := by
  have hrad : Continuous fun w : ℂˣ => g (cstarNormUnit w) := by
    have heq : (fun w : ℂˣ => g (cstarNormUnit w))
        = (fun t : ℝ => g (cstarPositivePath t)) ∘ fun w : ℂˣ => Real.log ‖(w : ℂ)‖ := by
      funext w
      simp only [Function.comp_apply, cstarNormUnit_eq_positivePath_log_norm]
    rw [heq]
    refine Continuous.comp ?_ continuous_log_norm_units
    exact continuous_of_measurable_of_mul_units
      (hg.comp (measurable_comap_iff.mpr
        (Units.continuous_val.comp continuous_cstarPositivePath).measurable))
      (fun t s => by rw [cstarPositivePath_add, map_mul])
  have hcirc : Continuous fun w : ℂˣ => g (cstarCircleUnit w) := by
    have heq : (fun w : ℂˣ => g (cstarCircleUnit w))
        = (fun z : Circle => g (Circle.toUnits z))
          ∘ fun w : ℂˣ => cstarUnitToCircle (cstarCircleUnit w) (norm_cstarCircleUnit w) := by
      funext w
      simp only [Function.comp_apply, cstarUnitToCircle_toUnits]
    rw [heq]
    exact (continuous_cstar_on_circle g hg).comp
      (continuous_cstarCircleUnit_val.subtype_mk _)
  exact (hrad.mul hcirc).congr fun w => (cstar_homomorphism_polar_factorization g w).symm

/--
A Borel-measurable homomorphism `ℂˣ → ℂˣ` has the boxed polar form `g w = |w|^s (w/|w|)^k`. This is
the measurable case of the classification: automatic continuity reduces it to
`cstar_homomorphism_formula_continuous`.
-/
theorem cstar_homomorphism_formula_measurable (g : ℂˣ →* ℂˣ) (hg : Measurable g) :
    ∃ s : ℂ, ∃ k : ℤ, ∀ w : ℂˣ, g w = cstarNormCPow s w * cstarCircleUnit w ^ k :=
  cstar_homomorphism_formula_continuous g (cstar_homomorphism_continuous_of_measurable g hg)

cstar_homomorphism_continuous_of_measurable assembles the radial and unit-circle factor continuities through the polar factorization, and cstar_homomorphism_formula_measurable feeds the resulting continuity into cstar_homomorphism_formula_continuous.

This is the formula needed for the free factor $g$ in Determinant From Homomorphism.

Multiplicative Cauchy from Measurable Homomorphisms¶

The measurable homomorphism classification gives a shorter derivation of the solutions to (21).

Let $m:\mathbb R\to\mathbb R$ be measurable and multiplicative:

m(xy)=m(x)m(y).

(36)

First, $m(1)=m(1)^2$ , so $m(1)=0$ or $m(1)=1$ . If $m(1)=0$ , then

m(x)=m(x\cdot 1)=m(x)m(1)=0,

(37)

so $m\equiv0$ .

Now assume $m(1)=1$ . Since $m(0)=m(0)^2$ , either $m(0)=0$ or $m(0)=1$ . If $m(0)=1$ , then

1=m(0)=m(0\cdot x)=m(0)m(x)=m(x),

(38)

so $m\equiv1$ .

It remains to handle $m(1)=1$ and $m(0)=0$ . For every $x\in\mathbb R^*$ ,

m(x)m(x^{-1})=m(1)=1,

(39)

so $m(x)\in\mathbb R^*$ . Therefore the restriction

m|_{\mathbb R^*}:\mathbb R^*\to\mathbb R^*

(40)

is a measurable group homomorphism.

The same classification argument as in Measurable Homomorphisms $\mathbb C^*\to\mathbb C^*$ , applied to $\mathbb R^*\cong\mathbb R_{>0}\times\{\pm1\}$ , gives

m(x)=\operatorname{sgn}(x)^\epsilon |x|^c, \qquad x\in\mathbb R^*, \qquad \epsilon\in\{0,1\},\quad c\in\mathbb R.

(41)

Indeed, the positive factor contributes $|x|^c$ , and the $\{\pm1\}$ factor contributes $m(-1)=\pm1$ , which is $\operatorname{sgn}(x)^\epsilon$ .

Extending by $m(0)=0$ gives exactly the nondegenerate solutions listed in (22), together with the degenerate solutions $m\equiv0$ and $m\equiv1$ .

CstarHomomorphismFlow.lean

/--
The same classification, with the nondegenerate branch explicitly recording the extension value
`m 0 = 0`.
-/
theorem cauchy_multiplicative_measurable_classification_with_zero (m : ℝ → ℝ)
    (hm : ∀ x y : ℝ, m (x * y) = m x * m y) (hmeas : Measurable m) :
    (∀ x : ℝ, m x = 0) ∨ (∀ x : ℝ, m x = 1) ∨
      ∃ c : ℝ,
        m 0 = 0 ∧ (m (-1) = 1 ∨ m (-1) = -1) ∧
          ∀ {x : ℝ}, x ≠ 0 → m x = (if x < 0 then m (-1) else 1) * |x| ^ c := by
  have h1sq : m 1 = m 1 * m 1 := by simpa using hm 1 1
  rcases eq_zero_or_eq_one_of_eq_mul_self h1sq with h1 | h1
  · exact Or.inl (cauchy_multiplicative_zero_of_map_one_eq_zero m hm h1)
  · right
    have h0sq : m 0 = m 0 * m 0 := by simpa using hm 0 0
    rcases eq_zero_or_eq_one_of_eq_mul_self h0sq with h0 | h0
    · exact Or.inr (by
        obtain ⟨c, hsign, hformula⟩ := cauchy_multiplicative_eq_sign_rpow_on_nonzero m hm h1 hmeas
        exact ⟨c, h0, hsign, hformula⟩)
    · exact Or.inl (cauchy_multiplicative_one_of_map_zero_eq_one m hm h0)

The three-way split (m≡0, m≡1, or the nondegenerate formula) follows the same case analysis on m(1) and m(0) used in the text; eq_zero_or_eq_one_of_eq_mul_self is the a=a²ᵉ ⇒ a∈{0,1} lemma.

The parameters in (41) are unique: the radial exponent $c\in\mathbb R$ is read off at $x=2$ (so $2^c=2^{c'}\Rightarrow c=c'$ ), and the sign $m(-1)\in\{\pm1\}$ at $x=-1$ . This is the real counterpart of the complex uniqueness Measurable Homomorphisms $\mathbb C^*\to\mathbb C^*$ : there the angular exponent is a full integer $k\in\mathbb Z$ , because the circle $U(1)$ has characters $\widehat{U(1)}=\mathbb Z$ ; here the angular group is $\{\pm1\}$ , whose character group is $\mathbb Z/2$ , so the integer $k$ collapses to $\epsilon=k\bmod 2$ — $k=1$ and $k=3$ give the same real sign character $\operatorname{sgn}$ .

CstarHomomorphismFlow.lean

/--
The real polar parametrization `(c, ε) ↦ (x ↦ ε^{[x<0]} |x|^c)` is injective on `ℝˣ`: the exponent
`c ∈ ℝ` (read off at `x = 2`) and the sign `ε` (read off at `x = -1`) are uniquely determined. This
is the real analogue of `cstarFormulaHom_injective`; note `ε` lives in `{±1}`, i.e. the angular
exponent is determined only modulo `2` — `k` and `k+2` give the same sign character.
-/
theorem realSignRpow_injective {c c' ε ε' : ℝ}
    (h : ∀ x : ℝ, x ≠ 0 →
      (if x < 0 then ε else 1) * |x| ^ c = (if x < 0 then ε' else 1) * |x| ^ c') :
    c = c' ∧ ε = ε' := by
  have hc : c = c' := by
    have h2 := h 2 (by norm_num)
    rw [if_neg (by norm_num : ¬(2 : ℝ) < 0), if_neg (by norm_num : ¬(2 : ℝ) < 0),
      one_mul, one_mul, show |(2 : ℝ)| = 2 from by norm_num] at h2
    have hlog := congrArg Real.log h2
    rw [Real.log_rpow (by norm_num), Real.log_rpow (by norm_num)] at hlog
    exact mul_right_cancel₀ (Real.log_pos (by norm_num)).ne' hlog
  have he : ε = ε' := by
    have hm1 := h (-1) (by norm_num)
    rw [if_pos (by norm_num : (-1 : ℝ) < 0), if_pos (by norm_num : (-1 : ℝ) < 0),
      show |(-1 : ℝ)| = 1 from by norm_num, Real.one_rpow, Real.one_rpow, mul_one, mul_one] at hm1
    exact hm1
  exact ⟨hc, he⟩

/--
**Uniqueness for the real classification.** For a measurable multiplicative `m : ℝ → ℝ` with
`m 1 = 1`, the pair `(c, m(-1)) ∈ ℝ × {±1}` in the nondegenerate form
`m x = (if x < 0 then m(-1) else 1) · |x|^c` is *unique*. This is the real counterpart of
`existsUnique_hom_factor_det_cstar`: the radial exponent `c` is unique in `ℝ` and the angular part
is the single sign `m(-1) ∈ {±1}` (the circle exponent `k ∈ ℤ` collapses to `k mod 2`).
-/
theorem existsUnique_cauchy_multiplicative_sign_rpow (m : ℝ → ℝ)
    (hm : ∀ x y : ℝ, m (x * y) = m x * m y) (h1 : m 1 = 1) (hmeas : Measurable m) :
    ∃! cε : ℝ × ℝ, (cε.2 = 1 ∨ cε.2 = -1) ∧
      ∀ x : ℝ, x ≠ 0 → m x = (if x < 0 then cε.2 else 1) * |x| ^ cε.1 := by
  obtain ⟨c, hsign, hform⟩ := cauchy_multiplicative_eq_sign_rpow_on_nonzero m hm h1 hmeas
  refine ⟨(c, m (-1)), ⟨hsign, fun x hx => hform hx⟩, ?_⟩
  rintro ⟨c', ε'⟩ ⟨_, hform'⟩
  have hagree : ∀ x : ℝ, x ≠ 0 →
      (if x < 0 then ε' else 1) * |x| ^ c' = (if x < 0 then m (-1) else 1) * |x| ^ c := by
    intro x hx
    rw [← hform' x hx, ← hform hx]
  obtain ⟨hc, he⟩ := realSignRpow_injective hagree
  simp only [Prod.mk.injEq]
  exact ⟨hc, he⟩

Multiplicative Functions on $\mathbb C$ ¶

The same argument extends the boxed homomorphism classification from $\mathbb C^*$ to all of $\mathbb C$ , i.e. to measurable functions

m:\mathbb C\to\mathbb C,\qquad m(zw)=m(z)m(w),

(42)

whose domain now contains 0. The result is the exact complex analogue of the real case in Multiplicative Cauchy from Measurable Homomorphisms: there are two degenerate solutions and one nondegenerate family.

First, $m(1)=m(1)^2$ , so $m(1)=0$ or $m(1)=1$ . If $m(1)=0$ , then

m(z)=m(z\cdot 1)=m(z)m(1)=0,

(43)

so $m\equiv0$ .

Now assume $m(1)=1$ . Since $m(0)=m(0)^2$ , either $m(0)=0$ or $m(0)=1$ . If $m(0)=1$ , then

1=m(0)=m(0\cdot z)=m(0)m(z)=m(z),

(44)

so $m\equiv1$ .

It remains to handle $m(1)=1$ and $m(0)=0$ . For every $z\in\mathbb C^*$ ,

m(z)m(z^{-1})=m(1)=1,

(45)

so $m(z)\in\mathbb C^*$ , and the restriction $m|_{\mathbb C^*}:\mathbb C^*\to\mathbb C^*$ is a measurable group homomorphism. By the boxed classification (28),

m(z)=|z|^{\,s}\left(\frac{z}{|z|}\right)^{k}, \qquad z\in\mathbb C^*,\qquad s\in\mathbb C,\ k\in\mathbb Z,

(46)

and the value at 0 is fixed by $m(0)=0$ .

So, in contrast with the $\mathbb C^*\to\mathbb C^*$ group homomorphisms (where $m\equiv1$ is just the parameter choice $s=0,\,k=0$ and $m\equiv0$ is impossible), the equation on all of $\mathbb C$ genuinely has the two extra degenerate solutions $m\equiv0$ and $m\equiv1$ , exactly because the codomain now includes 0 and the domain now includes 0.

CstarHomomorphismFlow.lean

/--
**Measurable multiplicative functions `ℂ → ℂ`.** A measurable `m : ℂ → ℂ` satisfying
`m (z * w) = m z * m w` is exactly one of three forms: the constant `0`; the constant `1`; or, in
the nondegenerate case `m 1 = 1` and `m 0 = 0`, the boxed `ℂ*`-homomorphism `z ↦ |z|^s (z / |z|)^k`
(`s ∈ ℂ`, `k ∈ ℤ`) extended by `m 0 = 0`. The nondegenerate branch restricts `m` to a measurable
group homomorphism `ℂ* → ℂ*` and invokes `cstar_homomorphism_formula_measurable`.
-/
theorem cauchy_multiplicative_complex_classification (m : ℂ → ℂ)
    (hm : ∀ z w : ℂ, m (z * w) = m z * m w) (hmeas : Measurable m) :
    (∀ z : ℂ, m z = 0) ∨ (∀ z : ℂ, m z = 1) ∨
      ∃ (s : ℂ) (k : ℤ), m 0 = 0 ∧
        ∀ z : ℂ, z ≠ 0 →
          m z = Complex.exp (s * (Real.log ‖z‖ : ℂ)) * (z / (‖z‖ : ℂ)) ^ k := by
  have h1sq : m 1 = m 1 * m 1 := by simpa using hm 1 1
  rcases eq_zero_or_eq_one_of_eq_mul_self h1sq with h1 | h1
  · exact Or.inl fun z => by simpa [h1] using hm z 1
  · refine Or.inr ?_
    have h0sq : m 0 = m 0 * m 0 := by simpa using hm 0 0
    rcases eq_zero_or_eq_one_of_eq_mul_self h0sq with h0 | h0
    · refine Or.inr ?_
      have hmne : ∀ w : ℂˣ, m (w : ℂ) ≠ 0 := by
        intro w hw
        have h := hm (w : ℂ) ((w : ℂ)⁻¹)
        rw [mul_inv_cancel₀ w.ne_zero, h1, hw, zero_mul] at h
        exact one_ne_zero h
      let M : ℂˣ →* ℂˣ :=
        { toFun := fun w => Units.mk0 (m (w : ℂ)) (hmne w)
          map_one' := by ext; simpa using h1
          map_mul' := fun w z => by ext; simpa using hm (w : ℂ) (z : ℂ) }
      have hMmeas : Measurable M :=
        measurable_comap_iff.mpr (hmeas.comp (comap_measurable Units.val))
      obtain ⟨s, k, hsk⟩ := cstar_homomorphism_formula_measurable M hMmeas
      refine ⟨s, k, h0, fun z hz => ?_⟩
      have hmz : m z = ((M (Units.mk0 z hz) : ℂˣ) : ℂ) := rfl
      rw [hmz, hsk (Units.mk0 z hz), Units.val_mul, coe_cstarNormCPow,
        Units.val_zpow_eq_zpow_val, coe_cstarCircleUnit, Units.val_mk0]
    · exact Or.inl fun z => by simpa [h0] using (hm 0 z).symm

The nondegenerate branch packages m|_{ℂ*} as a ℂˣ →* ℂˣ (m z ≠ 0 for z ≠ 0 because m(z)m(z⁻¹)=1), checks it is measurable, and applies cstar_homomorphism_formula_measurable; the polar factors are read back to ℂ via coe_cstarNormCPow and coe_cstarCircleUnit. The shared a=a² ⇒ a∈{0,1} lemma eq_zero_or_eq_one_of_eq_mul_self is now stated for any field, so it serves both the real and the complex case.

References¶

Wikipedia. (2025). Cauchy’s functional equation. https://en.wikipedia.org/wiki/Cauchy%27s_functional_equation

Homomorphisms from C-star to C-star

Cauchy’s Additive Functional Equation¶

Cauchy’s Multiplicative Functional Equation¶

Measurable Homomorphisms C∗→C∗\mathbb C^*\to\mathbb C^*C∗→C∗¶

Borel measurability implies continuity¶

Multiplicative Cauchy from Measurable Homomorphisms¶

Multiplicative Functions on C\mathbb CC¶

Measurable Homomorphisms $\mathbb C^\to\mathbb C^$ ¶

Multiplicative Functions on $\mathbb C$ ¶