OAI/NumberTheory/Ostmann/Arithmetic/MovingSupportedCells.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingSupportedCellValue line 11
2. theorem OAI.Ostmann.movingSupportedCellValue_norm line 18
3. theorem OAI.Ostmann.movingSupportedCellValue_eq line 31

   Source documentation

   The cell representative is used only on the proved original support. Its value is independent of the representative by the supplied local identity.

   theorem movingSupportedCellValue_eq {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XR a M : ℕ)
       (S : Finset ℝ) (hM : movingTopPeriod value hvalue childBound pivotBound T hf ∣ M)
       (hS : movingTopRootCuts value hvalue childBound pivotBound T hf XR ⊆ S)
       (w : ℕ → ℂ)
       (hw : ∀ XL YL, T.ArithmeticSupport value childBound pivotBound XL XR →
         T.ArithmeticSupport value childBound pivotBound YL XR →
         (XL : ℤ) ≡ (YL : ℤ) [ZMOD M] →
         rootCellCode S (XL : ℝ) = rootCellCode S (YL : ℝ) → w XL = w YL)
       (XL : ℕ) (hres : (XL : ℤ) ≡ (a : ℤ) [ZMOD M]) :
       movingArithmeticIndicator value childBound pivotBound T XL XR * w XL =
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingTopPeriod, OAI.Ostmann.movingTopRootCuts, OAI.Ostmann.rootCellCode, OAI.Ostmann.movingArithmeticIndicator

4. theorem OAI.Ostmann.movingSupportedPrimeInterval_cells line 63
5. theorem OAI.Ostmann.PublishedProgressionInput.moving_supported_prime_comparison line 89

   Source documentation

   The original gate times a residue weight is compared without deleting boundary primes or changing the retained Page density.

   theorem PublishedProgressionInput.moving_supported_prime_comparison
       (P : PublishedProgressionInput) {σ : Type*} (value : σ → ℕ)
       (hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (hf : T.Frequencies (· ≠ 0)) (XR a M Q : ℕ)
       (hM : movingTopPeriod value hvalue childBound pivotBound T hf ∣ M)
       (hQ : 2 ≤ Q) (hq : 1 ≤ M) (hqQ : M ≤ Q) (ha : a.Coprime M)
       (u v : ℝ) (hu : 1 ≤ u) (huv : u ≤ v) (hshort : v ≤ u + 1)
       {k : ℕ} (F : Fin k → ClippedPolynomialFactor) (S : Finset ℝ)
       (hS : movingTopRootCuts value hvalue childBound pivotBound T hf XR ⊆ S)
       (hroots : ∀ i r, r ∈ (F i).polynomial.derivative.roots → r ∈ S)
       (w : ℕ → ℂ) (B : ℝ) (hB : 0 ≤ B)
       (hwB : ∀ XL, T.ArithmeticSupport value childBound pivotBound XL XR → ‖w XL‖ ≤ B)
   …

   Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingTopPeriod, OAI.Ostmann.ClippedPolynomialFactor, OAI.Ostmann.movingTopRootCuts