The complex exponential and subset sums

Properties of t ↦ exp(-(t · x)) and the expansion of ∏ (1 + exp x) over a multiset of roots into zero- and nonzero-sum subset contributions, the analytic heart of Niven's proof of the transcendence of π.

theorem cexp_mul_cexp_neg (x : ℂ) : Complex.exp x * Complex.exp (-x) = 1

For x ∈ ℂ, one has exp(x) * exp(-x) = 1.

theorem continuousWithinAt_exp_neg_mul (x : ℂ) (t : ℝ) : ContinuousWithinAt (fun (t : ℝ) => Complex.exp (-(↑t * x))) (Set.uIcc 0 1) t

For x ∈ ℂ, the map t ↦ exp(-(t * x)) is continuous on [0, 1] at t.

theorem deriv_exp_neg_mul_real (x : ℂ) (t : ℝ) : deriv (fun (t : ℝ) => Complex.exp (-(↑t * x))) t = -x * Complex.exp (-(↑t * x))

For t ∈ ℝ and x ∈ ℂ, it holds that d/dt exp(-(t * x)) = -x * exp(-(t * x)).

theorem norm_cexp_neg_mul_le_exp_norm (a : ℂ) (t : ℝ) : t ∈ Set.uIcc 0 1 → ‖Complex.exp (-(↑t * a))‖ ≤ Real.exp ‖a‖

For a ∈ ℂ and t ∈ [0, 1], one has ‖exp(-(t * a))‖ ≤ exp(‖a‖).

theorem prod_one_add_cexp_aroots_eq_zero (P : Polynomial ℚ) (hP : P ≠ 0) (hroot : (Polynomial.aeval (↑Real.pi * Complex.I)) P = 0) : (Multiset.map (fun (x : ℂ) => 1 + Complex.exp x) (P.aroots ℂ)).prod = 0

If P(π i) = 0 and P ≠ 0, then ∏_{x ∈ roots(P)} (1 + e^x) = 0.

noncomputable def cexpMultisetSum : Multiset ℂ → ℂ

The map t ↦ e^(∑_{x ∈ t} x) on multisets of complex numbers.

Equations

• cexpMultisetSum t = Complex.exp t.sum

noncomputable def zeroSumPowerset (s : Multiset ℂ) : Multiset (Multiset ℂ)

The submultisets t ⊆ s with ∑_{x ∈ t} x = 0.

Equations

• zeroSumPowerset s = Multiset.filter (fun (x : Multiset ℂ) => x.sum = 0) s.powerset

noncomputable def nonZeroSumPowerset (s : Multiset ℂ) : Multiset (Multiset ℂ)

The submultisets t ⊆ s with ∑_{x ∈ t} x ≠ 0.

Equations

• nonZeroSumPowerset s = Multiset.filter (fun (x : Multiset ℂ) => x.sum ≠ 0) s.powerset

theorem sum_cexp_powerset_split (s : Multiset ℂ) : (Multiset.map cexpMultisetSum s.powerset).sum = (Multiset.map cexpMultisetSum (zeroSumPowerset s)).sum + (Multiset.map cexpMultisetSum (nonZeroSumPowerset s)).sum

The sum ∑_{t ⊆ s} e^(∑_{x ∈ t} x) splits into the zero-sum and nonzero-sum parts.

theorem prod_one_add_cexp_split (s : Multiset ℂ) : (Multiset.map (fun (x : ℂ) => 1 + Complex.exp x) s).prod = (Multiset.map cexpMultisetSum (zeroSumPowerset s)).sum + (Multiset.map cexpMultisetSum (nonZeroSumPowerset s)).sum

The product ∏_{x ∈ s} (1 + e^x) equals to ∑_{t ⊆ s, ∑_{y ∈ t} y = 0} e^(∑_{y ∈ t} y) + ∑_{t ⊆ s, ∑_{y ∈ t} y ≠ 0} e^(∑_{y ∈ t} y).

def subsetSums {α : Type u_1} [AddCommMonoid α] (s : Multiset α) : Multiset α

The multiset of all subset sums of s, i.e. { ∑_{x ∈ t} x | t ⊆ s }.

