GeneralPacketBounds.lean

1 import PaperIRelease.GeneralNormedPackets
2 
3 set_option autoImplicit false
4 noncomputable section
5 open scoped BigOperators
6 
7 namespace Komorebi.PaperIRelease.GeneralNormedPackets
8 namespace ContinuousProjectorFamily
9 
10 variable {𝕜 X Y I : Type*} [NormedField 𝕜]
11 variable [NormedAddCommGroup X] [NormedSpace 𝕜 X]
12 variable [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] [Fintype I]
13 
14 theorem analysis_bound (P : ContinuousProjectorFamily 𝕜 X I)
15     (C : ℝ) (hC : 0 ≤ C) (hb : ∀ i x, ‖P.proj i x‖ ≤ C * ‖x‖) (x : X) :
16     ‖P.analysis x‖ ≤ C * ‖x‖ := by
17   apply (pi_norm_le_iff_of_nonneg (mul_nonneg hC (norm_nonneg x))).mpr
18   intro i
19   exact hb i x
20 
21 theorem synthesis_bound (P : ContinuousProjectorFamily 𝕜 X I)
22     (z : ∀ i, P.packet i) : ‖P.synthesis z‖ ≤ (Fintype.card I : ℝ) * ‖z‖ := by
23   rw [P.synthesis_apply]
24   calc
25     ‖∑ i, (z i : X)‖ ≤ ∑ i, ‖(z i : X)‖ := norm_sum_le _ _
26     _ ≤ ∑ _i : I, ‖z‖ := Finset.sum_le_sum (fun i _ => norm_le_pi_norm z i)
27     _ = (Fintype.card I : ℝ) * ‖z‖ := by simp
28 
29 /-- Finite individual boundedness supplies a single bound for analysis. -/
30 theorem exists_uniform_bound (P : ContinuousProjectorFamily 𝕜 X I)
31     (hb : ∀ i, IsBoundedLinearMap 𝕜 (P.proj i)) :
32     ∃ C : ℝ, 0 ≤ C ∧ ∀ i x, ‖P.proj i x‖ ≤ C * ‖x‖ := by
33   classical
34   choose C hC hbound using fun i => (hb i).bound
35   refine ⟨∑ i, C i, Finset.sum_nonneg (fun i _ => (hC i).le), ?_⟩
36   intro i x
37   exact (hbound i x).trans (mul_le_mul_of_nonneg_right
38     (Finset.single_le_sum (fun j _ => (hC j).le) (Finset.mem_univ i)) (norm_nonneg x))
39 
40 theorem analysis_isBounded (P : ContinuousProjectorFamily 𝕜 X I)
41     (hb : ∀ i, IsBoundedLinearMap 𝕜 (P.proj i)) :
42     IsBoundedLinearMap 𝕜 P.analysis := by
43   obtain ⟨C, hC, h⟩ := P.exists_uniform_bound hb
44   exact P.analysis.toLinearMap.isLinear.with_bound C (P.analysis_bound C hC h)
45 
46 theorem synthesis_isBounded (P : ContinuousProjectorFamily 𝕜 X I) :
47     IsBoundedLinearMap 𝕜 P.synthesis :=
48   P.synthesis.toLinearMap.isLinear.with_bound (Fintype.card I : ℝ) P.synthesis_bound
49 
50 /-- Literal bounded packet maps in every norm equivalent to the canonical
51 finite-product norm, including over trivially valued normed fields. -/
52 theorem equivalent_norm_packet_bounds (P : ContinuousProjectorFamily 𝕜 X I)
53     (hb : ∀ i, IsBoundedLinearMap 𝕜 (P.proj i))
54     (e : (∀ i, P.packet i) ≃ₗ[𝕜] Y)
55     (C D : ℝ) (hC : ∀ z, ‖e z‖ ≤ C * ‖z‖)
56     (hD : ∀ y, ‖e.symm y‖ ≤ D * ‖y‖) :
57     (∀ i, IsClosed (P.packet i : Set X)) ∧
58       IsBoundedLinearMap 𝕜 (fun x => e (P.analysis x)) ∧
59       IsBoundedLinearMap 𝕜 (fun y => P.synthesis (e.symm y)) ∧
60       Function.LeftInverse (fun y => P.synthesis (e.symm y)) (fun x => e (P.analysis x)) ∧
61       Function.RightInverse (fun y => P.synthesis (e.symm y)) (fun x => e (P.analysis x)) := by
62   refine ⟨P.isClosed_packet, ?_, ?_, ?_, ?_⟩
63   · exact (e.toLinearMap.isLinear.with_bound C hC).comp (P.analysis_isBounded hb)
64   · exact P.synthesis_isBounded.comp (e.symm.toLinearMap.isLinear.with_bound D hD)
65   · intro x
66     simp only [e.symm_apply_apply, P.synthesis_analysis]
67   · intro y
68     simp only [P.analysis_synthesis, e.apply_symm_apply]
69 
70 end ContinuousProjectorFamily
71 end Komorebi.PaperIRelease.GeneralNormedPackets

Back to source controls