PrimitiveSlowScales.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

The finite slow scales in the high-accuracy primitive realization. These choices precede every accuracy order in its mean iteration.

def OAI.ClosedSurfaceR4.PrimitiveRealization.amplitudeExponent line 10
def OAI.ClosedSurfaceR4.PrimitiveRealization.scaleExponent line 11
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.amplitudeExponent_pos line 13
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.amplitudeExponent_zero line 17
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.amplitudeExponent_succ line 20
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.amplitudeExponent_lower line 25
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.exists_amplitude_steps line 32
Source documentation
A finite number of amplitude improvements achieves any prescribed finite metric order. No derivative count enters the later accuracy choices.
```
lemma exists_amplitude_steps (R N : ℕ) :
    ∃ steps : ℕ, 1 ≤ steps ∧ (N : ℝ)+R+1 < 2*amplitudeExponent steps := by
…
```
Mentions: OAI.ClosedSurfaceR4.PrimitiveRealization.amplitudeExponent
theorem OAI.ClosedSurfaceR4.PrimitiveRealization.exists_slow_exponent line 45
Source documentation
The loss powers determine one slow exponent before choosing the finite substitution accuracies in the primitive realization argument.
```
theorem exists_slow_exponent (R N L : ℕ) (hL : N+R < L) (p p₁ : ℝ) :
    ∃ σ : ℝ, 0 < σ ∧ σ < 1 ∧ σ*(p₁+2) < 1 ∧ σ*p < 1/2 ∧
      σ < 1/16 ∧ (L : ℝ)-R-σ*p₁ > N := by
…
```
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.scaleExponent_bounds line 74
lemma OAI.ClosedSurfaceR4.PrimitiveRealization.scaleExponent_step line 85

theorem OAI.ClosedSurfaceR4.PrimitiveRealization.slow_step_positive_powers line 92

Source documentation

Both the normalized cubic remainder and the C3 displacement decay at every stage of the finite slow iteration.

theorem slow_step_positive_powers {σ : ℝ} (hσ : 0 < σ) (hσsmall : σ < 1/16)
    {steps j : ℕ} (hs : 1 ≤ steps) (hj : j < steps) :
    0 < 3*amplitudeExponent j-scaleExponent σ steps (j+1)-2*amplitudeExponent (j+1) ∧
    0 < amplitudeExponent j-2*scaleExponent σ steps (j+1) ∧
    0 < min (σ/(steps : ℝ)) (1/2) := by
…

Mentions: OAI.ClosedSurfaceR4.PrimitiveRealization.amplitudeExponent, OAI.ClosedSurfaceR4.PrimitiveRealization.scaleExponent

theorem OAI.ClosedSurfaceR4.PrimitiveRealization.exists_step_accuracy line 105
Source documentation
Accuracy orders can be chosen after all scale and loss exponents are fixed; this prevents a circular dependence of the slow scale on accuracy.
```
theorem exists_step_accuracy {κ : ℝ} (hκ : 0 < κ) (j : ℕ) :
    ∃ q : ℕ, amplitudeExponent j+κ*q > 2*amplitudeExponent (j+1) := by
…
```
Mentions: OAI.ClosedSurfaceR4.PrimitiveRealization.amplitudeExponent

theorem OAI.ClosedSurfaceR4.PrimitiveRealization.slow_parameter_bound line 114

Source documentation

The perturbed mean parameter has a positive decay exponent independent of the accuracy order chosen at this stage.

theorem slow_parameter_bound {σ p z : ℝ} (hσ : 0 < σ) (hp : 0 ≤ p)
    (hσp : σ*p < 1/2) (hz : 0 < z) (hz1 : z ≤ 1)
    {steps j : ℕ} (hs : 1 ≤ steps) (hj : j < steps) :
    z^(scaleExponent σ steps (j+1))/z^(scaleExponent σ steps j)+
      z/(z^(scaleExponent σ steps (j+1)))^p ≤
        2*z^(min (σ/(steps : ℝ)) (1/2)) := by
…

Mentions: OAI.ClosedSurfaceR4.PrimitiveRealization.scaleExponent

theorem OAI.ClosedSurfaceR4.PrimitiveRealization.normalized_slow_error_threshold line 139

Source documentation

A small-increment error with the paper's two terms becomes arbitrarily small after division by the next amplitude squared. This is the finite inductive step used to improve the primitive's metric accuracy.

theorem normalized_slow_error_threshold {d d' b κ C e : ℝ} {q : ℕ}
    (hC : 0 ≤ C) (he : 0 < e)
    (ha : 0 < d+κ*q-2*d') (hb : 0 < 3*d-b-2*d') :
    ∃ ζ : ℝ, 0 < ζ ∧ ζ ≤ 1 ∧ ∀ z : ℝ, 0 < z → z < ζ →
      ∀ η : ℝ, 0 ≤ η → η ≤ 2*z^κ →
      (C*(z^d*η^q+(z^d)^3/z^b))/(z^d')^2 < e := by
…