Equations

• subsetSums s = Multiset.map Multiset.sum s.powerset

def nonzeroSubsetSums {α : Type u_1} [AddCommMonoid α] [DecidableEq α] (s : Multiset α) : Multiset α

The multiset of all nonzero subset sums of s, i.e. { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }.

Equations

• nonzeroSubsetSums s = Multiset.filter (fun (x : α) => x ≠ 0) (subsetSums s)

theorem ne_zero_of_mem_nonzeroSubsetSums {α : Type u_1} [AddCommMonoid α] [DecidableEq α] {s : Multiset α} {x : α} (hx : x ∈ nonzeroSubsetSums s) : x ≠ 0

Every element of { ∑_{x ∈ t} x ≠ 0 | t ⊆ s } is nonzero.

theorem mem_nonzeroSubsetSums_of_mem_of_ne_zero {α : Type u_1} [AddCommMonoid α] [DecidableEq α] {s : Multiset α} {x : α} (hx : x ∈ s) (hx0 : x ≠ 0) : x ∈ nonzeroSubsetSums s

If x ∈ s and x ≠ 0, then x ∈ { ∑_{x ∈ t} x ≠ 0 | t ⊆ s }.

theorem cexpMultisetSum_eq_one_of_mem_zeroSumPowerset {s t : Multiset ℂ} (ht : t ∈ zeroSumPowerset s) : cexpMultisetSum t = 1

If t ⊆ s and ∑_{x ∈ t} x = 0, then e^(∑_{x ∈ t} x) = 1.

theorem map_cexpMultisetSum_zeroSumPowerset_eq_replicate (s : Multiset ℂ) : Multiset.map cexpMultisetSum (zeroSumPowerset s) = Multiset.replicate (zeroSumPowerset s).card 1

Applying t ↦ e^(∑_{x ∈ t} x) to all t ⊆ s with ∑_{x ∈ t} x = 0 gives only 1s.

theorem sum_cexp_zeroSumPowerset_eq_count_zero_subsetSums (s : Multiset ℂ) : (Multiset.map cexpMultisetSum (zeroSumPowerset s)).sum = ↑↑(Multiset.count 0 (subsetSums s))

The sum ∑_{t ⊆ s, ∑_{x ∈ t} x = 0} e^(∑_{x ∈ t} x) equals #{t ⊆ s | ∑_{x ∈ t} x = 0}.

theorem sum_cexp_subsetSums_aroots_filter_ne_zero_eq_neg_count_zero (B : Polynomial ℚ) (hB : B ≠ 0) (hroot : (Polynomial.aeval (↑Real.pi * Complex.I)) B = 0) : (Multiset.map Complex.exp (nonzeroSubsetSums (B.aroots ℂ))).sum = -↑(Multiset.count 0 (subsetSums (B.aroots ℂ)))

If B(π i) = 0 and roots(B) is the multiset of roots of B, then ∑_{t ⊆ roots(B), ∑_{x ∈ t} x ≠ 0} e^(∑_{x ∈ t} x) = -#{t ⊆ roots(B) | ∑_{x ∈ t} x = 0}.

