source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIII.ContinuousPacketJets
6 import Mathlib.Analysis.Calculus.ContDiff.Comp
7 
8 /-!
9 # Finite partition composition of actual packet jets
10 
11 This is the packet expansion of mathlib's iterated Frechet derivative
12 composition theorem. `OrderedFinpartition n` lists the nonempty blocks of a
13 partition in the canonical order of their greatest elements. Every original
14 input slot and every intermediate packet label is retained. No symmetry
15 quotient or unproved combinatorial coefficient is inserted.
16 -/
17 
18 set_option autoImplicit false
19 noncomputable section
20 open scoped BigOperators ContDiff
21 
22 namespace Komorebi.PaperIII.PacketCoordinates
23 universe u v w z i j l
24 variable {K : Type u} [NontriviallyNormedField K]
25 variable {X : Type v} {Y : Type w} {Z : Type z}
26 variable [NormedAddCommGroup X] [NormedSpace K X]
27 variable [NormedAddCommGroup Y] [NormedSpace K Y]
28 variable [NormedAddCommGroup Z] [NormedSpace K Z]
29 variable {I : Type i} {J : Type j} {L : Type l}
30 variable [Fintype I] [Fintype J] [Fintype L]
31 
32 /-- The complete finite partition formula for the literal range jet of a
33 composition, including every intermediate packet label and order zero. -/
34 theorem iteratedPacketJet_comp
35     (P : System K X I) (M : System K Y J) (Q : System K Z L)
36     (hM : ∀ j, Continuous (M.projector j))
37     (hQ : ∀ l, Continuous (Q.projector l))
38     (f : X → Y) (g : Y → Z) (n : Nat) (x : X)
39     (hf : ContDiffAt K n f x) (hg : ContDiffAt K n g (f x))
40     (gamma : L) (alpha : Fin n → I)
41     (xs : (k : Fin n) → LinearMap.range (P.projector (alpha k))) :
42     (iteratedPacketJet P Q hQ (g ∘ f) n x gamma alpha xs : Z) =
43       ∑ c : OrderedFinpartition n, ∑ beta : Fin c.length → J,
44         (iteratedPacketJet M Q hQ g c.length (f x) gamma beta
45           (fun a => iteratedPacketJet P M hM f (c.partSize a) x (beta a)
46             (fun k => alpha (c.emb a k))
47             (fun k => xs (c.emb a k))) : Z) := by
48   classical
49   simp only [iteratedPacketJet_apply_coe]
50   rw [iteratedFDeriv_comp hg hf le_rfl]
51   simp only [FormalMultilinearSeries.taylorComp, sum_apply,
52     FormalMultilinearSeries.compAlongOrderedFinpartition_apply,
53     OrderedFinpartition.applyOrderedFinpartition_apply, ftaylorSeries, map_sum]
54   apply Finset.sum_congr rfl
55   intro c _
56   have expansion := multilinear_input_expansion M
57     (iteratedFDeriv K c.length g (f x)).toMultilinearMap
58     (fun a => iteratedFDeriv K (c.partSize a) f x
59       (fun k => (xs (c.emb a k) : X)))
60   simpa only [map_sum, Function.comp_apply] using
61     congrArg (Q.projector gamma) expansion
62 
63 end Komorebi.PaperIII.PacketCoordinates

Back to source controls