Exponential and logarithm of topologically nilpotent elements

Let S be a complete, separated, linearly topologized commutative ℚ-algebra. For a topologically nilpotent a : S, the series of Mathlib's exponential NormedSpace.exp and logarithm NormedSpace.log

exp a = ∑ aⁿ / n!, log (1 + a) = ∑ (-1)ⁿ⁺¹ aⁿ / n

converge (IsTopologicallyNilpotent.hasSum_exp, IsTopologicallyNilpotent.hasSum_log), the two maps are mutually inverse, and they satisfy the functional equations. So for an ideal I of topologically nilpotent elements, the exponential is an isomorphism from the additive group of I onto its principal unit group of units u with u - 1 ∈ I, with inverse the logarithm (Ideal.expMulEquiv).

The formal identities exp (log (1 + X)) = 1 + X and log (exp X) = X are Mathlib's PowerSeries.subst_exp_log and PowerSeries.subst_log_exp_sub_one. They are transported to S by evaluating power series at a through Mathlib's continuous evaluation PowerSeries.aeval, which is compatible with substitution (PowerSeries.aeval_subst). A power series without constant term evaluates to a multiple of a, which keeps exp a - 1 and log (1 + a) topologically nilpotent and in every ideal containing a. The functional equation exp (a + b) = exp a * exp b is the Cauchy product of the exponential series in the complete nonarchimedean ring S, matched coefficientwise with Mathlib's PowerSeries.exp_mul_exp_eq_exp_add; its proof follows that of Mathlib's NormedSpace.exp_add_of_commute_of_mem_ball. Since exp a - 1 lies in every open ideal containing a, the exponential is continuous on an ideal of topologically nilpotent elements, so it carries convergent sums to convergent products, as Mathlib's HasSum.exp does for complete normed algebras. A continuous derivation differentiates the logarithm series termwise, and the geometric series for u⁻¹ gives u * D (log u) = D u.

Main definitions

• Ideal.expMulEquiv: for an ideal I of topologically nilpotent elements, the exponential as an isomorphism from the additive group of I onto Ideal.principalUnitGroup I, with inverse the logarithm.

Main results

• IsTopologicallyNilpotent.hasSum_exp, IsTopologicallyNilpotent.hasSum_log: convergence of the two series.
• IsTopologicallyNilpotent.exp_sub_one, IsTopologicallyNilpotent.log: exp a - 1 and log (1 + a) are topologically nilpotent.
• IsTopologicallyNilpotent.exp_sub_one_mem, IsTopologicallyNilpotent.log_mem: exp a - 1 and log (1 + a) lie in every ideal containing a.
• IsTopologicallyNilpotent.exp_log, IsTopologicallyNilpotent.log_exp: the two inverse identities.
• IsTopologicallyNilpotent.exp_add, IsTopologicallyNilpotent.log_mul: the functional equations.
• IsTopologicallyNilpotent.hasSum_log_one_sub: log (1 - a) = -∑ aⁿ⁺¹ / (n + 1).
• IsTopologicallyNilpotent.hasSum_log_prod_one_sub: for a finite product ∏_μ (1 - μ a), its logarithm is -∑ₖ (∑_μ μᵏ⁺¹) aᵏ⁺¹ / (k + 1).
• HasSum.exp_of_mem_ideal: inside an ideal of topologically nilpotent elements, the exponential turns convergent sums into convergent products.
• IsTopologicallyNilpotent.mul_derivation_log: a continuous derivation D satisfies u * D (log u) = D u.
• IsTopologicallyNilpotent.map_log: continuous ring homomorphisms commute with the logarithm.

