source.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIII.MultilinearPacketJets
6 import KomorebiPaperIII.BoundedPacketJetNorm
7 import Mathlib.Analysis.Calculus.ContDiff.Defs
8 
9 /-!
10 # Continuous jets on the actual packet ranges
11 
12 The submodule ranges carry their inherited norms. Continuity of each projector
13 upgrades the previously constructed coordinate equivalence to a continuous
14 linear equivalence and makes the ranges closed. The range jet forgets literally
15 to the algebraic packet jet, has its own operator norm, and specializes to
16 mathlib's iterated Frechet derivative. No Taylor or composition formula is
17 assumed or asserted by that specialization.
18 -/
19 
20 set_option autoImplicit false
21 noncomputable section
22 open scoped BigOperators
23 
24 namespace Komorebi.PaperIII.PacketCoordinates
25 universe u v w x y
26 variable {K : Type u} [NontriviallyNormedField K]
27 variable {X : Type v} {Y : Type w}
28 variable [NormedAddCommGroup X] [NormedSpace K X]
29 variable [NormedAddCommGroup Y] [NormedSpace K Y]
30 variable {I : Type x} {J : Type y} [Fintype I] [Fintype J]
31 
32 namespace System
33 
34 /-- A bounded projector with the exact underlying algebraic map. -/
35 def continuousProjector (P : System K X I)
36     (hP : ∀ i, Continuous (P.projector i)) (i : I) : X →L[K] X :=
37   ⟨P.projector i, hP i⟩
38 
39 @[simp] theorem continuousProjector_apply (P : System K X I)
40     (hP : ∀ i, Continuous (P.projector i)) (i : I) (x : X) :
41     P.continuousProjector hP i x = P.projector i x := rfl
42 
43 /-- Every continuous projector has a closed range, identified with its fixed set. -/
44 theorem range_isClosed (P : System K X I)
45     (hP : ∀ i, Continuous (P.projector i)) (i : I) :
46     IsClosed (LinearMap.range (P.projector i) : Set X) := by
47   have hset : (LinearMap.range (P.projector i) : Set X) =
48       {x : X | P.projector i x = x} := by
49     ext x
50     exact P.mem_range_iff_fixed i x
51   rw [hset]
52   exact isClosed_eq (hP i) continuous_id
53 
54 /-- The actual finite packet coordinate equivalence is continuous in both directions. -/
55 def continuousCoordinateEquiv (P : System K X I)
56     (hP : ∀ i, Continuous (P.projector i)) : X ≃L[K] P.Coordinates :=
57   { P.coordinateEquiv with
58     continuous_toFun := continuous_pi (fun i => (hP i).subtype_mk _)
59     continuous_invFun := by
60       change Continuous (fun z : P.Coordinates => ∑ i, (z i : X))
61       exact continuous_finsetSum _
62         (fun i _ => continuous_subtype_val.comp (continuous_apply i)) }
63 
64 @[simp] theorem continuousCoordinateEquiv_apply (P : System K X I)
65     (hP : ∀ i, Continuous (P.projector i)) (x : X) :
66     P.continuousCoordinateEquiv hP x = P.analysis x := rfl
67 
68 @[simp] theorem continuousCoordinateEquiv_symm_apply (P : System K X I)
69     (hP : ∀ i, Continuous (P.projector i)) (z : P.Coordinates) :
70     (P.continuousCoordinateEquiv hP).symm z = P.synthesis z := rfl
71 
72 end System
73 
74 variable {n : Nat}
75 
76 /-- The continuous packet jet has the literal input ranges and output range. -/
77 def continuousPacketJet (P : System K X I) (Q : System K Y J)
78     (hQ : ∀ j, Continuous (Q.projector j))
79     (B : ContinuousMultilinearMap K (fun (_ : Fin n) => X) Y)
80     (gamma : J) (alpha : Fin n → I) :
81     ContinuousMultilinearMap K
82       (fun k : Fin n => LinearMap.range (P.projector (alpha k)))
83       (LinearMap.range (Q.projector gamma)) :=
84   ((Q.continuousProjector hQ gamma).compContinuousMultilinearMap
85     (B.compContinuousLinearMap (fun k =>
86       (LinearMap.range (P.projector (alpha k))).subtypeL))).codRestrict
87     (LinearMap.range (Q.projector gamma))
88     (by
89       intro xs
90       refine ⟨B (fun k => (xs k : X)), ?_⟩
91       rfl)
92 
93 @[simp] theorem continuousPacketJet_apply_coe
94     (P : System K X I) (Q : System K Y J)
95     (hQ : ∀ j, Continuous (Q.projector j))
96     (B : ContinuousMultilinearMap K (fun (_ : Fin n) => X) Y)
97     (gamma : J) (alpha : Fin n → I)
98     (xs : (k : Fin n) → LinearMap.range (P.projector (alpha k))) :
99     (continuousPacketJet P Q hQ B gamma alpha xs : Y) =
100       Q.projector gamma (B (fun k => (xs k : X))) := rfl
101 
102 /-- Forgetting continuity gives exactly the previously defined algebraic jet. -/
103 @[simp] theorem continuousPacketJet_toMultilinearMap
104     (P : System K X I) (Q : System K Y J)
105     (hQ : ∀ j, Continuous (Q.projector j))
106     (B : ContinuousMultilinearMap K (fun (_ : Fin n) => X) Y)
107     (gamma : J) (alpha : Fin n → I) :
108     (continuousPacketJet P Q hQ B gamma alpha).toMultilinearMap =
109       packetJet P Q B.toMultilinearMap gamma alpha := rfl
110 
111 /-- Restriction to the actual input ranges introduces no input projection factors. -/
112 theorem continuousPacketJet_norm_le
113     (P : System K X I) (Q : System K Y J)
114     (hQ : ∀ j, Continuous (Q.projector j))
115     (B : ContinuousMultilinearMap K (fun (_ : Fin n) => X) Y)
116     (gamma : J) (alpha : Fin n → I) :
117     ‖continuousPacketJet P Q hQ B gamma alpha‖ ≤
118       ‖Q.continuousProjector hQ gamma‖ * ‖B‖ := by
119   apply ContinuousMultilinearMap.opNorm_le_bound
120     (mul_nonneg (norm_nonneg _) (norm_nonneg _))
121   intro xs
122   change ‖Q.continuousProjector hQ gamma (B (fun k => (xs k : X)))‖ ≤
123     (‖Q.continuousProjector hQ gamma‖ * ‖B‖) * ∏ k, ‖xs k‖
124   calc
125     _ ≤ ‖Q.continuousProjector hQ gamma‖ *
126         ‖B (fun k => (xs k : X))‖ :=
127       (Q.continuousProjector hQ gamma).le_opNorm _
128     _ ≤ ‖Q.continuousProjector hQ gamma‖ *
129         (‖B‖ * ∏ k, ‖(xs k : X)‖) :=
130       mul_le_mul_of_nonneg_left (B.le_opNorm _) (norm_nonneg _)
131     _ = _ := by simp only [mul_assoc]; rfl
132 
133 /-- Continuous range jets reconstruct the given continuous multilinear map. -/
134 theorem continuous_multilinear_packet_reconstruction
135     (P : System K X I) (Q : System K Y J)
136     (hQ : ∀ j, Continuous (Q.projector j))
137     (B : ContinuousMultilinearMap K (fun (_ : Fin n) => X) Y)
138     (h : Fin n → X) :
139     B h = ∑ gamma : J, ∑ alpha : Fin n → I,
140       (continuousPacketJet P Q hQ B gamma alpha
141         (fun k => P.analysis (h k) (alpha k)) : Y) :=
142   multilinear_packet_reconstruction P Q B.toMultilinearMap h
143 
144 /-- A packet jet of mathlib's actual chosen iterated Frechet derivative. -/
145 def iteratedPacketJet (P : System K X I) (Q : System K Y J)
146     (hQ : ∀ j, Continuous (Q.projector j)) (f : X → Y)
147     (n : Nat) (x : X) (gamma : J) (alpha : Fin n → I) :=
148   continuousPacketJet P Q hQ (iteratedFDeriv K n f x) gamma alpha
149 
150 @[simp] theorem iteratedPacketJet_apply_coe
151     (P : System K X I) (Q : System K Y J)
152     (hQ : ∀ j, Continuous (Q.projector j)) (f : X → Y)
153     (n : Nat) (x : X) (gamma : J) (alpha : Fin n → I)
154     (xs : (k : Fin n) → LinearMap.range (P.projector (alpha k))) :
155     (iteratedPacketJet P Q hQ f n x gamma alpha xs : Y) =
156       Q.projector gamma (iteratedFDeriv K n f x (fun k => (xs k : X))) := rfl
157 
158 /-- Exact reconstruction of each chosen iterated Frechet derivative, including order zero.
159 This identity does not assert differentiability of an arbitrary supplied function. -/
160 theorem iteratedFDeriv_packet_reconstruction
161     (P : System K X I) (Q : System K Y J)
162     (hQ : ∀ j, Continuous (Q.projector j)) (f : X → Y)
163     (n : Nat) (x : X) (h : Fin n → X) :
164     iteratedFDeriv K n f x h = ∑ gamma : J, ∑ alpha : Fin n → I,
165       (iteratedPacketJet P Q hQ f n x gamma alpha
166         (fun k => P.analysis (h k) (alpha k)) : Y) :=
167   continuous_multilinear_packet_reconstruction P Q hQ (iteratedFDeriv K n f x) h
168 
169 /-- The norm estimate applies to the actual iterated derivative range jet. -/
170 theorem iteratedPacketJet_norm_le
171     (P : System K X I) (Q : System K Y J)
172     (hQ : ∀ j, Continuous (Q.projector j)) (f : X → Y)
173     (n : Nat) (x : X) (gamma : J) (alpha : Fin n → I) :
174     ‖iteratedPacketJet P Q hQ f n x gamma alpha‖ ≤
175       ‖Q.continuousProjector hQ gamma‖ * ‖iteratedFDeriv K n f x‖ :=
176   continuousPacketJet_norm_le P Q hQ (iteratedFDeriv K n f x) gamma alpha
177 
178 end Komorebi.PaperIII.PacketCoordinates

Back to source controls