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_def, ContinuousMultilinearMap.coe_coe] using
61     congrArg (Q.projector gamma) expansion
62 
63 /-- A composite jet vanishes when every labelled partition has a zero outer
64 jet or at least one zero inner jet. This is a sufficient vanishing condition. -/
65 theorem iteratedPacketJet_comp_eq_zero_of
66     (P : System K X I) (M : System K Y J) (Q : System K Z L)
67     (hM : ∀ j, Continuous (M.projector j))
68     (hQ : ∀ l, Continuous (Q.projector l))
69     (f : X → Y) (g : Y → Z) (n : Nat) (x : X)
70     (hf : ContDiffAt K n f x) (hg : ContDiffAt K n g (f x))
71     (gamma : L) (alpha : Fin n → I)
72     (hvanish : ∀ c : OrderedFinpartition n, ∀ beta : Fin c.length → J,
73       iteratedPacketJet M Q hQ g c.length (f x) gamma beta = 0 ∨
74         ∃ a : Fin c.length,
75           iteratedPacketJet P M hM f (c.partSize a) x (beta a)
76             (fun k => alpha (c.emb a k)) = 0) :
77     iteratedPacketJet P Q hQ (g ∘ f) n x gamma alpha = 0 := by
78   classical
79   apply ContinuousMultilinearMap.ext
80   intro xs
81   apply Subtype.ext
82   change (iteratedPacketJet P Q hQ (g ∘ f) n x gamma alpha xs : Z) = 0
83   rw [iteratedPacketJet_comp P M Q hM hQ f g n x hf hg gamma alpha xs]
84   apply Finset.sum_eq_zero
85   intro c _
86   apply Finset.sum_eq_zero
87   intro beta _
88   rcases hvanish c beta with houter | ⟨a, hinner⟩
89   · simp only [houter, zero_apply, Submodule.coe_zero]
90   · have harg :
91         iteratedPacketJet P M hM f (c.partSize a) x (beta a)
92           (fun k => alpha (c.emb a k)) (fun k => xs (c.emb a k)) = 0 := by
93       rw [hinner]
94       rfl
95     exact congrArg (fun z : LinearMap.range (Q.projector gamma) => (z : Z))
96       ((iteratedPacketJet M Q hQ g c.length (f x) gamma beta).map_coord_zero a harg)
97 
98 /-- Nonzero composite-jet support is contained in the structural partition
99 support. Cancellation can prevent the converse, which is not asserted. -/
100 theorem iteratedPacketJet_comp_support
101     (P : System K X I) (M : System K Y J) (Q : System K Z L)
102     (hM : ∀ j, Continuous (M.projector j))
103     (hQ : ∀ l, Continuous (Q.projector l))
104     (f : X → Y) (g : Y → Z) (n : Nat) (x : X)
105     (hf : ContDiffAt K n f x) (hg : ContDiffAt K n g (f x))
106     (gamma : L) (alpha : Fin n → I)
107     (hnonzero : iteratedPacketJet P Q hQ (g ∘ f) n x gamma alpha ≠ 0) :
108     ∃ c : OrderedFinpartition n, ∃ beta : Fin c.length → J,
109       iteratedPacketJet M Q hQ g c.length (f x) gamma beta ≠ 0 ∧
110         ∀ a : Fin c.length,
111           iteratedPacketJet P M hM f (c.partSize a) x (beta a)
112             (fun k => alpha (c.emb a k)) ≠ 0 := by
113   classical
114   by_contra hex
115   apply hnonzero
116   apply iteratedPacketJet_comp_eq_zero_of P M Q hM hQ f g n x hf hg gamma alpha
117   intro c beta
118   by_cases houter : iteratedPacketJet M Q hQ g c.length (f x) gamma beta = 0
119   · exact Or.inl houter
120   · right
121     have hnot : ¬ ∀ a : Fin c.length,
122         iteratedPacketJet P M hM f (c.partSize a) x (beta a)
123           (fun k => alpha (c.emb a k)) ≠ 0 := by
124       intro hall
125       exact hex ⟨c, beta, houter, hall⟩
126     obtain ⟨a, ha⟩ := not_forall.mp hnot
127     exact ⟨a, not_not.mp ha⟩
128 
129 end Komorebi.PaperIII.PacketCoordinates

Back to source controls