CorrectionNonzero.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

The correction stays away from zero and fixes the outer annulus

The lower bound follows from the two orthogonal inner regions and the two parameter cases in the outer tube region. All estimates concern the explicit formula defined in CorrectionData.

theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.norm_left_le_of_perp line 28
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.norm_right_le_of_perp line 33
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.radial_perp line 38

theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_inner_formula line 44

Source documentation

The orthogonal formula throughout the inner half of the tube.

theorem inside_inner_formula (x : C.tube) (hr : ‖C.residual x‖ ≤ C.rho / 2) :
    D.inside x =
      (D.a (C.parameter x) + beta C.rho ‖C.residual x‖ * D.q (C.parameter x)) •
        D.v (C.parameter x) + D.R (C.parameter x) (C.residual x) := by
…

Mentions: OAI.ThompsonNonamenability.Analytic.beta

theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_inner_radial_lower line 51
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_inner_residual_lower line 62
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.residual_blend_norm_le line 74
Source documentation
Convex interpolation between the identity and the rotation is a contraction on each individual residual.
```
theorem residual_blend_norm_le (x : C.tube) :
    ‖(1 - chi C.rho ‖C.residual x‖) • C.residual x +
      chi C.rho ‖C.residual x‖ • D.R (C.parameter x) (C.residual x)‖ ≤
      ‖C.residual x‖ := by
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.chi

theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_early_formula line 91

Source documentation

On the early part of the curve the rotation term vanishes identically.

theorem inside_early_formula (x : C.tube) (ht : C.parameter x ≤ 1) :
    D.inside x =
      (D.a (C.parameter x) + beta C.rho ‖C.residual x‖ * D.q (C.parameter x)) •
        D.v (C.parameter x) + C.residual x := by
…

Mentions: OAI.ThompsonNonamenability.Analytic.beta

theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_early_residual_lower line 102
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_lower line 111
Source documentation
The four tube regions give the same positive lower bound.
```
theorem inside_lower (x : C.tube) : C.rho / 4 ≤ ‖D.inside x‖ := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.G_lower line 145
Source documentation
The explicit correction has a uniform positive norm everywhere.
```
theorem G_lower (x : E) : C.rho / 4 ≤ ‖D.G x‖ := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.inside_outer line 160
Source documentation
Any tube point of norm at least one half has parameter on the unchanged negative ray, so both additive corrections vanish.
```
theorem inside_outer (x : C.tube) (hx : 1 / 2 ≤ ‖(x : E)‖) :
    D.inside x = (x : E) := by
…
```
theorem OAI.ThompsonNonamenability.Analytic.CorrectionData.G_outer line 187
Source documentation
The correction is exactly the identity on the whole outer annulus.
```
theorem G_outer (x : E) (hx : 1 / 2 ≤ ‖x‖) : D.G x = x := by
…
```