theorem continuousOn_exp_neg_mul_iteratedDeriv_sub (f : ℂ → ℂ) (x : ℂ) (n : ℕ) (hderiv : ∀ k ≤ n, ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : ContinuousOn (fun (t : ℝ) => x * Complex.exp (-(↑t * x)) * (iteratedDeriv n f (↑t * x) - f (↑t * x))) (Set.uIcc 0 1)

If f⁽ᵏ⁾ is differentiable at t * x for every k ≤ n and every t ∈ [0, 1], then t ↦ exp(-t * x) * ( f⁽ⁿ⁾(t * x) - f(t * x) ) is continuous on [0, 1].

theorem differentiableAt_exp_neg_mul_sum_iteratedDeriv (f : ℂ → ℂ) (x : ℂ) (n : ℕ) (t : ℝ) (hderiv : ∀ k ≤ n, DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : DifferentiableAt ℝ (fun (t : ℝ) => Complex.exp (-(↑t * x)) * ∑ k ∈ Finset.range (n + 1), iteratedDeriv k f (↑t * x)) t

If f⁽ᵏ⁾ is differentiable at t x for every k ≤ n, then t ↦ exp(-t * x) * ∑ₖ₌₀ⁿ⁺¹ f⁽ᵏ⁾(t * x) is differentiable at t.

theorem deriv_exp_neg_mul_sum_iteratedDeriv (f : ℂ → ℂ) (x : ℂ) (n : ℕ) (t : ℝ) (hderiv : ∀ k ≤ n, DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : deriv (fun (t : ℝ) => Complex.exp (-(↑t * x)) * ∑ k ∈ Finset.range (n + 1), iteratedDeriv k f (↑t * x)) t = x * Complex.exp (-(↑t * x)) * (iteratedDeriv (n + 1) f (↑t * x) - f (↑t * x))

If f⁽ᵏ⁾ is differentiable at t x for every k ≤ n, then with hasDeriv we have d/dt (exp(-t * x) * ∑ₖ₌₀ⁿ⁺¹ f⁽ᵏ⁾(t * x)) = x * exp(- t * x) * (f⁽ⁿ⁺¹⁾(t * x) - f(t * x)).

theorem hasDerivAt_exp_neg_mul_sum_iteratedDeriv (f : ℂ → ℂ) (x : ℂ) (n : ℕ) (t : ℝ) (hderiv : ∀ k ≤ n, DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : HasDerivAt (fun (t : ℝ) => Complex.exp (-(↑t * x)) * ∑ k ∈ Finset.range (n + 1), iteratedDeriv k f (↑t * x)) (x * Complex.exp (-(↑t * x)) * (iteratedDeriv (n + 1) f (↑t * x) - f (↑t * x))) t

If f⁽ᵏ⁾ is differentiable at t x for every k ≤ n, then with deriv we have d/dt (exp(-t * x) * ∑ₖ₌₀ⁿ⁺¹ f⁽ᵏ⁾(t * x)) = x * exp(- t * x) * (f⁽ⁿ⁺¹⁾(t * x) - f(t * x)).

theorem int_exp_neg_mul_fun (f : ℂ → ℂ) (x : ℂ) (n : ℕ) (hderiv : ∀ k ≤ n + 1, ∀ t ∈ Set.uIcc 0 1, DifferentiableAt ℂ (iteratedDeriv k f) (↑t * x)) : ∫ (t : ℝ) in 0..1, (fun (t : ℝ) => x * Complex.exp (-(↑t * x)) * (iteratedDeriv (n + 1) f (↑t * x) - f (↑t * x))) t = Complex.exp (-x) * ∑ k ∈ Finset.range (n + 1), iteratedDeriv k f x - ∑ k ∈ Finset.range (n + 1), iteratedDeriv k f 0

If f⁽ᵏ⁾ is differentiable at t x for every k ≤ n + 1 and every t ∈ [0, 1], then ∫₀¹ x * exp(-t x) * (f⁽ⁿ⁺¹⁾(t x) - f(t x)) dt = exp(- x) * ∑ₖ₌₀ⁿ f⁽ᵏ⁾(x) - ∑ₖ₌₀ⁿ f⁽ᵏ⁾(0).

theorem sum_weighted_cexp_nonzeroSubsetSums_eq_neg_count_zero_subsetSums {n : ℕ} (B : Polynomial ℚ) (hB : B ≠ 0) (hroot : (Polynomial.aeval (↑Real.pi * Complex.I)) B = 0) (a : Fin n → ℂ) (ha : nonzeroSubsetSums (B.aroots ℂ) = valuesFin a) (b : Fin n → ℂ) (hb : ∀ (i : Fin n), b i = 1) (k : ℕ) (hk : k = Multiset.count 0 (subsetSums (B.aroots ℂ))) : ∑ i : Fin n, b i * Complex.exp (a i) = -↑k

If a₀, …, aₙ₋₁ enumerate the nonzero subset sums of the roots of B and bᵢ = 1 for all i, then ∑ᵢ bᵢ exp(aᵢ) = -k.