DyadicDetailExamples.lean

1 import KomorebiSpace.DyadicResidualDetails
2 import KomorebiSpace.ResidualAliasing
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Hidden residual witnesses
8 
9 The previous all-level aliasing candidate retains its full nonzero defect in
10 its hidden-detail coordinate. A separate finite-dimensional block witnesses
11 information in the target-restriction kernel, not just adjacent cancellation.
12 -/
13 noncomputable section
14 namespace KomorebiSpace
15 namespace DyadicDetailExamples
16 open BanachTower
17 open ResidualAliasing
18 
19 /-- Identity target sections for the actual scalar tower. -/
20 def scalarSplitting : Splitting scalar where
21   up _ := ContinuousLinearMap.id ℝ ℝ
22   down_up _ := by apply ContinuousLinearMap.ext; intro x; rfl
23   bound := 1
24   up_bound _ := ContinuousLinearMap.norm_id_le
25 
26 abbrev pairCoarsen := DyadicResidual.coarsen scalar scalar scalar_contractive scalar_contractive
27 abbrev pairHidden := DyadicResidual.hidden scalar scalar scalar_contractive scalar_contractive scalarSplitting
28 abbrev fine := differential scalar scalar candidate
29 
30 theorem alternating_coarse_zero : pairCoarsen fine = 0 := by
31   apply lp.ext
32   funext n
33   rw [DyadicResidual.coarsen_pair, fine_defect_even, fine_defect_odd]
34   apply ContinuousLinearMap.ext
35   intro x
36   change -x + x = 0
37   exact neg_add_cancel _
38 
39 /-- The discarded coordinate is the whole fine residual in this example. -/
40 theorem alternating_hidden_full : pairHidden fine = fine := by
41   rw [DyadicResidual.hidden_apply, alternating_coarse_zero, map_zero, sub_zero]
42 
43 theorem alternating_hidden_norm : ‖pairHidden fine‖ = 1 := by
44   rw [alternating_hidden_full]
45   exact fine_residual_norm
46 
47 theorem alternating_vertical_zero (n : ℕ) :
48     DyadicResidual.innovation scalar scalar scalarSplitting fine n = 0 := by
49   apply ContinuousLinearMap.ext
50   intro x
51   change fine (2*n+1) x - fine (2*n+1) x = 0
52   exact sub_self _
53 
54 /-- Zero coarse data do not erase the incompatibility when the detail is retained. -/
55 theorem alternating_detected : pairCoarsen fine = 0 ∧ pairHidden fine ≠ 0 := by
56   refine ⟨alternating_coarse_zero, ?_⟩
57   intro h
58   have hn := alternating_hidden_norm
59   rw [h, norm_zero] at hn
60   norm_num at hn
61 
62 /- This namespace is a finite block, not an asserted infinite tower. -/
63 namespace BlockKernelWitness
64 
65 def down : (ℝ × ℝ) →L[ℝ] ℝ := ContinuousLinearMap.fst ℝ ℝ ℝ
66 
67 def up : ℝ →L[ℝ] (ℝ × ℝ) := (ContinuousLinearMap.id ℝ ℝ).prod 0
68 
69 def vertical : ℝ →L[ℝ] (ℝ × ℝ) := (0 : ℝ →L[ℝ] ℝ).prod (ContinuousLinearMap.id ℝ ℝ)
70 
71 @[simp] theorem down_up : down.comp up = ContinuousLinearMap.id ℝ ℝ := by apply ContinuousLinearMap.ext; intro x; rfl
72 
73 @[simp] theorem down_vertical : down.comp vertical = 0 := by apply ContinuousLinearMap.ext; intro x; rfl
74 
75 theorem vertical_nonzero : vertical ≠ 0 := by
76   intro h
77   have hc := congrArg (fun f : ℝ →L[ℝ] (ℝ × ℝ) => (f 1).2) h
78   change (1 : ℝ) = 0 at hc
79   norm_num at hc
80 
81 theorem vertical_is_its_innovation : vertical - up.comp (down.comp vertical) = vertical := by
82   rw [down_vertical]
83   simp
84 
85 /-- Coarse data and the even edge alone cannot detect this additional channel. -/
86 theorem coarse_even_insufficient :
87     down.comp vertical = down.comp (0 : ℝ →L[ℝ] (ℝ × ℝ)) ∧ vertical ≠ 0 := by
88   exact ⟨by simp, vertical_nonzero⟩
89 
90 end BlockKernelWitness
91 end DyadicDetailExamples
92 end KomorebiSpace
93 end

Back to source controls