AnalyticCurveBounds.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the actual Hilbert curve

The derivative estimate uses first-derivative product differences on the oscillating part and the exact straight-tail formula. No second derivative at a profile junction is assumed.

theorem OAI.ThompsonNonamenability.Analytic.a_sub_abs_le line 22
theorem OAI.ThompsonNonamenability.Analytic.aDeriv_sub_abs_le line 26
theorem OAI.ThompsonNonamenability.Analytic.theta_sub_abs_le line 31
theorem OAI.ThompsonNonamenability.Analytic.thetaDeriv_sub_abs_le line 34
theorem OAI.ThompsonNonamenability.Analytic.waveDeriv_norm_le_one line 39
theorem OAI.ThompsonNonamenability.Analytic.v_sub_norm_le_forward line 43
theorem OAI.ThompsonNonamenability.Analytic.v_lipschitz line 46
theorem OAI.ThompsonNonamenability.Analytic.smul_sub_smul_norm_le line 53
Source documentation
A product difference estimate with the coefficient difference at the first vector.
```
theorem smul_sub_smul_norm_le (r q : ℝ) (x y : Hilbert) :
    ‖r • x - q • y‖ ≤ |r - q| * ‖x‖ + |q| * ‖x - y‖ := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.q, OAI.ThompsonNonamenability.Analytic.Hilbert
theorem OAI.ThompsonNonamenability.Analytic.angularCoeff_bounds line 63
Source documentation
The second coefficient in the derivative is nonnegative and uniformly bounded.
```
theorem angularCoeff_bounds {t : ℝ} (ht : 1 ≤ t) :
    0 ≤ a t * thetaDeriv t ∧ a t * thetaDeriv t ≤ 5 / 16 := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.a, OAI.ThompsonNonamenability.Analytic.thetaDeriv
theorem OAI.ThompsonNonamenability.Analytic.angularCoeff_sub_abs_le line 70
theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_speed_upper line 91
Source documentation
A global upper speed bound, including the unbounded negative straight tail.
```
theorem gammaDeriv_speed_upper (t : ℝ) : ‖gammaDeriv t‖ ≤ 7 / 16 := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.gammaDeriv
theorem OAI.ThompsonNonamenability.Analytic.gamma_sub_norm_le_forward line 108
Source documentation
The ordinary mean value estimate applied to the proved derivative.
```
theorem gamma_sub_norm_le_forward (s t : ℝ) : ‖gamma s - gamma t‖ ≤ (7 / 16) * |s - t| := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.gamma
theorem OAI.ThompsonNonamenability.Analytic.gamma_lipschitz line 115
theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_sub_norm_le_tail line 122
Source documentation
On the oscillating tail, product differences give the derivative estimate.
```
private theorem gammaDeriv_sub_norm_le_tail {s t : ℝ} (hs : 1 ≤ s) (ht : 1 ≤ t) :
    ‖gammaDeriv s - gammaDeriv t‖ ≤ |s - t| := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.gammaDeriv
theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_sub_norm_le_forward line 154
Source documentation
The constant derivative on the straight tail joins the oscillating estimate at one.
```
theorem gammaDeriv_sub_norm_le_forward (s t : ℝ) :
    ‖gammaDeriv s - gammaDeriv t‖ ≤ |s - t| := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.gammaDeriv
theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_lipschitz line 181
theorem OAI.ThompsonNonamenability.Analytic.u_sub_norm_le_forward line 188
Source documentation
Normalize the actual nonzero tangent using its proved speed lower bound.
```
theorem u_sub_norm_le_forward (s t : ℝ) : ‖u s - u t‖ ≤ 16 * |s - t| := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.u
theorem OAI.ThompsonNonamenability.Analytic.u_lipschitz line 197
theorem OAI.ThompsonNonamenability.Analytic.v_sub_norm_le line 204
Source documentation
Pairwise estimates with the base parameter first.
```
theorem v_sub_norm_le (s t : ℝ) : ‖v t - v s‖ ≤ |t - s| :=
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.v
theorem OAI.ThompsonNonamenability.Analytic.gamma_sub_norm_le line 207
theorem OAI.ThompsonNonamenability.Analytic.gammaDeriv_sub_norm_le line 210
theorem OAI.ThompsonNonamenability.Analytic.u_sub_norm_le line 213
theorem OAI.ThompsonNonamenability.Analytic.lipschitzWith_v line 216
theorem OAI.ThompsonNonamenability.Analytic.lipschitzWith_u line 218