AnalyticConstruction.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

The actual positive-displacement map on the L² unit ball

Every elementary field of the generic tube and correction constructions is instantiated here by the explicit scalar profiles and the concrete L² curve. The final map has no geometric or analytic certificate as a hypothesis.

def OAI.ThompsonNonamenability.Analytic.separationAtScale line 22
theorem OAI.ThompsonNonamenability.Analytic.separationAtScale_pos line 25
theorem OAI.ThompsonNonamenability.Analytic.separationAtScale_le line 28
def OAI.ThompsonNonamenability.Analytic.regularCurve line 33
Source documentation
The proved elementary geometry of the actual radial oscillating curve.
```
def regularCurve : RegularCurveData Hilbert where
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.RegularCurveData, OAI.ThompsonNonamenability.Analytic.Hilbert
def OAI.ThompsonNonamenability.Analytic.tubeRadius line 48
Source documentation
The radius comes from proved uniform separation and the explicit speed bounds.
```
def tubeRadius : ℝ := regularCurve.rho
```
theorem OAI.ThompsonNonamenability.Analytic.tubeRadius_pos line 50
theorem OAI.ThompsonNonamenability.Analytic.tubeRadius_lt line 52
def OAI.ThompsonNonamenability.Analytic.correctionData line 58
Source documentation
The literal radial, angular, and rotation inputs to the correction formula.
```
def correctionData : CorrectionData regularCurve where
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.CorrectionData, OAI.ThompsonNonamenability.Analytic.regularCurve
def OAI.ThompsonNonamenability.Analytic.G line 82
Source documentation
The explicit correction, restricted to the shared actual closed unit ball.
```
def G (x : Ball) : Hilbert := correctionData.G (x : Hilbert)
```
Mentions: OAI.ThompsonNonamenability.Analytic.Ball, OAI.ThompsonNonamenability.Analytic.Hilbert
theorem OAI.ThompsonNonamenability.Analytic.G_norm_lower line 84
theorem OAI.ThompsonNonamenability.Analytic.G_outer line 87
theorem OAI.ThompsonNonamenability.Analytic.G_sub_norm_le line 90
theorem OAI.ThompsonNonamenability.Analytic.normalizationRadius_pos line 94
def OAI.ThompsonNonamenability.Analytic.displacementMap line 98
Source documentation
Negative radial normalization of the concrete nonvanishing correction.
```
def displacementMap : Ball → Ball :=
…
```
Mentions: OAI.ThompsonNonamenability.Analytic.Ball
theorem OAI.ThompsonNonamenability.Analytic.displacementMap_norm line 101
theorem OAI.ThompsonNonamenability.Analytic.displacementMap_displacement line 104
def OAI.ThompsonNonamenability.Analytic.displacementLipschitzConstant line 108
theorem OAI.ThompsonNonamenability.Analytic.displacementLipschitzConstant_pos line 111
theorem OAI.ThompsonNonamenability.Analytic.displacementMap_lipschitz line 115

theorem OAI.ThompsonNonamenability.Analytic.exists_displacementMap line 121

Source documentation

The unconditional analytic input used by the finite correlation proof.

theorem exists_displacementMap :
    ∃ (f : UnitBall Hilbert → UnitBall Hilbert) (L : ℝ),
      0 < L ∧
      (∀ x y, ‖(f x : Hilbert) - f y‖ ≤ L * ‖(x : Hilbert) - y‖) ∧
      (∀ x, (1 / 2 : ℝ) ≤ ‖(f x : Hilbert) - x‖) :=
…

Mentions: OAI.ThompsonNonamenability.UnitBall, OAI.ThompsonNonamenability.Analytic.Hilbert