BoundedPacketJetNorm.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 
5 SECTION 17 BOUNDED AMBIENT JET ESTIMATE.
6 Compiled with the pinned Lean compiler in the release verification.
7 This proves the ambient extension inequality. The literal submodule-range
8 norm comparison is proved separately in ContinuousPacketJets.lean.
9 -/
10 import Mathlib.Analysis.Normed.Module.Multilinear.Basic
11 
12 set_option autoImplicit false
13 noncomputable section
14 open scoped BigOperators
15 
16 namespace Komorebi.PaperIII.BoundedJet
17 
18 universe u v w
19 variable {K : Type u} [NontriviallyNormedField K]
20 variable {X : Type v} {Y : Type w}
21 variable [SeminormedAddCommGroup X] [NormedSpace K X]
22 variable [SeminormedAddCommGroup Y] [NormedSpace K Y]
23 variable {n : Nat}
24 
25 /-- Bounded ambient packet jet: input projections followed by an arbitrary
26     continuous multilinear map and an output projection. -/
27 def projectedJet (Q : Y →L[K] Y)
28     (P : Fin n → X →L[K] X)
29     (B : ContinuousMultilinearMap K (fun (_ : Fin n) => X) Y) :
30     ContinuousMultilinearMap K (fun (_ : Fin n) => X) Y :=
31   Q.compContinuousMultilinearMap (B.compContinuousLinearMap P)
32 
33 /-- The exact norm inequality for the projected ambient jet. This uses the
34     standard norm estimates for composition of continuous multilinear maps
35     with bounded input and output maps. -/
36 theorem projectedJet_norm_le (Q : Y →L[K] Y)
37     (P : Fin n → X →L[K] X)
38     (B : ContinuousMultilinearMap K (fun (_ : Fin n) => X) Y) :
39     ‖projectedJet Q P B‖ ≤ ‖Q‖ * ‖B‖ * ∏ k, ‖P k‖ := by
40   have houtput :
41       ‖Q.compContinuousMultilinearMap (B.compContinuousLinearMap P)‖ ≤
42         ‖Q‖ * ‖B.compContinuousLinearMap P‖ :=
43     ContinuousLinearMap.norm_compContinuousMultilinearMap_le Q _
44   have hinput :
45       ‖B.compContinuousLinearMap P‖ ≤ ‖B‖ * ∏ k, ‖P k‖ :=
46     ContinuousMultilinearMap.norm_compContinuousLinearMap_le B P
47   calc
48     ‖projectedJet Q P B‖ ≤ ‖Q‖ * ‖B.compContinuousLinearMap P‖ := houtput
49     _ ≤ ‖Q‖ * (‖B‖ * ∏ k, ‖P k‖) :=
50         mul_le_mul_of_nonneg_left hinput (norm_nonneg _)
51     _ = ‖Q‖ * ‖B‖ * ∏ k, ‖P k‖ := by ring
52 
53 end Komorebi.PaperIII.BoundedJet

Back to source controls