OAI/NumberTheory/Ostmann/Arithmetic/MovingCompensationFrequency.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.smoothGiant_integer_cell_lower line 10
2. theorem OAI.Ostmann.movingProductNaturalCutoff_compensation_scale line 17

   Source documentation

   This discharges the scale premise for the original, unconditioned compensation draw and every integer in the full outer cell.

   theorem movingProductNaturalCutoff_compensation_scale {σ : Type} [Fintype σ]
       (value : σ → ℕ) (μ : ℕ → σ → ℝ) (G c : ℕ → ℝ)
       (hμ : ∀ j x, μ j x ≠ 0 → Real.exp (c j - 1) ≤ (value x : ℝ))
       (W Y m : ℝ) (hm : 64 ≤ m) (hY : Y ≤ W)
       (hgap : ∀ j, 2 * movingCellPivotExponent G c j ≤
         movingProductExponent (movingCellPivotExponent G c) W j)
       (n : ℕ) (hH : 0 ≤ movingProductExponent (movingCellPivotExponent G c) W n -
         movingCellPivotExponent G c n)
       (u : TreeLeafIndex n × Fin 4 → σ) (hu : (∏ i, μ n (u i)) ≠ 0)
       (p : ℕ) (hp : Real.exp (G (n + 1) - 1) ≤ (p : ℝ)) :
       2 * movingProductNaturalCutoff (movingCellPivotExponent G c) W Y m n *
         ⌈Real.exp (movingProductExponent (movingCellPivotExponent G c) W n -
   …

   Mentions: OAI.Ostmann.movingCellPivotExponent, OAI.Ostmann.movingProductExponent, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.movingProductNaturalCutoff