Lean4
theorem exp_add_of_commute {a b : A} (h₁ : Commute a b) (h₂ : IsNilpotent a) (h₃ : IsNilpotent b) :
exp (a + b) = exp a * exp b := by
obtain ⟨n₁, hn₁⟩ := h₂
obtain ⟨n₂, hn₂⟩ := h₃
let N := n₁ ⊔ n₂
have h₄ : a ^ (N + 1) = 0 := pow_eq_zero_of_le (by omega) hn₁
have h₅ : b ^ (N + 1) = 0 := pow_eq_zero_of_le (by omega) hn₂
rw [exp_eq_sum (k := 2 * N + 1) (Commute.add_pow_eq_zero_of_add_le_succ_of_pow_eq_zero h₁ h₄ h₅ (by cutsat)),
exp_eq_sum h₄, exp_eq_sum h₅]
set R2N := range (2 * N + 1) with hR2N
set RN := range (N + 1) with hRN
have s₁ :=
by
calc
∑ i ∈ R2N, (i ! : ℚ)⁻¹ • (a + b) ^ i =
∑ i ∈ R2N, (i ! : ℚ)⁻¹ • ∑ j ∈ range (i + 1), a ^ j * b ^ (i - j) * i.choose j :=
?_
_ = ∑ i ∈ R2N, (∑ j ∈ range (i + 1), ((j ! : ℚ)⁻¹ * ((i - j)! : ℚ)⁻¹) • (a ^ j * b ^ (i - j))) := ?_
_ = ∑ ij ∈ R2N ×ˢ R2N with ij.1 + ij.2 ≤ 2 * N, ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
· refine sum_congr rfl fun i _ ↦ ?_
rw [Commute.add_pow h₁ i]
· simp_rw [smul_sum]
refine sum_congr rfl fun i hi ↦ sum_congr rfl fun j hj ↦ ?_
simp only [mem_range] at hi hj
replace hj := Nat.le_of_lt_succ hj
suffices (i ! : ℚ)⁻¹ * (i.choose j) = ((j ! : ℚ)⁻¹ * ((i - j)! : ℚ)⁻¹)
by
rw [← Nat.cast_commute (i.choose j), ← this, ← mul_smul_comm, ← nsmul_eq_mul, mul_smul, ← smul_assoc, smul_comm,
smul_assoc]
norm_cast
rw [Nat.choose_eq_factorial_div_factorial hj,
Nat.cast_div (Nat.factorial_mul_factorial_dvd_factorial hj) (by positivity)]
simp [field]
· rw [hR2N, sum_sigma']
apply sum_bij (fun ⟨i, j⟩ _ ↦ (j, i - j))
· simp only [mem_sigma, mem_range, mem_filter, mem_product, and_imp]
cutsat
· simp only [mem_sigma, mem_range, Prod.mk.injEq, and_imp]
rintro ⟨x₁, y₁⟩ - h₁ ⟨x₂, y₂⟩ - h₂ h₃ h₄
simp_all
cutsat
· simp only [mem_filter, mem_product, mem_range, mem_sigma, exists_prop, Sigma.exists, and_imp, Prod.forall,
Prod.mk.injEq]
exact fun x y _ _ _ ↦ ⟨x + y, x, by cutsat⟩
· simp only [mem_sigma, mem_range, implies_true]
have z₁ : ∑ ij ∈ R2N ×ˢ R2N with ¬ij.1 + ij.2 ≤ 2 * N, ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0 :=
sum_eq_zero fun i hi ↦ by
rw [mem_filter] at hi
cases le_or_gt (N + 1) i.1 with
| inl h => rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
| inr _ => rw [pow_eq_zero_of_le (by linarith) h₅, mul_zero, smul_zero]
have split₁ :=
sum_filter_add_sum_filter_not (R2N ×ˢ R2N) (fun ij ↦ ij.1 + ij.2 ≤ 2 * N)
(fun ij ↦ ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))
rw [z₁, add_zero] at split₁
rw [split₁] at s₁
have z₂ :
∑ ij ∈ R2N ×ˢ R2N with ¬(ij.1 ≤ N ∧ ij.2 ≤ N), ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) = 0 :=
sum_eq_zero fun i hi ↦ by
simp only [not_and, not_le, mem_filter] at hi
cases le_or_gt (N + 1) i.1 with
| inl h => rw [pow_eq_zero_of_le h h₄, zero_mul, smul_zero]
| inr h => rw [pow_eq_zero_of_le (hi.2 (Nat.le_of_lt_succ h)) h₅, mul_zero, smul_zero]
have split₂ :=
sum_filter_add_sum_filter_not (R2N ×ˢ R2N) (fun ij ↦ ij.1 ≤ N ∧ ij.2 ≤ N)
(fun ij ↦ ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2))
rw [z₂, add_zero] at split₂
rw [← split₂] at s₁
have restrict :
∑ ij ∈ R2N ×ˢ R2N with ij.1 ≤ N ∧ ij.2 ≤ N, ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) =
∑ ij ∈ RN ×ˢ RN, ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) :=
by
apply sum_congr
· ext x
simp only [mem_filter, mem_product, mem_range, hR2N, hRN]
cutsat
· tauto
rw [restrict] at s₁
have s₂ :=
by
calc
(∑ i ∈ RN, (i ! : ℚ)⁻¹ • a ^ i) * ∑ i ∈ RN, (i ! : ℚ)⁻¹ • b ^ i =
∑ i ∈ RN, ∑ j ∈ RN, ((i ! : ℚ)⁻¹ * (j ! : ℚ)⁻¹) • (a ^ i * b ^ j) :=
?_
_ = ∑ ij ∈ RN ×ˢ RN, ((ij.1! : ℚ)⁻¹ * (ij.2! : ℚ)⁻¹) • (a ^ ij.1 * b ^ ij.2) := ?_
· rw [sum_mul_sum]
refine sum_congr rfl fun _ _ ↦ sum_congr rfl fun _ _ ↦ ?_
rw [smul_mul_assoc, mul_smul_comm, smul_smul]
· rw [sum_sigma']
apply sum_bijective (fun ⟨i, j⟩ ↦ (i, j))
· exact ⟨fun ⟨i, j⟩ ⟨i', j'⟩ h ↦ by cases h; rfl, fun ⟨i, j⟩ ↦ ⟨⟨i, j⟩, rfl⟩⟩
· simp only [mem_sigma, mem_product, implies_true]
· simp only [implies_true]
rwa [s₂.symm] at s₁
