TransferGapRanges.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The manuscript's gaps give both frequency cutoffs and history rigidity

def OAI.Ostmann.transferErrorScale line 15
def OAI.Ostmann.transferNextGap line 19
Source documentation
The gap for step j+1.
```
noncomputable def transferNextGap (Δ m : ℝ) (j : ℕ) : ℝ :=
…
```
theorem OAI.Ostmann.transfer_gap_minus_error line 22
theorem OAI.Ostmann.transfer_error_reserve line 28

theorem OAI.Ostmann.eventually_transfer_reserve line 37

Source documentation

A single sufficiently-large-m cutoff gives every transfer level its fixed covering and integer-rounding reserve.

theorem eventually_transfer_reserve (C : ℝ) :
    ∀ᶠ m : ℝ in atTop, ∀ Δ : ℝ, ∀ j : ℕ,
      Real.log 4 + 2 * C < transferNextGap Δ m j - transferErrorScale Δ m j ∧
      Real.log 4 + 2 * C < transferErrorScale Δ m (j + 1) -
        (transferErrorScale Δ m j + transferNextGap Δ m j) := by
…

Mentions: OAI.Ostmann.transferNextGap, OAI.Ostmann.transferErrorScale

theorem OAI.Ostmann.transfer_integer_rigidity_gap line 52

Source documentation

The positive-product ranges make the determinant gap strict.

theorem transfer_integer_rigidity_gap (K B R : ℕ) (T Δ E C : ℝ)
    (hK : (K : ℝ) ≤ Real.exp (T + C)) (hB : (B : ℝ) ≤ Real.exp E)
    (hR : Real.exp (T + Δ - C) ≤ R) (hgap : Real.log 2 + 2 * C < Δ - E) :
    2 * K * B < R := by
…

theorem OAI.Ostmann.transfer_integer_frequency_cutoff line 67

Source documentation

Rounding the new exponential frequency cutoff downward costs at most one factor two, which is covered by the same square-root reserve.

theorem transfer_integer_frequency_cutoff (M H B V : ℕ) (T Δ E E' C : ℝ)
    (hM : Real.exp (T - C) ≤ M) (hH : (H : ℝ) ≤ Real.exp (T + Δ + C))
    (hB : (B : ℝ) ≤ Real.exp E) (hV : Real.exp E' ≤ 2 * V)
    (hgap : Real.log 4 + 2 * C + E + Δ ≤ E') :
    2 * B * H ≤ V * M := by
…