SplittingDependence.lean

1 import KomorebiSpace.GrowingTower
2 import KomorebiSpace.SplitTowerCanonicity
3 
4 set_option autoImplicit false
5 
6 /-!
7 # A checked counterexample to splitting-independent repair
8 
9 The same dimension-growing towers admit both zero extension and extension by
10 the first coordinate. Both splittings have norm at most one and the same gap.
11 They yield different exact repairs of the identity candidate, while agreeing
12 at the initial level and on every already-exact candidate.
13 -/
14 noncomputable section
15 open scoped NNReal ENNReal
16 namespace KomorebiSpace
17 namespace SplittingDependence
18 open BanachTower GrowingTower
19 
20 def skewInsertLinear (n : ℕ) : Stage n →ₗ[ℝ] Stage (n+1) where
21   toFun x := Fin.snoc x (x 0)
22   map_add' x y := by
23     funext i
24     refine Fin.lastCases ?_ (fun j => ?_) i <;> simp
25   map_smul' c x := by
26     funext i
27     refine Fin.lastCases ?_ (fun j => ?_) i <;> simp
28 
29 theorem skewInsertLinear_bound (n : ℕ) (x : Stage n) :
30     ‖skewInsertLinear n x‖ ≤ ‖x‖ := by
31   apply (pi_norm_le_iff_of_nonneg (norm_nonneg x)).mpr
32   intro i
33   refine Fin.lastCases ?_ (fun j => ?_) i
34   · simpa [skewInsertLinear] using norm_le_pi_norm x 0
35   · simpa [skewInsertLinear] using norm_le_pi_norm x j
36 
37 def skewInsert (n : ℕ) : Stage n →L[ℝ] Stage (n+1) :=
38   (skewInsertLinear n).mkContinuous 1 (fun x => by simpa using skewInsertLinear_bound n x)
39 
40 @[simp] theorem skewInsert_old (n : ℕ) (x : Stage n) (i : Fin (n+1)) :
41     skewInsert n x i.castSucc = x i := by
42   change (Fin.snoc x (x 0) : Stage (n+1)) i.castSucc = x i
43   simp
44 
45 @[simp] theorem skewInsert_last (n : ℕ) (x : Stage n) :
46     skewInsert n x (Fin.last (n+1)) = x 0 := by
47   change (Fin.snoc x (x 0) : Stage (n+1)) (Fin.last (n+1)) = x 0
48   simp
49 
50 theorem skewInsert_opNorm (n : ℕ) : ‖skewInsert n‖ ≤ 1 :=
51   ContinuousLinearMap.opNorm_le_bound _ zero_le_one
52     (fun x => by simpa only [skewInsert, LinearMap.mkContinuous_apply, one_mul]
53       using skewInsertLinear_bound n x)
54 
55 theorem drop_skewInsert (n : ℕ) :
56     (drop n).comp (skewInsert n) = ContinuousLinearMap.id ℝ (Stage n) := by
57   ext x i
58   simp
59 
60 def skewSplitting : Splitting target where
61   up := skewInsert
62   down_up := drop_skewInsert
63   bound := 1
64   up_bound := skewInsert_opNorm
65 
66 theorem skew_gap : (skewSplitting.bound : ℝ) * source.bound < 1 := by
67   norm_num [skewSplitting, source]
68 
69 def skewRepair : Candidates source target →L[ℝ] Candidates source target :=
70   skewSplitting.repair source skew_gap
71 
72 theorem skewRepair_exact (f : Candidates source target) :
73     Exact source target (skewRepair f) :=
74   skewSplitting.repair_exact source skew_gap f
75 
76 @[simp] theorem skewRepair_seed (f : Candidates source target) : skewRepair f 0 = f 0 :=
77   skewSplitting.repair_preserves_zero source skew_gap f
78 
79 theorem skew_identity_first_new (x : Stage 1) :
80     skewRepair identityCandidate 1 x 1 = x 1 - (1/2 : ℝ) * x 0 := by
81   change x 1 - skewInsert 0 ((differential source target identityCandidate 0 +
82     (0 : Stage 0 →L[ℝ] Stage 0).comp (source.down 0)) x) (Fin.last 1) = _
83   rw [skewInsert_last, identityCandidate_defect]
84   simp [smul_eq_mul]
85 
86 theorem skew_identity_first_old (x : Stage 1) :
87     skewRepair identityCandidate 1 x 0 = (1/2 : ℝ) * x 0 := by
88   change x 0 - skewInsert 0 ((differential source target identityCandidate 0 +
89     (0 : Stage 0 →L[ℝ] Stage 0).comp (source.down 0)) x) 0 = _
90   rw [identityCandidate_defect]
91   simp [skewInsert, skewInsertLinear, drop_apply, smul_eq_mul]
92   ring
93 
94 /-- A concrete inequality of two exact infinite transport families. -/
95 theorem exact_repairs_differ : skewRepair identityCandidate ≠ exactRepair identityCandidate := by
96   intro he
97   have h := congrArg (fun f : Candidates source target => f 1 (fun _ => 1) 1) he
98   rw [skew_identity_first_new, identityRepair_first_new] at h
99   norm_num at h
100 
101 theorem repair_operators_differ : skewRepair ≠ exactRepair := by
102   intro he
103   exact exact_repairs_differ (congrArg (fun T : Candidates source target →L[ℝ]
104     Candidates source target => T identityCandidate) he)
105 
106 /-- The protected-profile subspaces remain literally equal. -/
107 theorem profile_spaces_equal :
108     skewSplitting.semanticSpace source = targetSplitting.semanticSpace source :=
109   skewSplitting.semanticSpace_eq source targetSplitting
110 
111 /-- But the profile values of a nonexact candidate may differ. -/
112 theorem protected_profiles_differ :
113     skewSplitting.observable source identityCandidate ≠
114       targetSplitting.observable source identityCandidate := by
115   intro he
116   have h := congrArg (fun f : Candidates source target => f 1 (fun _ => 1) 1) he
117   change (1 : ℝ) - skewInsert 0 (drop 0 (fun _ => 1)) (Fin.last 1) =
118     1 - GrowingTower.insert 0 (drop 0 (fun _ => 1)) (Fin.last 1) at h
119   rw [skewInsert_last, GrowingTower.insert_last] at h
120   norm_num [drop_apply] at h
121 
122 /-- Different exact retractions onto this common kernel fail to commute. -/
123 theorem repair_operators_do_not_commute :
124     skewRepair.comp exactRepair ≠ exactRepair.comp skewRepair := by
125   intro he
126   apply repair_operators_differ
127   exact (skewSplitting.repairs_commute_iff source targetSplitting skew_gap propagation_gap).mp he
128 
129 /-- The counterexample changes neither the towers nor their norms or the initial operator. -/
130 theorem same_seed_distinct_exact_repairs :
131     Exact source target (skewRepair identityCandidate) ∧
132     Exact source target (exactRepair identityCandidate) ∧
133     skewRepair identityCandidate 0 = exactRepair identityCandidate 0 ∧
134     skewRepair identityCandidate ≠ exactRepair identityCandidate := by
135   refine ⟨skewRepair_exact _, exactRepair_exact _, ?_, exact_repairs_differ⟩
136   rw [skewRepair_seed, exactRepair_seed]
137 
138 end SplittingDependence
139 end KomorebiSpace
140 end

Back to source controls