theorem IsTopologicallyNilpotent.hasSum_exp {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {a : S} [Algebra ℚ S] (ha : IsTopologicallyNilpotent a) : HasSum (fun (n : ℕ) => (↑n.factorial)⁻¹ • a ^ n) (NormedSpace.exp a)

For a topologically nilpotent a, the exponential series ∑ aⁿ / n! converges to exp a.

theorem IsTopologicallyNilpotent.hasSum_log {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {u : S} [Algebra ℚ S] (hu : IsTopologicallyNilpotent (u - 1)) : HasSum (fun (n : ℕ) => ((-1) ^ (n + 1) / ↑n) • (u - 1) ^ n) (NormedSpace.log u)

For a topologically nilpotent u - 1, the logarithm series ∑ (-1)ⁿ⁺¹ (u - 1)ⁿ / n converges to log u.

theorem IsTopologicallyNilpotent.exp_sub_one {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {a : S} [Algebra ℚ S] (ha : IsTopologicallyNilpotent a) : IsTopologicallyNilpotent (NormedSpace.exp a - 1)

If a is topologically nilpotent, so is exp a - 1.

theorem IsTopologicallyNilpotent.log {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {u : S} [Algebra ℚ S] (hu : IsTopologicallyNilpotent (u - 1)) : IsTopologicallyNilpotent (NormedSpace.log u)

If u - 1 is topologically nilpotent, so is log u.

theorem IsTopologicallyNilpotent.exp_sub_one_mem {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {a : S} [Algebra ℚ S] (ha : IsTopologicallyNilpotent a) {I : Ideal S} (haI : a ∈ I) : NormedSpace.exp a - 1 ∈ I

exp a - 1 lies in every ideal containing the topologically nilpotent a.

theorem IsTopologicallyNilpotent.log_mem {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {u : S} [Algebra ℚ S] (hu : IsTopologicallyNilpotent (u - 1)) {I : Ideal S} (huI : u - 1 ∈ I) : NormedSpace.log u ∈ I

log u lies in every ideal containing the topologically nilpotent u - 1.

theorem IsTopologicallyNilpotent.exp_log {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {u : S} [Algebra ℚ S] (hu : IsTopologicallyNilpotent (u - 1)) : NormedSpace.exp (NormedSpace.log u) = u

The exponential of the logarithm: exp (log u) = u when u - 1 is topologically nilpotent.

theorem IsTopologicallyNilpotent.log_exp {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {a : S} [Algebra ℚ S] (ha : IsTopologicallyNilpotent a) : NormedSpace.log (NormedSpace.exp a) = a

The logarithm of the exponential: log (exp a) = a when a is topologically nilpotent.

theorem IsTopologicallyNilpotent.exp_add {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {a b : S} [Algebra ℚ S] (ha : IsTopologicallyNilpotent a) (hb : IsTopologicallyNilpotent b) : NormedSpace.exp (a + b) = NormedSpace.exp a * NormedSpace.exp b

The exponential turns sums of topologically nilpotent elements into products.

theorem IsTopologicallyNilpotent.log_mul {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {u v : S} [Algebra ℚ S] (hu : IsTopologicallyNilpotent (u - 1)) (hv : IsTopologicallyNilpotent (v - 1)) : NormedSpace.log (u * v) = NormedSpace.log u + NormedSpace.log v

The logarithm turns products into sums: log (u * v) = log u + log v when u - 1 and v - 1 are topologically nilpotent.

theorem IsTopologicallyNilpotent.hasSum_log_one_sub {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {a : S} [Algebra ℚ S] (ha : IsTopologicallyNilpotent a) : HasSum (fun (n : ℕ) => -((↑(n + 1))⁻¹ • a ^ (n + 1))) (NormedSpace.log (1 - a))

For a topologically nilpotent a, the logarithm of 1 - a is -∑ₙ aⁿ⁺¹ / (n + 1).

theorem IsTopologicallyNilpotent.hasSum_log_prod_one_sub {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {a : S} [Algebra ℚ S] {K : Type u_2} [CommRing K] [Algebra K S] (ha : IsTopologicallyNilpotent a) (s : Multiset K) : HasSum (fun (k : ℕ) => -((↑(k + 1))⁻¹ • (Multiset.map (fun (x : K) => x ^ (k + 1)) s).sum • a ^ (k + 1))) (NormedSpace.log (Multiset.map (fun (μ : K) => 1 - (algebraMap K S) μ * a) s).prod)

For a multiset s of scalars, the logarithm of ∏_{μ ∈ s} (1 - μ a) is -∑ₖ (∑_{μ ∈ s} μᵏ⁺¹) aᵏ⁺¹ / (k + 1).

theorem IsTopologicallyNilpotent.mul_derivation_log {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {u : S} [Algebra ℚ S] {R : Type u_2} [CommSemiring R] [Algebra R S] (D : Derivation R S S) (hD : Continuous ⇑D) (hu : IsTopologicallyNilpotent (u - 1)) : u * D (NormedSpace.log u) = D u

A continuous derivation D differentiates the logarithm as D (log u) = u⁻¹ * D u, in the form u * D (log u) = D u, when u - 1 is topologically nilpotent.

theorem IsTopologicallyNilpotent.map_log {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] {u : S} [Algebra ℚ S] {S' : Type u_2} [CommRing S'] [UniformSpace S'] [IsUniformAddGroup S'] [IsTopologicalRing S'] [IsLinearTopology S' S'] [T2Space S'] [CompleteSpace S'] [Algebra ℚ S'] (hu : IsTopologicallyNilpotent (u - 1)) (ψ : S →+* S') (hψ : Continuous ⇑ψ) : ψ (NormedSpace.log u) = NormedSpace.log (ψ u)

A continuous ring homomorphism ψ commutes with the logarithm: ψ (log u) = log (ψ u) when u - 1 is topologically nilpotent.

theorem HasSum.exp_of_mem_ideal {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] [Algebra ℚ S] {ι : Type u_2} {I : Ideal S} (hI : ∀ a ∈ I, IsTopologicallyNilpotent a) {f : ι → S} {a : S} (h : HasSum f a) (hf : ∀ (i : ι), f i ∈ I) (ha : a ∈ I) : HasProd (NormedSpace.exp ∘ f) (NormedSpace.exp a)

The exponential of a sum is the product of the exponentials. If f has sum a, with all f i and a in an ideal I of topologically nilpotent elements, then exp ∘ f has product exp a.

noncomputable def Ideal.expMulEquiv {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] [Algebra ℚ S] (I : Ideal S) (hI : ∀ a ∈ I, IsTopologicallyNilpotent a) : Multiplicative ↥I ≃* ↥I.principalUnitGroup

Exponential and logarithm: for an ideal I of topologically nilpotent elements, the exponential is an isomorphism from the additive group of I onto its principal unit group, with inverse the logarithm.

@[simp]

theorem Ideal.coe_expMulEquiv_apply {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] [Algebra ℚ S] (I : Ideal S) (hI : ∀ a ∈ I, IsTopologicallyNilpotent a) (a : ↥I) : ↑↑((I.expMulEquiv hI) (Multiplicative.ofAdd a)) = NormedSpace.exp ↑a

Ideal.expMulEquiv sends a to the unit exp a.

@[simp]

theorem Ideal.coe_expMulEquiv_symm_apply {S : Type u_1} [CommRing S] [UniformSpace S] [IsUniformAddGroup S] [IsTopologicalRing S] [IsLinearTopology S S] [T2Space S] [CompleteSpace S] [Algebra ℚ S] (I : Ideal S) (hI : ∀ a ∈ I, IsTopologicallyNilpotent a) (u : ↥I.principalUnitGroup) : ↑(Multiplicative.toAdd ((I.expMulEquiv hI).symm u)) = NormedSpace.log ↑↑u

The inverse of Ideal.expMulEquiv sends a unit u to log u.