BoundedParity.lean

1 import Mathlib.Analysis.Normed.Lp.lpSpace
2 import Mathlib.Analysis.Normed.Operator.NormedSpace
3 
4 set_option autoImplicit false
5 
6 /-!
7 # Exact parity coordinates for a bounded dependent family
8 
9 The even and odd families retain every coordinate. The product norm is the
10 maximum norm. No finiteness or uniform dimension of the fibers is assumed.
11 -/
12 universe u v
13 noncomputable section
14 namespace KomorebiSpace
15 namespace BoundedParity
16 open scoped NNReal ENNReal
17 variable {𝕜 : Type u} [NontriviallyNormedField 𝕜]
18 variable {E : ℕ → Type v}
19 
20 /-- Interleave a dependent even family and a dependent odd family. -/
21 def join (a : ∀ n, E (2*n)) (b : ∀ n, E (2*n+1)) (n : ℕ) : E n :=
22   if h : n % 2 = 0 then
23     (show 2*(n/2) = n by omega) ▸ a (n/2)
24   else
25     (show 2*(n/2)+1 = n by omega) ▸ b (n/2)
26 
27 theorem transport_family (g : ℕ → ℕ) (a : ∀ n, E (g n))
28     {i j : ℕ} (h : i = j) : (congrArg g h) ▸ a i = a j := by
29   cases h
30   rfl
31 
32 @[simp] theorem join_even (a : ∀ n, E (2*n)) (b : ∀ n, E (2*n+1)) (n : ℕ) :
33     join a b (2*n) = a n := by
34   have hd : 2*n/2 = n := by omega
35   simp [join]
36   exact transport_family (fun k => 2*k) a hd
37 
38 @[simp] theorem join_odd (a : ∀ n, E (2*n)) (b : ∀ n, E (2*n+1)) (n : ℕ) :
39     join a b (2*n+1) = b n := by
40   have hd : (2*n+1)/2 = n := by omega
41   simp [join]
42   exact transport_family (fun k => 2*k+1) b hd
43 
44 theorem family_ext (f g : ∀ n, E n)
45     (he : ∀ n, f (2*n) = g (2*n)) (ho : ∀ n, f (2*n+1) = g (2*n+1)) : f = g := by
46   funext n
47   have hn : n = 2*(n/2) ∨ n = 2*(n/2)+1 := by omega
48   rcases hn with h | h
49   · rw [h]; exact he _
50   · rw [h]; exact ho _
51 
52 variable [∀ n, NormedAddCommGroup (E n)] [∀ n, NormedSpace 𝕜 (E n)]
53 abbrev Family := lp E (∞ : ℝ≥0∞)
54 abbrev Even := lp (fun n => E (2*n)) (∞ : ℝ≥0∞)
55 abbrev Odd := lp (fun n => E (2*n+1)) (∞ : ℝ≥0∞)
56 
57 def even (f : Family (E := E)) : Even (E := E) :=
58   ⟨fun n => f (2*n), memℓp_infty ⟨‖f‖, by
59     rintro _ ⟨n, rfl⟩
60     exact lp.norm_apply_le_norm ENNReal.top_ne_zero f (2*n)⟩⟩
61 
62 def odd (f : Family (E := E)) : Odd (E := E) :=
63   ⟨fun n => f (2*n+1), memℓp_infty ⟨‖f‖, by
64     rintro _ ⟨n, rfl⟩
65     exact lp.norm_apply_le_norm ENNReal.top_ne_zero f (2*n+1)⟩⟩
66 
67 @[simp] theorem even_apply (f : Family (E := E)) (n : ℕ) : even f n = f (2*n) := rfl
68 @[simp] theorem odd_apply (f : Family (E := E)) (n : ℕ) : odd f n = f (2*n+1) := rfl
69 
70 theorem even_bound (f : Family (E := E)) : ‖even f‖ ≤ ‖f‖ := by
71   apply lp.norm_le_of_forall_le (norm_nonneg f)
72   intro n
73   exact lp.norm_apply_le_norm ENNReal.top_ne_zero f (2*n)
74 
75 theorem odd_bound (f : Family (E := E)) : ‖odd f‖ ≤ ‖f‖ := by
76   apply lp.norm_le_of_forall_le (norm_nonneg f)
77   intro n
78   exact lp.norm_apply_le_norm ENNReal.top_ne_zero f (2*n+1)
79 
80 theorem join_bound (a : ∀ n, E (2*n)) (b : ∀ n, E (2*n+1)) (K : ℝ)
81     (ha : ∀ n, ‖a n‖ ≤ K) (hb : ∀ n, ‖b n‖ ≤ K) (n : ℕ) :
82     ‖join a b n‖ ≤ K := by
83   have hn : (∃ k, n = 2*k) ∨ (∃ k, n = 2*k+1) := by
84     have h : n = 2*(n/2) ∨ n = 2*(n/2)+1 := by omega
85     exact h.elim (fun h => Or.inl ⟨n/2, h⟩) (fun h => Or.inr ⟨n/2, h⟩)
86   rcases hn with ⟨k, rfl⟩ | ⟨k, rfl⟩
87   · rw [join_even]; exact ha k
88   · rw [join_odd]; exact hb k
89 
90 def merge (z : Even (E := E) × Odd (E := E)) : Family (E := E) :=
91   ⟨join z.1 z.2, memℓp_infty ⟨max ‖z.1‖ ‖z.2‖, by
92     rintro _ ⟨n, rfl⟩
93     exact join_bound _ _ _
94       (fun k => (lp.norm_apply_le_norm ENNReal.top_ne_zero z.1 k).trans (le_max_left _ _))
95       (fun k => (lp.norm_apply_le_norm ENNReal.top_ne_zero z.2 k).trans (le_max_right _ _)) n⟩⟩
96 
97 @[simp] theorem merge_even (z : Even (E := E) × Odd (E := E)) (n : ℕ) :
98     merge z (2*n) = z.1 n := join_even _ _ n
99 @[simp] theorem merge_odd (z : Even (E := E) × Odd (E := E)) (n : ℕ) :
100     merge z (2*n+1) = z.2 n := join_odd _ _ n
101 
102 theorem merge_bound (z : Even (E := E) × Odd (E := E)) : ‖merge z‖ ≤ ‖z‖ := by
103   apply lp.norm_le_of_forall_le (norm_nonneg z)
104   intro n
105   have hn : n = 2*(n/2) ∨ n = 2*(n/2)+1 := by omega
106   rcases hn with h | h
107   · rw [h, merge_even]
108     exact (lp.norm_apply_le_norm ENNReal.top_ne_zero z.1 _).trans (le_max_left _ _)
109   · rw [h, merge_odd]
110     exact (lp.norm_apply_le_norm ENNReal.top_ne_zero z.2 _).trans (le_max_right _ _)
111 
112 def splitLinear : Family (E := E) ≃ₗ[𝕜] (Even (E := E) × Odd (E := E)) where
113   toFun f := (even f, odd f)
114   invFun := merge
115   left_inv f := by
116     apply lp.ext
117     exact family_ext _ _ (fun n => merge_even _ n) (fun n => merge_odd _ n)
118   right_inv z := by
119     apply Prod.ext <;> apply lp.ext <;> funext n
120     · exact merge_even z n
121     · exact merge_odd z n
122   map_add' f g := by apply Prod.ext <;> apply lp.ext <;> rfl
123   map_smul' c f := by apply Prod.ext <;> apply lp.ext <;> rfl
124 
125 theorem split_bound (f : Family (E := E)) : ‖splitLinear (𝕜 := 𝕜) f‖ ≤ ‖f‖ :=
126   max_le (even_bound f) (odd_bound f)
127 
128 def split : Family (E := E) ≃L[𝕜] (Even (E := E) × Odd (E := E)) :=
129   (splitLinear (𝕜 := 𝕜)).toContinuousLinearEquivOfBounds 1 1
130     (fun f => by simpa using split_bound (𝕜 := 𝕜) f)
131     (fun z => by
132       change ‖merge z‖ ≤ 1 * ‖z‖
133       simpa only [one_mul] using merge_bound z)
134 
135 @[simp] theorem split_apply (f : Family (E := E)) : split (𝕜 := 𝕜) f = (even f, odd f) := rfl
136 @[simp] theorem split_symm (z : Even (E := E) × Odd (E := E)) :
137     (split (𝕜 := 𝕜)).symm z = merge z := rfl
138 
139 theorem split_norm (f : Family (E := E)) : ‖split (𝕜 := 𝕜) f‖ = ‖f‖ := by
140   apply le_antisymm (split_bound f)
141   have h := merge_bound (even f, odd f)
142   have hm : merge (even f, odd f) = f := (splitLinear (𝕜 := 𝕜)).symm_apply_apply f
143   rw [hm] at h
144   exact h
145 
146 end BoundedParity
147 end KomorebiSpace
148 end

Back to source controls