AnalyticCorrection.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Global gluing of the explicit Hilbert correction

The cutoff tails tend to zero at the actual tube boundary. These estimates give the mixed inside/outside case; a uniform bound on the additive change handles distant pairs. Together with the local tube estimate, this covers every pair of points, including the boundary itself.

theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.rotated_residual_sub_bound line 28
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.change_bound line 34
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.change_uniform_bound line 51
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.change_tail_bound line 62
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.radius_gap_le line 81
Source documentation
Distance to an outside point controls the remaining radius of the tube.
```
theorem radius_gap_le (x : C.tube) {y : E} (hy : y ∉ C.tube) :
    C.rho - ‖C.residual x‖ ≤ ‖(x : E) - y‖ := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_outside_bound line 93
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.G_sub_self_bound line 111
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.G_distant_bound line 120
Source documentation
The distant-pair estimate uses only the bounded additive change.
```
theorem G_distant_bound (x y : E) (hxy : C.rho ≤ ‖x - y‖) :
    ‖D.G x - D.G y‖ ≤ (5 + 7 / (8 * C.rho)) * ‖x - y‖ := by
…
```
def OAI.ThompsonNonamenability.Analytic.CorrectionData.lipschitzConstant line 138
Source documentation
A finite positive constant valid for all pairs in the ambient Hilbert space.
```
def lipschitzConstant (_ : CorrectionData C) : ℝ :=
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.CorrectionData
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.lipschitzConstant_pos line 141
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.G_lipschitz line 144