IndisputableMonolith.Gravity.SevenGaps.StrainDescent
IndisputableMonolith/Gravity/SevenGaps/StrainDescent.lean · 833 lines · 36 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Gravity.SevenGaps.HingeStationarityCore
3
4/-!
5# The strain descent: a convergent least-cost flow on the link
6
7## Why this module exists
8
9The C2 bridge's last premise with physical content is the existence half of
10its stationarity adoption: the substrate attains the sourced least-cost
11carrier on each hinge's link. The descent wall
12(`Foundation.RecognitionUpdateDescentWall`) proves the canonical tick update
13cannot carry that premise: on its eventual image the update is 8-periodic,
14so no functional it descends is non-constant there. The premise needs a new
15object: a dynamics on the carrier's strain space. This module builds it and
16proves it convergent.
17
18## The construction
19
20The sourced action on a link decomposes per channel
21(`sourcedAction_eq_sum`): `Φ_c(t) = Σ_i (cosh t_i - 1) - (c/n) Σ_i t_i`.
22The per-channel cost is `ψ_a(s) = cosh s - 1 - a·s` with `a = c/n`,
23strictly convex with unique stationary point `s* = arsinh a`. The descent is
24the gradient step with an explicit self-tuned step size. Writing `g :=
25sinh s - a` (the residual),
26
27 `E := max (2·(cosh s / 2 + |sinh s|·|g|/6)·cosh |g|) (cosh (|s|+|g|))`,
28 `η := E⁻¹`, `s' := s - η·g`,
29
30the envelope is chosen so that the Lyapunov bound and the contraction bound
31hold at once.
32
33## What is proved (all THEOREM; 0 sorry, 0 admit, no new axiom, no
34`native_decide`)
35
36* Scalar bounds from single integrals: `cosh x - 1 ≤ (x²/2)·cosh x`
37 (`cosh_sub_one_le_sq_half_cosh`) and `|sinh x - x| ≤ (|x|³/6)·cosh x`
38 (`abs_sinh_sub_self_le_sixth`), by FTC plus monotonicity of cosh on `ℝ≥0`
39 (`cosh_le_cosh_of_nonneg_of_le`, an elementary exponential proof).
40* `step_one_dim_sub`: the exact algebraic identity of one step (cosh/sinh
41 addition laws, no Taylor theorem).
42* `descent_one_dim`: the Lyapunov decrease `ψ(s') - ψ(s) ≤ -(η/2)·g²`.
43* `descent_one_dim_lt` / `step_fixed_iff_arsinh`: strict decrease exactly
44 off the stationary point; the step's fixed points are exactly
45 `s* = arsinh a` (via `Real.sinh_injective`).
46* `contraction_one_dim`: `|s' - s*| ≤ (1 - η)·|s - s*|` with `η > 0`, from
47 the mean value theorem for `sinh`.
48* `strainOrbit_abs_le` and `strainOrbit_tendsto`: the iterated step
49 converges geometrically to `arsinh a` with a uniform explicit rate on the
50 initial level set, hence `Tendsto (strainOrbit a s₀) atTop (𝓝 s*)`.
51* Vector forms on the link: `strainStepVec` (componentwise), the sourced
52 action strictly decreases off the minimizer (`sourcedAction_step_lt`),
53 the fixed points are exactly `sourcedMinimizer n c`
54 (`stepVec_fixed_iff_minimizer`), and each channel converges
55 (`strainStepVec_tendsto_minimizer`).
56
57## The honest verdict for (A3)
58
59The flow is the steepest descent of the FORCED cost: the descent direction
60`sinh t_i - c/n` is the derivative of the ledger's own cost in the log
61coordinate, i.e. the recognition phase `ph(e^{t_i})` itself (banked:
62`d/dt J(e^t) = ph(e^t)`). The flow is orientation-free: its only signed
63input is the adopted source `c`. So the stationarity premise is reduced to
64one named dynamical principle: that the substrate's strain state follows
65the steepest descent of its total recognition cost. Whether THAT principle
66is itself derivable from the recognition kernel (rather than adopted) is
67the remaining open question, named in the record.
68-/
69
70namespace IndisputableMonolith
71namespace Gravity
72namespace SevenGaps
73namespace StrainDescent
74
75open Real Set Filter
76open scoped Topology
77
78noncomputable section
79
80/-! ## §1. The one-dimensional objects and the scalar bounds -/
81
82/-- The per-channel sourced cost: `ψ_a(s) = cosh s - 1 - a·s`. -/
83def sourceCost1 (a : ℝ) : ℝ → ℝ := fun s => Real.cosh s - 1 - a * s
84
85/-- The residual (the gradient of the per-channel cost): `sinh s - a`. -/
86def strainResidual (a : ℝ) : ℝ → ℝ := fun s => Real.sinh s - a
87
88/-- The envelope: the larger of the two bounds the proof needs,
89`2·(cosh s / 2 + |sinh s|·|g|/6)·cosh |g|` for the Lyapunov assembly and
90`cosh (|s|+|g|)` for the contraction. -/
91def strainEnvelope (a s : ℝ) : ℝ :=
92 max (2 * (Real.cosh s / 2 + |Real.sinh s| * |strainResidual a s| / 6)
93 * Real.cosh (|strainResidual a s|))
94 (Real.cosh (|s| + |strainResidual a s|))
95
96/-- The self-tuned step size: the reciprocal of the envelope. -/
97def strainStepSize (a s : ℝ) : ℝ := (strainEnvelope a s)⁻¹
98
99/-- One descent step: `s' = s - η·g`. -/
100def strainStep1 (a s : ℝ) : ℝ := s - strainStepSize a s * strainResidual a s
101
102/-- The envelope is at least `1`. -/
103theorem strainEnvelope_ge_one (a s : ℝ) : 1 ≤ strainEnvelope a s := by
104 unfold strainEnvelope
105 exact le_max_of_le_right (Real.one_le_cosh _)
106
107/-- The envelope is strictly positive. -/
108theorem strainEnvelope_pos (a s : ℝ) : 0 < strainEnvelope a s :=
109 lt_of_lt_of_le one_pos (strainEnvelope_ge_one a s)
110
111/-- The step size is strictly positive. -/
112theorem strainStepSize_pos (a s : ℝ) : 0 < strainStepSize a s := by
113 unfold strainStepSize
114 exact inv_pos.mpr (strainEnvelope_pos a s)
115
116/-- The step size is at most `1`. -/
117theorem strainStepSize_le_one (a s : ℝ) : strainStepSize a s ≤ 1 := by
118 unfold strainStepSize
119 rw [inv_le_one_iff₀]
120 exact Or.inr (strainEnvelope_ge_one a s)
121
122/-- `cosh` is monotone on `ℝ≥0`: for `0 ≤ t ≤ x`, `cosh t ≤ cosh x`.
123The difference factors as `(e^x - e^t)(1 - e^{-(x+t)})/2 ≥ 0`. -/
124theorem cosh_le_cosh_of_nonneg_of_le {t x : ℝ} (ht : 0 ≤ t) (htx : t ≤ x) :
125 Real.cosh t ≤ Real.cosh x := by
126 have hx : 0 ≤ x := le_trans ht htx
127 have key : Real.cosh x - Real.cosh t
128 = (Real.exp x - Real.exp t) * (1 - Real.exp (-x) * Real.exp (-t)) / 2 := by
129 rw [Real.cosh_eq, Real.cosh_eq, Real.exp_neg, Real.exp_neg]
130 field_simp [Real.exp_ne_zero]
131 ring
132 have h1 : (0:ℝ) ≤ Real.exp x - Real.exp t := sub_nonneg.mpr (Real.exp_le_exp.mpr htx)
133 have h2 : Real.exp (-x) * Real.exp (-t) ≤ 1 := by
134 rw [← Real.exp_add]
135 exact Real.exp_le_one_iff.mpr (by linarith)
136 have h3 : (0:ℝ) ≤ 1 - Real.exp (-x) * Real.exp (-t) := sub_nonneg.mpr h2
137 have h4 : (0:ℝ) ≤ (Real.exp x - Real.exp t) * (1 - Real.exp (-x) * Real.exp (-t)) / 2 :=
138 div_nonneg (mul_nonneg h1 h3) (by norm_num)
139 linarith [key, h4]
140
141/-- The FTC evaluations for cosh and sinh, stated for all `x` (oriented). -/
142theorem integral_sinh (x : ℝ) :
143 ∫ t in (0:ℝ)..x, Real.sinh t = Real.cosh x - 1 := by
144 have h := intervalIntegral.integral_eq_sub_of_hasDerivAt
145 (f := Real.cosh) (f' := Real.sinh) (a := 0) (b := x)
146 (fun t _ => Real.hasDerivAt_cosh t)
147 (Real.continuous_sinh.intervalIntegrable _ _)
148 simpa using h
149
150theorem integral_cosh (x : ℝ) :
151 ∫ t in (0:ℝ)..x, Real.cosh t = Real.sinh x := by
152 have h := intervalIntegral.integral_eq_sub_of_hasDerivAt
153 (f := Real.sinh) (f' := Real.cosh) (a := 0) (b := x)
154 (fun t _ => Real.hasDerivAt_sinh t)
155 (Real.continuous_cosh.intervalIntegrable _ _)
156 simpa using h
157
158/-- For `t ≥ 0`: `sinh t ≤ t · cosh t`. -/
159theorem sinh_le_mul_cosh {t : ℝ} (ht : 0 ≤ t) :
160 Real.sinh t ≤ t * Real.cosh t := by
161 rw [← integral_cosh t]
162 calc ∫ u in (0:ℝ)..t, Real.cosh u
163 ≤ ∫ u in (0:ℝ)..t, Real.cosh t :=
164 intervalIntegral.integral_mono_on ht
165 (Real.continuous_cosh.intervalIntegrable _ _)
166 (continuous_const.intervalIntegrable _ _)
167 (fun u hu => cosh_le_cosh_of_nonneg_of_le hu.1 hu.2)
168 _ = t * Real.cosh t := by
169 rw [intervalIntegral.integral_const]
170 simp [mul_comm]
171
172/-- The antiderivative of `t ↦ t` on `[0, x]`. -/
173theorem integral_id_half_sq (x : ℝ) :
174 ∫ t in (0:ℝ)..x, (t : ℝ) = x ^ 2 / 2 := by
175 have h := intervalIntegral.integral_eq_sub_of_hasDerivAt
176 (f := fun t : ℝ => t ^ 2 / 2) (f' := fun t : ℝ => t)
177 (a := 0) (b := x)
178 (fun t _ => by
179 have hder := ((hasDerivAt_id t).pow 2).div_const 2
180 convert hder using 1 <;> simp only [Pi.pow_apply, id_eq] <;> ring)
181 (continuous_id.intervalIntegrable _ _)
182 simpa using h
183
184/-- The antiderivative of `t ↦ t²/2` on `[0, x]`. -/
185theorem integral_sq_half_third (x : ℝ) :
186 ∫ t in (0:ℝ)..x, (t ^ 2 / 2 : ℝ) = x ^ 3 / 6 := by
187 have h := intervalIntegral.integral_eq_sub_of_hasDerivAt
188 (f := fun t : ℝ => t ^ 3 / 6) (f' := fun t : ℝ => t ^ 2 / 2)
189 (a := 0) (b := x)
190 (fun t _ => by
191 have hder := ((hasDerivAt_id t).pow 3).div_const 6
192 convert hder using 1 <;> simp only [Pi.pow_apply, id_eq] <;> ring)
193 (((continuous_id.pow 2).div_const 2).intervalIntegrable _ _)
194 simpa using h
195
196/-- **First scalar bound**: `cosh x - 1 ≤ (x²/2)·cosh x`, all `x`. -/
197theorem cosh_sub_one_le_sq_half_cosh (x : ℝ) :
198 Real.cosh x - 1 ≤ (x ^ 2 / 2) * Real.cosh x := by
199 rcases le_or_gt 0 x with hx | hx
200 · rw [← integral_sinh x]
201 calc ∫ t in (0:ℝ)..x, Real.sinh t
202 ≤ ∫ t in (0:ℝ)..x, (fun t => t * Real.cosh x) t := by
203 apply intervalIntegral.integral_mono_on hx
204 (Real.continuous_sinh.intervalIntegrable _ _)
205 ((continuous_id.mul continuous_const).intervalIntegrable _ _)
206 · intro t ht'
207 exact le_trans (sinh_le_mul_cosh ht'.1)
208 (mul_le_mul_of_nonneg_left
209 (cosh_le_cosh_of_nonneg_of_le ht'.1 ht'.2) ht'.1)
210 _ = (x ^ 2 / 2) * Real.cosh x := by
211 rw [intervalIntegral.integral_mul_const, integral_id_half_sq]
212 · have h0 : 0 ≤ -x := le_of_lt (neg_pos.mpr hx)
213 have hmain : Real.cosh (-x) - 1 ≤ ((-x) ^ 2 / 2) * Real.cosh (-x) := by
214 rw [← integral_sinh (-x)]
215 calc ∫ t in (0:ℝ)..(-x), Real.sinh t
216 ≤ ∫ t in (0:ℝ)..(-x), (fun t => t * Real.cosh (-x)) t := by
217 apply intervalIntegral.integral_mono_on h0
218 (Real.continuous_sinh.intervalIntegrable _ _)
219 ((continuous_id.mul continuous_const).intervalIntegrable _ _)
220 · intro t ht'
221 exact le_trans (sinh_le_mul_cosh ht'.1)
222 (mul_le_mul_of_nonneg_left
223 (cosh_le_cosh_of_nonneg_of_le ht'.1 ht'.2) ht'.1)
224 _ = ((-x) ^ 2 / 2) * Real.cosh (-x) := by
225 rw [intervalIntegral.integral_mul_const, integral_id_half_sq]
226 rwa [Real.cosh_neg, neg_sq] at hmain
227
228/-- **Second scalar bound**: `|sinh x - x| ≤ (|x|³/6)·cosh x`, all `x`. -/
229theorem abs_sinh_sub_self_le_sixth (x : ℝ) :
230 |Real.sinh x - x| ≤ (|x| ^ 3 / 6) * Real.cosh x := by
231 rcases le_or_gt 0 x with hx | hx
232 · have hnonneg : (0:ℝ) ≤ Real.sinh x - x := by
233 rw [show Real.sinh x - x = ∫ t in (0:ℝ)..x, (Real.cosh t - 1) from
234 by rw [intervalIntegral.integral_sub
235 (Real.continuous_cosh.intervalIntegrable _ _)
236 (continuous_const.intervalIntegrable _ _),
237 integral_cosh, intervalIntegral.integral_const]; simp]
238 apply intervalIntegral.integral_nonneg hx
239 intro t _
240 have h1 : (1:ℝ) ≤ Real.cosh t := Real.one_le_cosh t
241 simp [h1]
242 rw [abs_of_nonneg hnonneg, abs_of_nonneg hx]
243 calc Real.sinh x - x
244 = ∫ t in (0:ℝ)..x, (Real.cosh t - 1) := by
245 rw [intervalIntegral.integral_sub
246 (Real.continuous_cosh.intervalIntegrable _ _)
247 (continuous_const.intervalIntegrable _ _),
248 integral_cosh, intervalIntegral.integral_const]
249 simp
250 _ ≤ ∫ t in (0:ℝ)..x, (fun t => (t ^ 2 / 2) * Real.cosh x) t := by
251 apply intervalIntegral.integral_mono_on hx
252 ((Real.continuous_cosh.sub continuous_const).intervalIntegrable _ _)
253 (((continuous_id.pow 2).div_const 2).mul continuous_const
254 |>.intervalIntegrable _ _)
255 · intro t ht'
256 have h1 : Real.cosh t - 1 ≤ (t ^ 2 / 2) * Real.cosh t :=
257 cosh_sub_one_le_sq_half_cosh t
258 have h2 : Real.cosh t ≤ Real.cosh x :=
259 cosh_le_cosh_of_nonneg_of_le ht'.1 ht'.2
260 exact le_trans h1 (mul_le_mul_of_nonneg_left h2 (by positivity))
261 _ = (x ^ 3 / 6) * Real.cosh x := by
262 rw [intervalIntegral.integral_mul_const, integral_sq_half_third]
263 · have h0 : 0 ≤ -x := le_of_lt (neg_pos.mpr hx)
264 have hodd : Real.sinh x - x = -(Real.sinh (-x) - (-x)) := by
265 rw [Real.sinh_neg]; ring
266 have hmain : |Real.sinh (-x) - (-x)| ≤ ((-x) ^ 3 / 6) * Real.cosh (-x) := by
267 have hnonneg : (0:ℝ) ≤ Real.sinh (-x) - (-x) := by
268 rw [show Real.sinh (-x) - (-x)
269 = ∫ t in (0:ℝ)..(-x), (Real.cosh t - 1) from
270 by rw [intervalIntegral.integral_sub
271 (Real.continuous_cosh.intervalIntegrable _ _)
272 (continuous_const.intervalIntegrable _ _),
273 integral_cosh, intervalIntegral.integral_const]; simp]
274 apply intervalIntegral.integral_nonneg h0
275 intro t _
276 have h1 : (1:ℝ) ≤ Real.cosh t := Real.one_le_cosh t
277 simp [h1]
278 rw [abs_of_nonneg hnonneg]
279 calc Real.sinh (-x) - (-x)
280 = ∫ t in (0:ℝ)..(-x), (Real.cosh t - 1) := by
281 rw [intervalIntegral.integral_sub
282 (Real.continuous_cosh.intervalIntegrable _ _)
283 (continuous_const.intervalIntegrable _ _),
284 integral_cosh, intervalIntegral.integral_const]
285 simp
286 _ ≤ ∫ t in (0:ℝ)..(-x), (fun t => (t ^ 2 / 2) * Real.cosh (-x)) t := by
287 apply intervalIntegral.integral_mono_on h0
288 ((Real.continuous_cosh.sub continuous_const).intervalIntegrable _ _)
289 (((continuous_id.pow 2).div_const 2).mul continuous_const
290 |>.intervalIntegrable _ _)
291 · intro t ht'
292 have h1 : Real.cosh t - 1 ≤ (t ^ 2 / 2) * Real.cosh t :=
293 cosh_sub_one_le_sq_half_cosh t
294 have h2 : Real.cosh t ≤ Real.cosh (-x) :=
295 cosh_le_cosh_of_nonneg_of_le ht'.1 ht'.2
296 exact le_trans h1 (mul_le_mul_of_nonneg_left h2 (by positivity))
297 _ = ((-x) ^ 3 / 6) * Real.cosh (-x) := by
298 rw [intervalIntegral.integral_mul_const, integral_sq_half_third]
299 calc |Real.sinh x - x|
300 = |-(Real.sinh (-x) - (-x))| := by rw [hodd]
301 _ = |Real.sinh (-x) - (-x)| := abs_neg _
302 _ ≤ ((-x) ^ 3 / 6) * Real.cosh (-x) := hmain
303 _ = (|x| ^ 3 / 6) * Real.cosh x := by
304 rw [Real.cosh_neg, abs_of_neg hx, neg_pow]
305
306/-! ## §2. The exact one-step identity and the Lyapunov decrease -/
307
308/-- **The exact identity for one step** (no Taylor theorem). -/
309theorem step_one_dim_sub (a s : ℝ) :
310 sourceCost1 a (strainStep1 a s) - sourceCost1 a s
311 = - strainStepSize a s * strainResidual a s ^ 2
312 + Real.cosh s * (Real.cosh (strainStepSize a s * strainResidual a s) - 1)
313 - Real.sinh s * (Real.sinh (strainStepSize a s * strainResidual a s)
314 - strainStepSize a s * strainResidual a s) := by
315 unfold sourceCost1 strainStep1 strainResidual
316 rw [Real.cosh_sub]
317 ring
318
319/-- The cosh-on-the-step is bounded by the cosh of the residual. -/
320theorem cosh_step_le_cosh_abs_residual (a s : ℝ) :
321 Real.cosh (strainStepSize a s * strainResidual a s)
322 ≤ Real.cosh (|strainResidual a s|) := by
323 have hη : 0 < strainStepSize a s := strainStepSize_pos a s
324 have hηle : strainStepSize a s ≤ 1 := strainStepSize_le_one a s
325 have habs : |strainStepSize a s * strainResidual a s|
326 ≤ |strainResidual a s| := by
327 rw [abs_mul, abs_of_nonneg hη.le]
328 calc strainStepSize a s * |strainResidual a s|
329 ≤ 1 * |strainResidual a s| :=
330 mul_le_mul_of_nonneg_right hηle (abs_nonneg _)
331 _ = |strainResidual a s| := one_mul _
332 rw [← Real.cosh_abs (strainStepSize a s * strainResidual a s)]
333 exact cosh_le_cosh_of_nonneg_of_le (abs_nonneg _) habs
334
335/-- **The correction is at most half the tangent descent.** -/
336theorem correction_le_half (a s : ℝ) :
337 Real.cosh s * (Real.cosh (strainStepSize a s * strainResidual a s) - 1)
338 - Real.sinh s * (Real.sinh (strainStepSize a s * strainResidual a s)
339 - strainStepSize a s * strainResidual a s)
340 ≤ (strainStepSize a s / 2) * strainResidual a s ^ 2 := by
341 set η := strainStepSize a s with hηdef
342 set g := strainResidual a s with hgdef
343 have hηpos : 0 < η := strainStepSize_pos a s
344 have hηle : η ≤ 1 := strainStepSize_le_one a s
345 set B := Real.cosh s / 2 + |Real.sinh s| * |g| / 6 with hBdef
346 have hBnn : (0:ℝ) ≤ B := by
347 rw [hBdef]
348 have h1 := Real.one_le_cosh s
349 have h2 : (0:ℝ) ≤ |Real.sinh s| * |g| / 6 := by positivity
350 linarith
351 have hT1 : Real.cosh s * (Real.cosh (η * g) - 1)
352 ≤ Real.cosh s * (((η * g) ^ 2 / 2) * Real.cosh (η * g)) :=
353 mul_le_mul_of_nonneg_left (cosh_sub_one_le_sq_half_cosh (η * g))
354 (zero_le_one.trans (Real.one_le_cosh s))
355 have hT2 : -(Real.sinh s * (Real.sinh (η * g) - η * g))
356 ≤ |Real.sinh s| * ((|η * g| ^ 3 / 6) * Real.cosh (η * g)) :=
357 calc -(Real.sinh s * (Real.sinh (η * g) - η * g))
358 ≤ |Real.sinh s * (Real.sinh (η * g) - η * g)| := neg_le_abs _
359 _ = |Real.sinh s| * |Real.sinh (η * g) - η * g| := abs_mul _ _
360 _ ≤ |Real.sinh s| * ((|η * g| ^ 3 / 6) * Real.cosh (η * g)) :=
361 mul_le_mul_of_nonneg_left (abs_sinh_sub_self_le_sixth (η * g))
362 (abs_nonneg _)
363 have hT12 : Real.cosh s * (((η * g) ^ 2 / 2) * Real.cosh (η * g))
364 + |Real.sinh s| * ((|η * g| ^ 3 / 6) * Real.cosh (η * g))
365 ≤ Real.cosh (η * g) * (η ^ 2 * g ^ 2) * B := by
366 have hη2 : |η| = η := abs_of_nonneg hηpos.le
367 have hexp : (η * g) ^ 2 = η ^ 2 * g ^ 2 := by ring
368 have habs3 : |η * g| ^ 3 ≤ η ^ 2 * (g ^ 2 * |g|) := by
369 have hη3 : η ^ 3 ≤ η ^ 2 := by
370 have hη2nn : (0:ℝ) ≤ η ^ 2 := by positivity
371 calc η ^ 3 = η ^ 2 * η := by ring
372 _ ≤ η ^ 2 * 1 := mul_le_mul_of_nonneg_left hηle hη2nn
373 _ = η ^ 2 := mul_one _
374 calc |η * g| ^ 3 = (η * |g|) ^ 3 := by rw [abs_mul, hη2]
375 _ = η ^ 3 * |g| ^ 3 := by ring
376 _ ≤ η ^ 2 * |g| ^ 3 := mul_le_mul_of_nonneg_right hη3 (by positivity)
377 _ = η ^ 2 * (g ^ 2 * |g|) := by rw [← sq_abs g]; ring
378 have hT1eq : Real.cosh s * (((η * g) ^ 2 / 2) * Real.cosh (η * g))
379 = Real.cosh (η * g) * (η ^ 2 * g ^ 2) * (Real.cosh s / 2) := by
380 rw [hexp]; ring
381 have hT2le : |Real.sinh s| * ((|η * g| ^ 3 / 6) * Real.cosh (η * g))
382 ≤ Real.cosh (η * g) * (η ^ 2 * g ^ 2) * (|g| * |Real.sinh s| / 6) := by
383 have hnn : (0:ℝ) ≤ |Real.sinh s| * Real.cosh (η * g) := by positivity
384 calc |Real.sinh s| * ((|η * g| ^ 3 / 6) * Real.cosh (η * g))
385 = |Real.sinh s| * Real.cosh (η * g) * (|η * g| ^ 3 / 6) := by ring
386 _ ≤ |Real.sinh s| * Real.cosh (η * g) * ((η ^ 2 * (g ^ 2 * |g|)) / 6) :=
387 mul_le_mul_of_nonneg_left (by linarith [habs3] :
388 |η * g| ^ 3 / 6 ≤ (η ^ 2 * (g ^ 2 * |g|)) / 6) hnn
389 _ = Real.cosh (η * g) * (η ^ 2 * g ^ 2) * (|g| * |Real.sinh s| / 6) := by ring
390 calc Real.cosh s * (((η * g) ^ 2 / 2) * Real.cosh (η * g))
391 + |Real.sinh s| * ((|η * g| ^ 3 / 6) * Real.cosh (η * g))
392 = Real.cosh (η * g) * (η ^ 2 * g ^ 2) * (Real.cosh s / 2)
393 + |Real.sinh s| * ((|η * g| ^ 3 / 6) * Real.cosh (η * g)) := by
394 rw [hT1eq]
395 _ ≤ Real.cosh (η * g) * (η ^ 2 * g ^ 2) * (Real.cosh s / 2)
396 + Real.cosh (η * g) * (η ^ 2 * g ^ 2) * (|g| * |Real.sinh s| / 6) :=
397 add_le_add le_rfl hT2le
398 _ = Real.cosh (η * g) * (η ^ 2 * g ^ 2) * B := by rw [hBdef]; ring
399 have henvm : Real.cosh (η * g) ≤ Real.cosh |g| :=
400 cosh_step_le_cosh_abs_residual a s
401 have hkey : Real.cosh |g| * (η ^ 2 * g ^ 2) * B ≤ (η / 2) * g ^ 2 := by
402 have hE : 2 * B * Real.cosh |g| ≤ strainEnvelope a s := le_max_left _ _
403 have hηE : η * (2 * B * Real.cosh |g|) ≤ 1 := by
404 rw [hηdef, strainStepSize]
405 rw [inv_mul_le_iff₀ (strainEnvelope_pos a s)]
406 calc 2 * B * Real.cosh |g| ≤ strainEnvelope a s := hE
407 _ = strainEnvelope a s * 1 := (mul_one _).symm
408 have hhalf : η * B * Real.cosh |g| ≤ 1 / 2 := by
409 have h2 : η * (2 * B * Real.cosh |g|) = 2 * (η * B * Real.cosh |g|) := by ring
410 rw [h2] at hηE
411 linarith
412 by_cases hg0 : g = 0
413 · rw [hg0]
414 simp
415 · have hg2 : (0:ℝ) < g ^ 2 := sq_pos_of_ne_zero hg0
416 have hdiv : Real.cosh |g| * (η ^ 2 * g ^ 2) * B
417 = (η * g ^ 2) * (η * B * Real.cosh |g|) := by ring
418 rw [hdiv]
419 calc (η * g ^ 2) * (η * B * Real.cosh |g|)
420 ≤ (η * g ^ 2) * (1 / 2) :=
421 mul_le_mul_of_nonneg_left hhalf (by positivity)
422 _ = (η / 2) * g ^ 2 := by ring
423 calc Real.cosh s * (Real.cosh (η * g) - 1)
424 - Real.sinh s * (Real.sinh (η * g) - η * g)
425 ≤ Real.cosh s * (((η * g) ^ 2 / 2) * Real.cosh (η * g))
426 + |Real.sinh s| * ((|η * g| ^ 3 / 6) * Real.cosh (η * g)) :=
427 add_le_add hT1 hT2
428 _ ≤ Real.cosh (η * g) * (η ^ 2 * g ^ 2) * B := hT12
429 _ ≤ Real.cosh |g| * (η ^ 2 * g ^ 2) * B :=
430 mul_le_mul_of_nonneg_right
431 (mul_le_mul_of_nonneg_right henvm (by positivity)) hBnn
432 _ ≤ (η / 2) * g ^ 2 := hkey
433
434/-- **THEOREM (the Lyapunov decrease).** -/
435theorem descent_one_dim (a s : ℝ) :
436 sourceCost1 a (strainStep1 a s) - sourceCost1 a s
437 ≤ -(strainStepSize a s / 2) * strainResidual a s ^ 2 := by
438 rw [step_one_dim_sub]
439 have h := correction_le_half a s
440 linarith [h]
441
442/-- **THEOREM (strict decrease off the stationary point).** -/
443theorem descent_one_dim_lt (a s : ℝ) (hs : strainResidual a s ≠ 0) :
444 sourceCost1 a (strainStep1 a s) < sourceCost1 a s := by
445 have h := descent_one_dim a s
446 have hg2 : (0:ℝ) < strainResidual a s ^ 2 := sq_pos_of_ne_zero hs
447 have hη : (0:ℝ) < strainStepSize a s / 2 := by
448 have := strainStepSize_pos a s
449 positivity
450 have hneg : -(strainStepSize a s / 2) * strainResidual a s ^ 2 < 0 := by
451 have hpos : (0:ℝ) < (strainStepSize a s / 2) * strainResidual a s ^ 2 := by
452 positivity
453 linarith
454 linarith
455
456/-- **THEOREM (fixed points).** The step's fixed points are exactly the
457sourced stationary point. -/
458theorem step_fixed_iff_arsinh (a s : ℝ) :
459 strainStep1 a s = s ↔ s = Real.arsinh a := by
460 constructor
461 · intro h
462 unfold strainStep1 at h
463 have hg : strainStepSize a s * strainResidual a s = 0 := by linarith
464 have hg2 : strainResidual a s = 0 :=
465 (mul_eq_zero.mp hg).resolve_left (strainStepSize_pos a s).ne'
466 have hsinh : Real.sinh s = a := by
467 unfold strainResidual at hg2
468 linarith
469 rw [← Real.sinh_arsinh a] at hsinh
470 exact Real.sinh_injective hsinh
471 · intro h
472 rw [h]
473 unfold strainStep1 strainResidual
474 rw [Real.sinh_arsinh]
475 simp
476
477/-! ## §3. The contraction -/
478
479/-- |sinh x| = sinh |x|. -/
480theorem abs_sinh_eq_sinh_abs (x : ℝ) : |Real.sinh x| = Real.sinh |x| := by
481 rcases le_or_gt 0 x with h | h
482 · have h2 : 0 ≤ Real.sinh x := by
483 have := Real.sinh_strictMono.monotone (show (0:ℝ) ≤ x from h)
484 simpa using this
485 rw [abs_of_nonneg h, abs_of_nonneg h2]
486 · have h2 : Real.sinh x < 0 := by
487 have := Real.sinh_strictMono (show x < 0 from h)
488 simpa using this
489 rw [abs_of_neg h, abs_of_neg h2, Real.sinh_neg]
490
491/-- **THEOREM (the contraction).** One step contracts the distance to the
492sourced stationary point by `1 - η`. -/
493theorem contraction_one_dim (a s : ℝ) :
494 |strainStep1 a s - Real.arsinh a|
495 ≤ (1 - strainStepSize a s) * |s - Real.arsinh a| := by
496 set sstar := Real.arsinh a with hsstar
497 set η := strainStepSize a s with hηdef
498 set g := strainResidual a s with hgdef
499 have ha : a = Real.sinh sstar := by rw [hsstar, Real.sinh_arsinh]
500 have hηpos : 0 < η := strainStepSize_pos a s
501 by_cases hs : s = sstar
502 · rw [hs]
503 have hg0 : strainResidual a sstar = 0 := by
504 unfold strainResidual
505 rw [Real.sinh_arsinh]
506 simp
507 have hstep0 : strainStep1 a sstar = sstar := by
508 unfold strainStep1
509 rw [hg0]
510 simp
511 rw [hstep0]
512 simp
513 · -- MVT for sinh between s and s*.
514 have hsub : Real.sinh s - Real.sinh sstar = g := by
515 rw [hgdef]
516 unfold strainResidual
517 rw [ha]
518 have hmvt : ∃ ξ : ℝ, ξ ∈ Set.Ioo (min s sstar) (max s sstar) ∧
519 Real.cosh ξ = (Real.sinh s - Real.sinh sstar) / (s - sstar) := by
520 rcases lt_or_gt_of_ne hs with hlt | hgt
521 · have h := exists_deriv_eq_slope Real.sinh (show s < sstar from hlt)
522 Real.continuous_sinh.continuousOn
523 (Real.differentiable_sinh.differentiableOn)
524 obtain ⟨ξ, hξ, hξeq⟩ := h
525 refine ⟨ξ, ?_, ?_⟩
526 · rw [min_eq_left hlt.le, max_eq_right hlt.le]
527 exact hξ
528 · rw [Real.deriv_sinh] at hξeq
529 rw [hξeq, div_eq_div_iff (sub_ne_zero.mpr hlt.ne') (sub_ne_zero.mpr hlt.ne)]
530 ring
531 · have h := exists_deriv_eq_slope Real.sinh (show sstar < s from hgt)
532 Real.continuous_sinh.continuousOn
533 (Real.differentiable_sinh.differentiableOn)
534 obtain ⟨ξ, hξ, hξeq⟩ := h
535 refine ⟨ξ, ?_, ?_⟩
536 · rw [min_eq_right hgt.le, max_eq_left hgt.le]
537 exact hξ
538 · rw [Real.deriv_sinh] at hξeq
539 exact hξeq
540 obtain ⟨ξ, hξmem, hξeq⟩ := hmvt
541 have hgc : g = Real.cosh ξ * (s - sstar) := by
542 rw [← hsub, hξeq]
543 field_simp [sub_ne_zero.mpr hs]
544 have hg_abs : |g| = Real.cosh ξ * |s - sstar| := by
545 rw [hgc, abs_mul, abs_of_pos
546 (lt_of_lt_of_le one_pos (Real.one_le_cosh ξ))]
547 have hsg : |s - sstar| ≤ |g| := by
548 rw [hg_abs]
549 calc |s - sstar| = 1 * |s - sstar| := (one_mul _).symm
550 _ ≤ Real.cosh ξ * |s - sstar| :=
551 mul_le_mul_of_nonneg_right (Real.one_le_cosh ξ) (abs_nonneg _)
552 have hξle : |ξ| ≤ |s| + |g| := by
553 have hM : |ξ| ≤ max |s| |sstar| := by
554 rw [abs_le]
555 constructor
556 · have hneg : -(max |s| |sstar|) = min (-|s|) (-|sstar|) := by
557 rcases le_total |s| |sstar| with h | h
558 · rw [max_eq_right h, min_eq_right (neg_le_neg h)]
559 · rw [max_eq_left h, min_eq_left (neg_le_neg h)]
560 calc -(max |s| |sstar|) = min (-|s|) (-|sstar|) := hneg
561 _ ≤ min s sstar := min_le_min (neg_abs_le s) (neg_abs_le sstar)
562 _ ≤ ξ := hξmem.1.le
563 · calc ξ ≤ max s sstar := hξmem.2.le
564 _ ≤ max |s| |sstar| := max_le_max (le_abs_self s) (le_abs_self sstar)
565 have hS : |sstar| ≤ |s| + |g| := by
566 calc |sstar| = |sstar - s + s| := by ring_nf
567 _ ≤ |sstar - s| + |s| := abs_add_le _ _
568 _ = |s - sstar| + |s| := by rw [abs_sub_comm]
569 _ ≤ |g| + |s| := add_le_add_left hsg |s|
570 _ = |s| + |g| := add_comm _ _
571 calc |ξ| ≤ max |s| |sstar| := hM
572 _ ≤ |s| + |g| := max_le (le_add_of_nonneg_right (abs_nonneg _)) hS
573 have hstep : strainStep1 a s - sstar = (s - sstar) * (1 - η * Real.cosh ξ) := by
574 unfold strainStep1
575 rw [← hηdef, ← hgdef, hgc]
576 ring
577 rw [hstep]
578 have hηc : η * Real.cosh (|s| + |g|) ≤ 1 := by
579 rw [hηdef, strainStepSize]
580 rw [inv_mul_le_iff₀ (strainEnvelope_pos a s)]
581 calc Real.cosh (|s| + |g|) ≤ strainEnvelope a s := le_max_right _ _
582 _ = strainEnvelope a s * 1 := (mul_one _).symm
583 have hcξ : Real.cosh ξ ≤ Real.cosh (|s| + |g|) := by
584 rw [← Real.cosh_abs ξ]
585 exact cosh_le_cosh_of_nonneg_of_le (abs_nonneg _) hξle
586 have hfactor : |1 - η * Real.cosh ξ| ≤ 1 - η := by
587 have h1 : (1:ℝ) ≤ Real.cosh ξ := Real.one_le_cosh ξ
588 have hlo : η ≤ η * Real.cosh ξ := by
589 calc η = η * 1 := (mul_one _).symm
590 _ ≤ η * Real.cosh ξ := mul_le_mul_of_nonneg_left h1 hηpos.le
591 have hhi : η * Real.cosh ξ ≤ 1 := le_trans
592 (mul_le_mul_of_nonneg_left hcξ hηpos.le) hηc
593 rw [abs_of_nonneg (by linarith : (0:ℝ) ≤ 1 - η * Real.cosh ξ)]
594 linarith
595 calc |(s - sstar) * (1 - η * Real.cosh ξ)|
596 = |s - sstar| * |1 - η * Real.cosh ξ| := abs_mul _ _
597 _ ≤ |s - sstar| * (1 - η) :=
598 mul_le_mul_of_nonneg_left hfactor (abs_nonneg _)
599 _ = (1 - η) * |s - sstar| := mul_comm _ _
600
601/-! ## §4. The orbit and convergence -/
602
603/-- The strain orbit: iterate the step. -/
604noncomputable def strainOrbit (a : ℝ) (s₀ : ℝ) : ℕ → ℝ
605 | 0 => s₀
606 | k + 1 => strainStep1 a (strainOrbit a s₀ k)
607
608/-- **THEOREM (geometric convergence).** -/
609theorem strainOrbit_abs_le (a : ℝ) (s₀ : ℝ) :
610 ∃ q : ℝ, 0 ≤ q ∧ q < 1 ∧ ∀ k : ℕ,
611 |strainOrbit a s₀ k - Real.arsinh a| ≤ q ^ k * |s₀ - Real.arsinh a| := by
612 set sstar := Real.arsinh a with hsstar
613 set M := |sstar| + |s₀ - sstar| with hMdef
614 set G := Real.sinh M + |a| with hGdef
615 set E2 := 2 * (Real.cosh M + Real.sinh M * G / 6) * Real.cosh G
616 + Real.cosh (M + G) with hE2def
617 set q := 1 - E2⁻¹ with hqdef
618 have hMnn : 0 ≤ M := by rw [hMdef]; positivity
619 have hsinhM : 0 ≤ Real.sinh M := by
620 simpa using Real.sinh_strictMono.monotone hMnn
621 have hGnn : 0 ≤ G := by rw [hGdef]; linarith [hsinhM, abs_nonneg a]
622 have hprod_nn : (0:ℝ) ≤ 2 * (Real.cosh M + Real.sinh M * G / 6) * Real.cosh G := by
623 have h1 : (0:ℝ) ≤ Real.sinh M * G := mul_nonneg hsinhM hGnn
624 have h2 : (0:ℝ) ≤ Real.cosh M + Real.sinh M * G / 6 := by
625 linarith [Real.one_le_cosh M, h1]
626 have h3 : (0:ℝ) ≤ Real.cosh G := le_trans zero_le_one (Real.one_le_cosh G)
627 exact mul_nonneg (mul_nonneg (by norm_num) h2) h3
628 have hE2pos : 0 < E2 := by
629 rw [hE2def]
630 linarith [hprod_nn, Real.one_le_cosh (M + G)]
631 have hq0 : 0 ≤ q := by
632 have h1 : E2⁻¹ ≤ 1 := by
633 rw [inv_le_one_iff₀]
634 right
635 rw [hE2def]
636 linarith [hprod_nn, Real.one_le_cosh (M + G)]
637 linarith
638 have hq1 : q < 1 := by
639 have h1 : (0:ℝ) < E2⁻¹ := by positivity
640 linarith
641 refine ⟨q, hq0, hq1, ?_⟩
642 intro k
643 induction k with
644 | zero => simp [strainOrbit]
645 | succ k ih =>
646 have hbound : |strainOrbit a s₀ k| ≤ M := by
647 have hd : |strainOrbit a s₀ k - sstar| ≤ |s₀ - sstar| := by
648 exact le_trans ih (by
649 have hq1' : q ^ k ≤ 1 := pow_le_one₀ hq0 (le_of_lt hq1)
650 calc q ^ k * |s₀ - sstar| ≤ 1 * |s₀ - sstar| :=
651 mul_le_mul_of_nonneg_right hq1' (abs_nonneg _)
652 _ = |s₀ - sstar| := one_mul _)
653 calc |strainOrbit a s₀ k|
654 = |sstar + (strainOrbit a s₀ k - sstar)| := by ring_nf
655 _ ≤ |sstar| + |strainOrbit a s₀ k - sstar| := abs_add_le _ _
656 _ ≤ |sstar| + |s₀ - sstar| := add_le_add_right hd |sstar|
657 _ = M := rfl
658 have hηk : E2⁻¹ ≤ strainStepSize a (strainOrbit a s₀ k) := by
659 have hE : strainEnvelope a (strainOrbit a s₀ k) ≤ E2 := by
660 apply max_le
661 · have hcosh : Real.cosh (strainOrbit a s₀ k) ≤ Real.cosh M := by
662 rw [← Real.cosh_abs (strainOrbit a s₀ k)]
663 exact cosh_le_cosh_of_nonneg_of_le (abs_nonneg _) hbound
664 have hsinh : |Real.sinh (strainOrbit a s₀ k)| ≤ Real.sinh M := by
665 rw [abs_sinh_eq_sinh_abs]
666 exact Real.sinh_strictMono.monotone hbound
667 have hg : |strainResidual a (strainOrbit a s₀ k)| ≤ G := by
668 unfold strainResidual
669 calc |Real.sinh (strainOrbit a s₀ k) - a|
670 ≤ |Real.sinh (strainOrbit a s₀ k)| + |a| := abs_sub _ _
671 _ ≤ Real.sinh M + |a| := add_le_add hsinh le_rfl
672 _ = G := rfl
673 have hprod : |Real.sinh (strainOrbit a s₀ k)|
674 * |strainResidual a (strainOrbit a s₀ k)| ≤ Real.sinh M * G :=
675 mul_le_mul hsinh hg (abs_nonneg _)
676 (by simpa using Real.sinh_strictMono.monotone hMnn)
677 calc 2 * (Real.cosh (strainOrbit a s₀ k) / 2
678 + |Real.sinh (strainOrbit a s₀ k)|
679 * |strainResidual a (strainOrbit a s₀ k)| / 6)
680 * Real.cosh (|strainResidual a (strainOrbit a s₀ k)|)
681 ≤ 2 * (Real.cosh M + Real.sinh M * G / 6) * Real.cosh G := by
682 apply mul_le_mul
683 · apply mul_le_mul_of_nonneg_left _ (by norm_num : (0:ℝ) ≤ 2)
684 linarith [hcosh, hprod, Real.one_le_cosh M]
685 · exact cosh_le_cosh_of_nonneg_of_le (abs_nonneg _) hg
686 · positivity
687 · positivity
688 _ ≤ 2 * (Real.cosh M + Real.sinh M * G / 6) * Real.cosh G
689 + Real.cosh (M + G) :=
690 le_add_of_nonneg_right (by positivity :
691 (0:ℝ) ≤ Real.cosh (M + G))
692 _ = E2 := rfl
693 · have hsinh : |Real.sinh (strainOrbit a s₀ k)| ≤ Real.sinh M := by
694 rw [abs_sinh_eq_sinh_abs]
695 exact Real.sinh_strictMono.monotone hbound
696 have hg : |strainResidual a (strainOrbit a s₀ k)| ≤ G := by
697 unfold strainResidual
698 calc |Real.sinh (strainOrbit a s₀ k) - a|
699 ≤ |Real.sinh (strainOrbit a s₀ k)| + |a| := abs_sub _ _
700 _ ≤ Real.sinh M + |a| := add_le_add hsinh le_rfl
701 _ = G := rfl
702 calc Real.cosh (|strainOrbit a s₀ k|
703 + |strainResidual a (strainOrbit a s₀ k)|)
704 ≤ Real.cosh (M + G) :=
705 cosh_le_cosh_of_nonneg_of_le (by positivity)
706 (add_le_add hbound hg)
707 _ ≤ 2 * (Real.cosh M + Real.sinh M * G / 6) * Real.cosh G
708 + Real.cosh (M + G) :=
709 le_add_of_nonneg_left (by positivity :
710 (0:ℝ) ≤ 2 * (Real.cosh M + Real.sinh M * G / 6) * Real.cosh G)
711 _ = E2 := rfl
712 rw [strainStepSize]
713 exact (inv_le_inv₀ hE2pos (strainEnvelope_pos _ _)).mpr hE
714 have hstep := contraction_one_dim a (strainOrbit a s₀ k)
715 calc |strainStep1 a (strainOrbit a s₀ k) - sstar|
716 ≤ (1 - strainStepSize a (strainOrbit a s₀ k))
717 * |strainOrbit a s₀ k - sstar| := hstep
718 _ ≤ (1 - E2⁻¹) * |strainOrbit a s₀ k - sstar| := by
719 apply mul_le_mul_of_nonneg_right _ (abs_nonneg _)
720 linarith [hηk]
721 _ ≤ (1 - E2⁻¹) * (q ^ k * |s₀ - sstar|) :=
722 mul_le_mul_of_nonneg_left ih (by linarith [hq0, hq1])
723 _ = q ^ (k + 1) * |s₀ - sstar| := by rw [hqdef, pow_succ]; ring
724
725/-- **THEOREM (convergence to the sourced stationary point).** -/
726theorem strainOrbit_tendsto (a : ℝ) (s₀ : ℝ) :
727 Tendsto (strainOrbit a s₀) atTop (𝓝 (Real.arsinh a)) := by
728 obtain ⟨q, hq0, hq1, hbound⟩ := strainOrbit_abs_le a s₀
729 rw [tendsto_iff_dist_tendsto_zero]
730 have hgeom : Tendsto (fun k => q ^ k * |s₀ - Real.arsinh a|) atTop (𝓝 0) := by
731 have hpow : Tendsto (fun k => q ^ k) atTop (𝓝 0) :=
732 tendsto_pow_atTop_nhds_zero_of_lt_one hq0 hq1
733 have := hpow.mul_const |s₀ - Real.arsinh a|
734 simpa [zero_mul] using this
735 have habs := (squeeze_zero (fun k => abs_nonneg _) hbound hgeom).abs
736 simpa [Real.dist_eq, abs_zero] using habs
737
738/-! ## §5. The vector form on the link -/
739
740/-- The componentwise step on the link. -/
741noncomputable def strainStepVec (n : ℕ) (c : ℝ) (t : Fin n → ℝ) : Fin n → ℝ :=
742 fun i => strainStep1 (c / n) (t i)
743
744/-- The sourced action is the sum of the per-channel costs. -/
745theorem sourcedAction_eq_sum_sourceCost1 (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
746 sourcedAction n c t = ∑ i, sourceCost1 (c / n) (t i) := by
747 unfold sourceCost1
748 exact sourcedAction_eq_sum n c t
749
750/-- **THEOREM (the sourced action decreases).** -/
751theorem sourcedAction_step_le (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
752 sourcedAction n c (strainStepVec n c t)
753 ≤ sourcedAction n c t
754 - (1/2) * ∑ i, strainStepSize (c / n) (t i)
755 * strainResidual (c / n) (t i) ^ 2 := by
756 rw [sourcedAction_eq_sum_sourceCost1, sourcedAction_eq_sum_sourceCost1]
757 rw [Finset.mul_sum, ← Finset.sum_sub_distrib]
758 apply Finset.sum_le_sum
759 intro i _
760 have h := descent_one_dim (c / n) (t i)
761 show sourceCost1 (c / n) (strainStep1 (c / n) (t i))
762 ≤ sourceCost1 (c / n) (t i)
763 - 1 / 2 * (strainStepSize (c / n) (t i) * strainResidual (c / n) (t i) ^ 2)
764 linarith
765
766/-- **THEOREM (strict decrease of the sourced action off the minimizer).** -/
767theorem sourcedAction_step_lt (n : ℕ) (c : ℝ) (t : Fin n → ℝ)
768 (h : ∃ i, strainResidual (c / n) (t i) ≠ 0) :
769 sourcedAction n c (strainStepVec n c t) < sourcedAction n c t := by
770 rw [sourcedAction_eq_sum_sourceCost1, sourcedAction_eq_sum_sourceCost1,
771 ← sub_neg, ← Finset.sum_sub_distrib,
772 show (0 : ℝ) = ∑ i : Fin n, (0 : ℝ) from (Finset.sum_const_zero).symm]
773 obtain ⟨i, hi⟩ := h
774 apply Finset.sum_lt_sum
775 · intro j _
776 calc sourceCost1 (c / n) (strainStep1 (c / n) (t j))
777 - sourceCost1 (c / n) (t j)
778 ≤ -(strainStepSize (c / n) (t j) / 2)
779 * strainResidual (c / n) (t j) ^ 2 :=
780 descent_one_dim (c / n) (t j)
781 _ ≤ 0 := by
782 have hη : 0 < strainStepSize (c / n) (t j) := strainStepSize_pos _ _
783 have hg : (0:ℝ) ≤ strainResidual (c / n) (t j) ^ 2 := by positivity
784 nlinarith [hη, hg]
785 · exact ⟨i, Finset.mem_univ i, sub_neg.mpr (descent_one_dim_lt (c / n) (t i) hi)⟩
786
787/-- **THEOREM (fixed points of the vector step).** -/
788theorem stepVec_fixed_iff_minimizer (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
789 strainStepVec n c t = t ↔ t = sourcedMinimizer n c := by
790 constructor
791 · intro h
792 funext i
793 have hi : strainStep1 (c / n) (t i) = t i := congrFun h i
794 exact (step_fixed_iff_arsinh (c / n) (t i)).mp hi
795 · intro h
796 rw [h]
797 funext i
798 exact (step_fixed_iff_arsinh (c / n) _).mpr rfl
799
800/-- The componentwise orbit on the link. -/
801noncomputable def strainStepVecOrbit (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
802 ℕ → (Fin n → ℝ)
803 | 0 => t
804 | k + 1 => strainStepVec n c (strainStepVecOrbit n c t k)
805
806/-- The componentwise orbit is the per-channel orbit. -/
807theorem strainStepVecOrbit_apply (n : ℕ) (c : ℝ) (t : Fin n → ℝ) (k : ℕ)
808 (i : Fin n) :
809 strainStepVecOrbit n c t k i = strainOrbit (c / n) (t i) k := by
810 induction k with
811 | zero => rfl
812 | succ j ih =>
813 show strainStep1 (c / n) (strainStepVecOrbit n c t j i)
814 = strainStep1 (c / n) (strainOrbit (c / n) (t i) j)
815 rw [ih]
816
817/-- **THEOREM (each channel converges to the minimizer).** -/
818theorem strainStepVec_tendsto_minimizer (n : ℕ) (c : ℝ) (t : Fin n → ℝ)
819 (i : Fin n) :
820 Tendsto (fun k => strainStepVecOrbit n c t k i) atTop
821 (𝓝 (Real.arsinh (c / n))) := by
822 rw [show (fun k => strainStepVecOrbit n c t k i)
823 = (fun k => strainOrbit (c / n) (t i) k) from
824 funext (strainStepVecOrbit_apply n c t · i)]
825 exact strainOrbit_tendsto _ _
826
827end
828
829end StrainDescent
830end SevenGaps
831end Gravity
832end IndisputableMonolith
833