CompactReciprocal.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ReciprocalCompletion
6 
7 namespace Komorebi.PaperIV
8 noncomputable section
9 variable {K : Type*} [Field K] [CharZero K]
10 
11 private theorem ordinary_low_equations (N : ℕ) (r : K) :
12     reciprocalOrdCoeff N 1 r = r / (N.factorial : K) ∧
13     2 * reciprocalOrdCoeff N 2 r =
14       r * (r + 1) / (N.factorial : K)^2 - 2*r / ((2*N).factorial : K) ∧
15     6 * reciprocalOrdCoeff N 3 r =
16       r*(r+1)*(r+2)/(N.factorial : K)^3 -
17       6*r*(r+1)/((N.factorial : K)*((2*N).factorial : K)) +
18       6*r/((3*N).factorial : K) := by
19   have h0 := reciprocalOrdCoeff_parameter_equation N 0 r
20   have h1 := reciprocalOrdCoeff_parameter_equation N 1 r
21   have h2 := reciprocalOrdCoeff_parameter_equation N 2 r
22   have hb : reciprocalOrdCoeff N 0 r = 1 := by simp [reciprocalOrdCoeff]
23   norm_num [Finset.Nat.antidiagonal_succ, Finset.Nat.antidiagonal_zero,
24     coeff_reducedDenominator, hb, eq_ratCast, Nat.mul_comm N] at h0 h1 h2
25   constructor
26   · linear_combination h0
27   constructor
28   · linear_combination h1 + (r+1)/(N.factorial : K)*h0
29   · linear_combination 2*h2 + (r+2)/(N.factorial : K)*h1 +
30       ((r+1)*(r+2)/(N.factorial : K)^2 - (4*r+2)/((2*N).factorial : K))*h0
31 
32 theorem reciprocalCoeff_two_compact {N : ℕ} (hN : 0 < N) (r : K) :
33     reciprocalCoeff N 2 r =
34       r * (((2*N).choose N : K) / 2 * (r+1) - 1) := by
35   have h := (ordinary_low_equations N r).2.1
36   change 2 * PowerSeries.coeff 2 (reciprocalSeries N r) = _ at h
37   rw [reciprocalCoeff, blockCoeff, Nat.mul_comm N 2,
38     Nat.cast_choose K (show N ≤ 2*N by omega), show 2*N-N=N by omega]
39   have hf : ((2*N).factorial : K) ≠ 0 := by exact_mod_cast (2*N).factorial_ne_zero
40   have hg : (N.factorial : K) ≠ 0 := by exact_mod_cast N.factorial_ne_zero
41   field_simp at h ⊢
42   linear_combination h
43 
44 theorem reciprocalCoeff_three_compact {N : ℕ} (hN : 0 < N) (r : K) :
45     reciprocalCoeff N 3 r =
46       r * (((3*N).factorial : K)/(6*(N.factorial : K)^3)*(r+1)*(r+2) -
47         ((3*N).choose N : K)*(r+1)+1) := by
48   have h := (ordinary_low_equations N r).2.2
49   change 6 * PowerSeries.coeff 3 (reciprocalSeries N r) = _ at h
50   rw [reciprocalCoeff, blockCoeff, Nat.mul_comm N 3,
51     Nat.cast_choose K (show N ≤ 3*N by omega), show 3*N-N=2*N by omega]
52   have hf : ((3*N).factorial : K) ≠ 0 := by exact_mod_cast (3*N).factorial_ne_zero
53   have hg : (N.factorial : K) ≠ 0 := by exact_mod_cast N.factorial_ne_zero
54   have hh : ((2*N).factorial : K) ≠ 0 := by exact_mod_cast (2*N).factorial_ne_zero
55   field_simp at h ⊢
56   linear_combination h
57 
58 end
59 end Komorebi.PaperIV

Back to source controls