source.lean

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

Back to source controls