OperatorEncodingBridge.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.ParameterThetaCompletion
6 
7 namespace Komorebi.PaperIV
8 open scoped PowerSeries
9 noncomputable section
10 variable {R : Type*} [CommRing R]
11 
12 theorem truncatedDifferentialOperator_apply (d : ℕ) (A : R⟦X⟧) (p : Polynomial R) :
13     truncatedDifferentialOperator d A p =
14       ∑ q ∈ Finset.range (d + 1), Polynomial.C (PowerSeries.coeff q A) *
15         Polynomial.derivative^[q] p := by
16   change (Polynomial.eval₂ (algebraMap R (Module.End R (Polynomial R)))
17     Polynomial.derivative (PowerSeries.trunc (d + 1) A)) p = _
18   rw [PowerSeries.eval₂_trunc_eq_sum_range]
19   simp only [LinearMap.sum_apply, Module.End.mul_apply, Module.End.pow_apply,
20     Algebra.algebraMap_eq_smul_one, LinearMap.smul_apply, Module.End.one_apply,
21     Polynomial.smul_eq_C_mul]
22 
23 theorem truncatedDifferentialOperator_egfAction (A : R⟦X⟧) (p : Polynomial R) :
24     truncatedDifferentialOperator p.natDegree A p =
25       egfConstantCoeffAction (fun q => (q.factorial : R) * PowerSeries.coeff q A) p := by
26   rw [truncatedDifferentialOperator_apply, egfConstantCoeffAction]
27   apply Finset.sum_congr rfl
28   intro q _
29   have h := congrFun (Polynomial.factorial_smul_hasseDeriv (R := R) q) p
30   change q.factorial • (Polynomial.hasseDeriv q p) = Polynomial.derivative^[q] p at h
31   rw [← h]
32   simp only [nsmul_eq_mul, map_mul, map_natCast]
33   ring
34 
35 variable [Algebra ℚ R] [Nontrivial R]
36 
37 theorem residueAppell_operator_forward (N j : ℕ) (hN : 0 < N) (r : R) (m : ℕ) :
38     truncatedDifferentialOperator m
39         (PowerSeries.expand N hN.ne' (residuePowerSeries N j r)) (Polynomial.X ^ m) =
40       residueAppellPolynomialParam N j hN r m := by
41   have h := truncatedDifferentialOperator_egfAction
42     (PowerSeries.expand N hN.ne' (residuePowerSeries N j r)) (Polynomial.X ^ m)
43   rw [Polynomial.natDegree_X_pow] at h
44   exact h.trans (egfConstantCoeffAction_residuePowerSeries_X_pow N j hN r m)
45 
46 /-- The actual inverse relation on the named arbitrary-order Appell polynomial.
47 The expanded opposite-order symbol is Phi_(N,j)(X^N)^r. -/
48 theorem residueAppell_operator_inverse (N j : ℕ) (hN : 0 < N) (r : R) (m : ℕ) :
49     truncatedDifferentialOperator m
50         (PowerSeries.expand N hN.ne' (residuePowerSeries N j (-r)))
51         (residueAppellPolynomialParam N j hN r m) = Polynomial.X ^ m := by
52   rw [← residueAppell_operator_forward N j hN r m]
53   exact truncatedDifferentialOperator_residuePowerSeries_inverse N j hN r m
54     (by simp)
55 
56 end
57 end Komorebi.PaperIV

Back to source controls