IdentityTowerObstruction.lean

1 import KomorebiSpace.ConstantTower
2 import KomorebiSpace.SplitTowerCoordinates
3 
4 set_option autoImplicit false
5 
6 /-!
7 # A boundary counterexample
8 
9 For identity bonding maps on the reals, the bounded constant residual 1 has
10 no bounded primitive. Thus the tower differential has no right inverse on all
11 bounded residuals. This does not deny the already proved exact repair of
12 bounded candidates preserving their initial value.
13 -/
14 noncomputable section
15 open scoped NNReal ENNReal
16 namespace KomorebiSpace
17 namespace IdentityTowerObstruction
18 open BanachTower
19 
20 abbrev realTower : BanachTower ℝ where
21   Obj _ := ℝ
22   down _ := ContinuousLinearMap.id ℝ ℝ
23   bound := 1
24   down_bound _ := ContinuousLinearMap.norm_id_le
25 
26 def splitting : Splitting realTower where
27   up _ := ContinuousLinearMap.id ℝ ℝ
28   down_up _ := rfl
29   bound := 1
30   up_bound _ := ContinuousLinearMap.norm_id_le
31 
32 theorem propagation_product_one : (splitting.bound : ℝ) * realTower.bound = 1 := by
33   norm_num [splitting, realTower]
34 
35 def unitResidual : Residuals realTower realTower :=
36   ⟨fun _ => ContinuousLinearMap.id ℝ ℝ, memℓp_infty ⟨1, by
37     rintro _ ⟨n, rfl⟩
38     exact ContinuousLinearMap.norm_id_le⟩⟩
39 
40 @[simp] theorem unitResidual_apply (n : ℕ) (x : ℝ) : unitResidual n x = x := rfl
41 
42 /-- A primitive of the unit residual would grow by one at every resolution. -/
43 theorem primitive_growth (f : Candidates realTower realTower)
44     (hf : differential realTower realTower f = unitResidual) (n : ℕ) :
45     f n 1 = f 0 1 + (n : ℝ) := by
46   induction n with
47   | zero => simp
48   | succ n ih =>
49     have h := congrArg (fun r : Residuals realTower realTower => r n 1) hf
50     change f (n+1) 1 - f n 1 = 1 at h
51     rw [Nat.cast_add, Nat.cast_one]
52     linarith
53 
54 /-- This is an infinite mathematical obstruction, not a finite search result. -/
55 theorem no_bounded_primitive :
56     ¬ ∃ f : Candidates realTower realTower, differential realTower realTower f = unitResidual := by
57   rintro ⟨f, hf⟩
58   obtain ⟨n, hn⟩ := exists_nat_gt (‖f‖ - f 0 1)
59   have hb : f n 1 ≤ ‖f‖ := by
60     calc
61       f n 1 ≤ ‖f n 1‖ := le_abs_self _
62       _ ≤ ‖f n‖ * ‖(1 : ℝ)‖ := (f n).le_opNorm 1
63       _ = ‖f n‖ := by simp
64       _ ≤ ‖f‖ := lp.norm_apply_le_norm ENNReal.top_ne_zero f n
65   rw [primitive_growth f hf n] at hb
66   linarith
67 
68 /-- Even an arbitrary function-valued right inverse is impossible in this bounded space. -/
69 theorem no_right_inverse :
70     ¬ ∃ A : Residuals realTower realTower → Candidates realTower realTower,
71       ∀ r, differential realTower realTower (A r) = r := by
72   rintro ⟨A, hA⟩
73   exact no_bounded_primitive ⟨A unitResidual, hA unitResidual⟩
74 
75 /-- Exact repair of candidates and surjectivity onto all residuals are different assertions. -/
76 theorem repair_exists_but_right_inverse_does_not :
77     (∀ f : Candidates realTower realTower, ∃! g : Candidates realTower realTower,
78       Exact realTower realTower g ∧ g 0 = f 0) ∧
79     (¬ ∃ A : Residuals realTower realTower → Candidates realTower realTower,
80       ∀ r, differential realTower realTower (A r) = r) := by
81   exact ⟨fun f => constant_unique_repair f, no_right_inverse⟩
82 
83 end IdentityTowerObstruction
84 end KomorebiSpace
85 end

Back to source controls