StationaryContraction.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

The conditional stationary correction argument

Exact rational estimates and the Banach fixed-point step from OpenAI, Stationary instability and nonuniqueness for axisymmetric swirl-free Navier–Stokes, section “Correcting the stationary profile”. The inverse, change of variables and bilinear map satisfy explicit operator norm hypotheses.

def OAI.StationaryNS.kappa line 25
Source documentation
The weight in the stationary profile norm D.
```
def kappa : ℝ := 3 / 25
```
def OAI.StationaryNS.eta line 28
Source documentation
Coercivity margin, η = .29.
```
def eta : ℝ := 29 / 100
```
def OAI.StationaryNS.residualBound line 31
Source documentation
Upper bound F₀ = 5.1 × 10⁻⁷ for the stationary residual.
```
def residualBound : ℝ := 51 / 100000000
```
def OAI.StationaryNS.nonlinearBound line 34
Source documentation
Upper bound for the transformed nonlinearity, c = .271.
```
def nonlinearBound : ℝ := 271 / 1000
```
def OAI.StationaryNS.correctionRadius line 37
Source documentation
Radius of the contraction ball, r₀ = 2 F₀ / η.
```
def correctionRadius : ℝ := 2 * residualBound / eta
```
Mentions: OAI.StationaryNS.residualBound, OAI.StationaryNS.eta
def OAI.StationaryNS.targetError line 40
Source documentation
The strict correction bound 2.216 × 10⁻⁴.
```
def targetError : ℝ := 277 / 1250000
```
theorem OAI.StationaryNS.lipschitz_budget line 43
Source documentation
The Lipschitz bound .027 is strictly less than one.
```
theorem lipschitz_budget :
    2 * nonlinearBound * 63 ^ 2 * correctionRadius / eta < (27 / 1000 : ℝ) := by
…
```
Mentions: OAI.StationaryNS.nonlinearBound, OAI.StationaryNS.correctionRadius, OAI.StationaryNS.eta
theorem OAI.StationaryNS.correction_budget line 48
Source documentation
The norm bound on the actual correction is strictly below the stated decimal.
```
theorem correction_budget : (63 : ℝ) * correctionRadius < targetError := by
…
```
Mentions: OAI.StationaryNS.correctionRadius, OAI.StationaryNS.targetError
theorem OAI.StationaryNS.ball_budget line 52
Source documentation
The closed-ball invariance inequality at the correction radius.
```
theorem ball_budget :
    eta⁻¹ * (residualBound + nonlinearBound * 63 ^ 2 * correctionRadius ^ 2) ≤
      correctionRadius := by
…
```
Mentions: OAI.StationaryNS.eta, OAI.StationaryNS.residualBound, OAI.StationaryNS.nonlinearBound, OAI.StationaryNS.correctionRadius
theorem OAI.StationaryNS.coercivity_budget line 58
Source documentation
Common coercivity margin after the moment-residual error.
```
theorem coercivity_budget :
    (29 / 100 : ℝ) < 109 / 350 - (164 / 25) * (3 / 2500) := by
…
```
theorem OAI.StationaryNS.endpoint_budget line 63
Source documentation
Endpoint error allowed by the largest of the three change-of-variable bounds.
```
theorem endpoint_budget :
    2 * nonlinearBound * targetError * 828 < (11 / 100 : ℝ) := by
…
```
Mentions: OAI.StationaryNS.nonlinearBound, OAI.StationaryNS.targetError
theorem OAI.StationaryNS.matrix_budget line 68
Source documentation
The certified total matrix error is smaller than the certified spectral gap.
```
theorem matrix_budget :
    (151 / 50000 : ℝ) < 669 / 100000 ∧
      (669 / 100000 : ℝ) < eta / (eta + (164 / 25) * (164 / 25 + 3 / 2500)) := by
…
```
Mentions: OAI.StationaryNS.eta
def OAI.StationaryNS.correctionMap line 82
Source documentation
The actual quadratic fixed-point map from the stationary correction argument, written for arbitrary Banach spaces. I is the modified inverse, T = I+G₀, and N is the projected tensor-divergence bilinear map.
```
def correctionMap (I : Y →L[ℝ] E) (T : E →L[ℝ] E)
    (N : E →L[ℝ] E →L[ℝ] Y) (f : Y) (w : E) : E :=
…
```
theorem OAI.StationaryNS.quadratic_difference line 88
Source documentation
Bilinearity gives the quadratic difference identity, with no differential or inverse-operator assumption.
```
theorem quadratic_difference (N : E →L[ℝ] E →L[ℝ] Y) (x y : E) :
    N x x - N y y = N (x - y) x + N y (x - y) := by
…
```

theorem OAI.StationaryNS.quadratic_norm line 94

Source documentation

Norm estimate for the quadratic term, using its actual bilinear operator norm.

theorem quadratic_norm (N : E →L[ℝ] E →L[ℝ] Y) (T : E →L[ℝ] E)
    (hN : ‖N‖ ≤ nonlinearBound) (hT : ‖T‖ ≤ 63) (x : E) :
    ‖N (T x) (T x)‖ ≤ nonlinearBound * 63 ^ 2 * ‖x‖ ^ 2 := by
…

Mentions: OAI.StationaryNS.nonlinearBound

theorem OAI.StationaryNS.quadratic_lipschitz line 112

Source documentation

Lipschitz estimate for the quadratic term on a norm ball.

theorem quadratic_lipschitz (N : E →L[ℝ] E →L[ℝ] Y) (T : E →L[ℝ] E)
    (hN : ‖N‖ ≤ nonlinearBound) (hT : ‖T‖ ≤ 63)
    {x y : E} (hx : ‖x‖ ≤ correctionRadius) (hy : ‖y‖ ≤ correctionRadius) :
    ‖N (T x) (T x) - N (T y) (T y)‖ ≤
      2 * nonlinearBound * 63 ^ 2 * correctionRadius * ‖x - y‖ := by
…

Mentions: OAI.StationaryNS.nonlinearBound, OAI.StationaryNS.correctionRadius

theorem OAI.StationaryNS.stationary_contraction line 146

Source documentation

The stationary correction exists under explicit inverse and bilinear operator bounds.

theorem stationary_contraction [CompleteSpace E] (I : Y →L[ℝ] E) (T : E →L[ℝ] E)
    (N : E →L[ℝ] E →L[ℝ] Y) (f : Y)
    (hI : ‖I‖ ≤ eta⁻¹) (hT : ‖T‖ ≤ 63) (hN : ‖N‖ ≤ nonlinearBound)
    (hf : ‖f‖ ≤ residualBound) :
    ∃ w : E, ‖w‖ ≤ correctionRadius ∧
      correctionMap I T N f w = w ∧ ‖T w‖ < targetError := by
…

Mentions: OAI.StationaryNS.eta, OAI.StationaryNS.nonlinearBound, OAI.StationaryNS.residualBound, OAI.StationaryNS.correctionRadius, OAI.StationaryNS.correctionMap, OAI.StationaryNS.targetError