ScheduleNormObstruction.lean

1 import KomorebiSpace.BanachReindexing
2 import Mathlib.Tactic.NormNum
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Cofinal schedule invariance is not sup-norm invariance
8 
9 An actual exact transport on constant real Banach stages has level maps 2^(-n) id.
10 Sampling n+1 is cofinal but changes its candidate sup norm from 1 to 1/2.
11 Both bonding maps are surjective. The phenomenon is not an empty-limit artifact.
12 -/
13 
14 noncomputable section
15 open scoped NNReal ENNReal
16 namespace KomorebiSpace
17 namespace ScheduleNormObstruction
18 open BanachTower
19 
20 abbrev source : BanachTower ℝ where
21   Obj _ := ℝ
22   down _ := (1/2 : ℝ) • ContinuousLinearMap.id ℝ ℝ
23   bound := 1/2
24   down_bound _ := by norm_num [norm_smul, ContinuousLinearMap.norm_id]
25 
26 abbrev target : BanachTower ℝ where
27   Obj _ := ℝ
28   down _ := ContinuousLinearMap.id ℝ ℝ
29   bound := 1
30   down_bound _ := ContinuousLinearMap.norm_id_le
31 
32 def levelMap (n : ℕ) : ℝ →L[ℝ] ℝ :=
33   ((1/2 : ℝ)^n) • ContinuousLinearMap.id ℝ ℝ
34 
35 @[simp] theorem levelMap_norm (n : ℕ) : ‖levelMap n‖ = (1/2 : ℝ)^n := by
36   rw [levelMap, norm_smul, ContinuousLinearMap.norm_id, mul_one]
37   exact Real.norm_of_nonneg (pow_nonneg (by norm_num) n)
38 
39 theorem levelMap_bound (n : ℕ) : ‖levelMap n‖ ≤ 1 := by
40   rw [levelMap_norm]
41   exact pow_le_one₀ (by norm_num) (by norm_num)
42 
43 def geometricCandidate : Candidates source target :=
44   ⟨levelMap, memℓp_infty ⟨1, by
45     rintro _ ⟨n, rfl⟩
46     exact levelMap_bound n⟩⟩
47 
48 theorem geometricCandidate_exact : Exact source target geometricCandidate := by
49   intro n
50   apply ContinuousLinearMap.ext
51   intro x
52   change (1/2 : ℝ)^(n+1) * x = (1/2 : ℝ)^n * ((1/2 : ℝ) * x)
53   rw [pow_succ, mul_assoc]
54 
55 theorem geometricCandidate_norm : ‖geometricCandidate‖ = 1 := by
56   apply le_antisymm
57   · exact lp.norm_le_of_forall_le (by norm_num) levelMap_bound
58   · have h := lp.norm_apply_le_norm ENNReal.top_ne_zero geometricCandidate 0
59     change ‖levelMap 0‖ ≤ ‖geometricCandidate‖ at h
60     simpa only [levelMap_norm, pow_zero] using h
61 
62 def sampledCandidate : Candidates source target := (1/2 : ℝ) • geometricCandidate
63 
64 /-- This is exactly the levelwise subsequence, not an unrelated rescaling. -/
65 theorem sampledCandidate_coordinate (n : ℕ) :
66     sampledCandidate n = geometricCandidate (n+1) := by
67   apply ContinuousLinearMap.ext
68   intro x
69   change (1/2 : ℝ) * ((1/2 : ℝ)^n * x) = (1/2 : ℝ)^(n+1) * x
70   rw [pow_succ]
71   ring
72 
73 theorem sampledCandidate_exact : Exact source target sampledCandidate := by
74   intro n
75   rw [sampledCandidate_coordinate, sampledCandidate_coordinate]
76   exact geometricCandidate_exact (n+1)
77 
78 theorem sampledCandidate_norm : ‖sampledCandidate‖ = (1/2 : ℝ) := by
79   rw [sampledCandidate, norm_smul, geometricCandidate_norm]
80   norm_num
81 
82 theorem cofinal_sampling_changes_norm :
83     ‖geometricCandidate‖ ≠ ‖sampledCandidate‖ := by
84   rw [geometricCandidate_norm, sampledCandidate_norm]
85   norm_num
86 
87 theorem source_down_surjective (n : ℕ) : Function.Surjective (source.down n) := by
88   intro x
89   refine ⟨2*x, ?_⟩
90   change (1/2 : ℝ) * (2*x) = x
91   ring
92 
93 theorem target_down_surjective (n : ℕ) : Function.Surjective (target.down n) := by
94   intro x
95   exact ⟨x, rfl⟩
96 
97 end ScheduleNormObstruction
98 end KomorebiSpace
99 end

Back to source controls