Exactification.lean

1 import Mathlib.Topology.Algebra.InfiniteSum.Real
2 import Mathlib.Topology.Semicontinuity.Basic
3 import Mathlib.Analysis.SpecificLimits.Basic
4 import Mathlib.Tactic.Linarith
5 import Mathlib.Tactic.Ring
6 
7 set_option autoImplicit false
8 
9 /-!
10 # Exactification from summable movement and vanishing residual
11 
12 Completeness, lower semicontinuity and nonnegativity are explicit hypotheses.
13 No assertion of uniqueness follows from residual zero alone.
14 -/
15 universe u
16 namespace KomorebiSpace
17 namespace Exactification
18 open Filter
19 open scoped Topology
20 variable {M : Type u} [PseudoMetricSpace M]
21 
22 /-- Lower semicontinuity is sufficient to preserve a vanishing residual at a limit. -/
23 theorem residual_zero_of_limit (ω : M → ℝ) (hω : ∀ x, 0 ≤ ω x)
24     (hlsc : LowerSemicontinuous ω) {f : ℕ → M} {x : M}
25     (hx : Tendsto f atTop (𝓝 x))
26     (hv : Tendsto (fun n => ω (f n)) atTop (𝓝 0)) : ω x = 0 := by
27   apply le_antisymm _ (hω x)
28   apply le_of_forall_pos_le_add
29   intro ε hε
30   have hev : ∀ᶠ n in atTop, ω (f n) ≤ ε :=
31     ((tendsto_order.1 hv).2 ε hε).mono fun _ h => le_of_lt h
32   have hm : ω x ≤ ε := (hlsc.isClosed_preimage ε).mem_of_tendsto hx hev
33   simpa only [zero_add] using hm
34 
35 /-- General exactification, with an explicit a posteriori tail estimate. -/
36 theorem summable_exactification [CompleteSpace M]
37     (ω : M → ℝ) (hω : ∀ x, 0 ≤ ω x) (hlsc : LowerSemicontinuous ω)
38     (f : ℕ → M) (b : ℕ → ℝ) (hb : Summable b)
39     (hstep : ∀ n, dist (f n) (f (n+1)) ≤ b n)
40     (hv : Tendsto (fun n => ω (f n)) atTop (𝓝 0)) :
41     ∃ x, Tendsto f atTop (𝓝 x) ∧ ω x = 0 ∧
42       ∀ n, dist (f n) x ≤ ∑' k, b (n+k) := by
43   have hc : CauchySeq f := cauchySeq_of_dist_le_of_summable b hstep hb
44   obtain ⟨x, hx⟩ := cauchySeq_tendsto_of_complete hc
45   exact ⟨x, hx, residual_zero_of_limit ω hω hlsc hx hv,
46     dist_le_tsum_of_dist_le_of_tendsto b hstep hb hx⟩
47 
48 /-- Prefix product Q₀=1, Qₙ₊₁=qₙQₙ. -/
49 def productRate (q : ℕ → ℝ) : ℕ → ℝ
50   | 0 => 1
51   | n+1 => q n * productRate q n
52 
53 theorem productRate_nonneg (q : ℕ → ℝ) (hq : ∀ n, 0 ≤ q n) :
54     ∀ n, 0 ≤ productRate q n := by
55   intro n
56   induction n with
57   | zero => norm_num [productRate]
58   | succ n ih => exact mul_nonneg (hq n) ih
59 
60 omit [PseudoMetricSpace M] in
61 theorem variable_decay (ω : M → ℝ) (f : ℕ → M) (q : ℕ → ℝ)
62     (hq : ∀ n, 0 ≤ q n)
63     (hdec : ∀ n, ω (f (n+1)) ≤ q n * ω (f n)) :
64     ∀ n, ω (f n) ≤ productRate q n * ω (f 0) := by
65   intro n
66   induction n with
67   | zero => simp [productRate]
68   | succ n ih =>
69     calc
70       ω (f (n+1)) ≤ q n * ω (f n) := hdec n
71       _ ≤ q n * (productRate q n * ω (f 0)) := mul_le_mul_of_nonneg_left ih (hq n)
72       _ = productRate q (n+1) * ω (f 0) := by simp [productRate, mul_assoc]
73 
74 /-- Variable cancellation factors: no fixed geometric rate is required. -/
75 theorem variable_exactification [CompleteSpace M]
76     (ω : M → ℝ) (hω : ∀ x, 0 ≤ ω x) (hlsc : LowerSemicontinuous ω)
77     (f : ℕ → M) (q C : ℕ → ℝ)
78     (hq : ∀ n, 0 ≤ q n) (hC : ∀ n, 0 ≤ C n)
79     (hdec : ∀ n, ω (f (n+1)) ≤ q n * ω (f n))
80     (hstep : ∀ n, dist (f n) (f (n+1)) ≤ C n * ω (f n))
81     (hQ : Tendsto (productRate q) atTop (𝓝 0))
82     (hs : Summable (fun n => C n * productRate q n)) :
83     ∃ x, Tendsto f atTop (𝓝 x) ∧ ω x = 0 ∧
84       ∀ n, dist (f n) x ≤ ∑' k, (C (n+k) * productRate q (n+k)) * ω (f 0) := by
85   have hbound := variable_decay ω f q hq hdec
86   have hv : Tendsto (fun n => ω (f n)) atTop (𝓝 0) := by
87     apply squeeze_zero (fun n => hω (f n)) hbound
88     simpa using hQ.mul_const (ω (f 0))
89   refine summable_exactification ω hω hlsc f
90     (fun n => (C n * productRate q n) * ω (f 0)) (hs.mul_right _) ?_ hv
91   intro n
92   calc
93     dist (f n) (f (n+1)) ≤ C n * ω (f n) := hstep n
94     _ ≤ C n * (productRate q n * ω (f 0)) := mul_le_mul_of_nonneg_left (hbound n) (hC n)
95     _ = (C n * productRate q n) * ω (f 0) := (mul_assoc _ _ _).symm
96 
97 omit [PseudoMetricSpace M] in
98 theorem geometric_decay (ω : M → ℝ) (f : ℕ → M) (q : ℝ) (hq : 0 ≤ q)
99     (hdec : ∀ n, ω (f (n+1)) ≤ q * ω (f n)) :
100     ∀ n, ω (f n) ≤ q^n * ω (f 0) := by
101   intro n
102   induction n with
103   | zero => simp
104   | succ n ih =>
105     calc
106       ω (f (n+1)) ≤ q * ω (f n) := hdec n
107       _ ≤ q * (q^n * ω (f 0)) := mul_le_mul_of_nonneg_left ih hq
108       _ = q^(n+1) * ω (f 0) := by rw [pow_succ]; ring
109 
110 /-- A posteriori error estimate relative to the residual at level n. -/
111 theorem geometric_limit_bound (ω : M → ℝ) (f : ℕ → M) (q C : ℝ)
112     (hq₀ : 0 ≤ q) (hq₁ : q < 1) (hC : 0 ≤ C)
113     (hdec : ∀ n, ω (f (n+1)) ≤ q * ω (f n))
114     (hstep : ∀ n, dist (f n) (f (n+1)) ≤ C * ω (f n))
115     {x : M} (hx : Tendsto f atTop (𝓝 x)) (n : ℕ) :
116     dist (f n) x ≤ (C / (1-q)) * ω (f n) := by
117   let g : ℕ → M := fun k => f (n+k)
118   have hg : Tendsto g atTop (𝓝 x) := by
119     simpa only [g, Function.comp_def, Nat.add_comm] using hx.comp (tendsto_add_atTop_nat n)
120   have hd : ∀ k, ω (g (k+1)) ≤ q * ω (g k) := by
121     intro k; exact hdec (n+k)
122   have hb := geometric_decay ω g q hq₀ hd
123   have hs : Summable (fun k : ℕ => C * (q^k * ω (f n))) :=
124     ((summable_geometric_of_lt_one hq₀ hq₁).mul_right _).mul_left _
125   have hst : ∀ k, dist (g k) (g (k+1)) ≤ C * (q^k * ω (f n)) := by
126     intro k
127     exact (hstep (n+k)).trans (mul_le_mul_of_nonneg_left (hb k) hC)
128   have hh := dist_le_tsum_of_dist_le_of_tendsto₀
129     (fun k : ℕ => C * (q^k * ω (f n))) hst hs hg
130   have hsum : (∑' k : ℕ, C * (q^k * ω (f n))) = (C / (1-q)) * ω (f n) := by
131     rw [tsum_mul_left, tsum_mul_right, tsum_geometric_of_lt_one hq₀ hq₁]
132     simp [div_eq_mul_inv, mul_assoc]
133   simpa only [g, Nat.add_zero, hsum] using hh
134 
135 /-- Geometric exactification plus the residual-based tail bound. -/
136 theorem geometric_exactification [CompleteSpace M]
137     (ω : M → ℝ) (hω : ∀ x, 0 ≤ ω x) (hlsc : LowerSemicontinuous ω)
138     (f : ℕ → M) (q C : ℝ)
139     (hq₀ : 0 ≤ q) (hq₁ : q < 1) (hC : 0 ≤ C)
140     (hdec : ∀ n, ω (f (n+1)) ≤ q * ω (f n))
141     (hstep : ∀ n, dist (f n) (f (n+1)) ≤ C * ω (f n)) :
142     ∃ x, Tendsto f atTop (𝓝 x) ∧ ω x = 0 ∧
143       ∀ n, dist (f n) x ≤ (C / (1-q)) * ω (f n) := by
144   have hb := geometric_decay ω f q hq₀ hdec
145   have hv : Tendsto (fun n => ω (f n)) atTop (𝓝 0) := by
146     apply squeeze_zero (fun n => hω (f n)) hb
147     simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one hq₀ hq₁).mul_const (ω (f 0))
148   have hs : Summable (fun n : ℕ => C * (q^n * ω (f 0))) :=
149     ((summable_geometric_of_lt_one hq₀ hq₁).mul_right _).mul_left _
150   have hst : ∀ n, dist (f n) (f (n+1)) ≤ C * (q^n * ω (f 0)) := by
151     intro n
152     exact (hstep n).trans (mul_le_mul_of_nonneg_left (hb n) hC)
153   obtain ⟨x, hx, hw, _⟩ := summable_exactification ω hω hlsc f _ hs hst hv
154   exact ⟨x, hx, hw, geometric_limit_bound ω f q C hq₀ hq₁ hC hdec hstep hx⟩
155 
156 end Exactification
157 
158 namespace PathIndependence
159 open Filter
160 open scoped Topology
161 variable {M : Type u} [MetricSpace M]
162 
163 theorem limits_equal_of_distance_vanishes {f g : ℕ → M} {x y : M}
164     (hf : Tendsto f atTop (𝓝 x)) (hg : Tendsto g atTop (𝓝 y))
165     (hfg : Tendsto (fun n => dist (f n) (g n)) atTop (𝓝 0)) : x = y := by
166   exact dist_eq_zero.mp (tendsto_nhds_unique (hf.dist hg) hfg)
167 
168 theorem limits_equal_of_budget {f g : ℕ → M} {x y : M} (b : ℕ → ℝ)
169     (hf : Tendsto f atTop (𝓝 x)) (hg : Tendsto g atTop (𝓝 y))
170     (hbudget : ∀ n, dist (f n) (g n) ≤ b n)
171     (hb : Tendsto b atTop (𝓝 0)) : x = y := by
172   apply limits_equal_of_distance_vanishes hf hg
173   exact squeeze_zero (fun _ => dist_nonneg) hbudget hb
174 end PathIndependence
175 end KomorebiSpace

Back to source controls