Polynomial.lean

1 import KomorebiLSM.Transfer
2 import Mathlib.LinearAlgebra.Multilinear.Basic
3 
4 /-! P5. All ordered cross-packet interactions of each multilinear term
5 are retained; no independent-packet approximation is inserted. -/
6 set_option autoImplicit false
7 open scoped BigOperators
8 namespace Komorebi.LSM
9 universe u v w
10 variable {R : Type u} [CommSemiring R]
11 variable {X : Type v} [AddCommMonoid X] [Module R X]
12 variable {Y : Type w} [AddCommMonoid Y] [Module R Y]
13 
14 theorem multilinear_packet_expansion {I : Type*} [Fintype I] (m : ℕ)
15     (P : I → X →ₗ[R] X) (complete : ∑ i, P i = LinearMap.id)
16     (B : MultilinearMap R (fun _ : Fin m => X) Y) (x : X) :
17     B (fun _ => x) = ∑ f : Fin m → I, B (fun k => P (f k) x) := by
18   classical
19   have h := B.map_sum (fun (_ : Fin m) (i : I) => P i x)
20   simpa only [packet_reconstruction P complete x] using h
21 
22 theorem polynomial_packet_expansion {I : Type*} [Fintype I] (n : ℕ)
23     (P : I → X →ₗ[R] X) (complete : ∑ i, P i = LinearMap.id)
24     (B : (m : Fin n) → MultilinearMap R (fun _ : Fin (m.val + 1) => X) Y)
25     (Q : Y →ₗ[R] Y) (b : Y) (x : X) :
26     Q (b + ∑ m, B m (fun _ => x)) =
27       Q b + ∑ m : Fin n, ∑ f : Fin (m.val + 1) → I,
28         Q (B m (fun k => P (f k) x)) := by
29   classical
30   rw [map_add, map_sum]
31   congr 1
32   apply Finset.sum_congr rfl
33   intro m _
34   rw [multilinear_packet_expansion (m.val + 1) P complete (B m) x, map_sum]
35 
36 end Komorebi.LSM

Back to source controls