OAI/NumberTheory/Ostmann/Arithmetic/MovingArithmeticCells.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.rootCellCode_eq_of_subset line 11
2. def OAI.Ostmann.movingArithmeticCellValue line 18

   Source documentation

   A cell is accepted precisely when it contains an original supported integer in the prescribed progression. Invariance supplies the converse.

   noncomputable def movingArithmeticCellValue {σ : Type*} (value : σ → ℕ)
       (_hvalue : ∀ i, value i ≠ 0) (childBound pivotBound : ℕ → ℕ) {n : ℕ}
       (T : MovingSlotData σ n) (_hf : T.Frequencies (· ≠ 0)) (XR a M : ℕ)
       (S : Finset ℝ) (code : S → Ordering) : ℂ :=
   …

   Mentions: OAI.Ostmann.MovingSlotData

3. theorem OAI.Ostmann.movingArithmeticCellValue_norm line 27
4. theorem OAI.Ostmann.movingArithmeticIndicator_eq_cell line 37

   Source documentation

   Adding derivative roots to the arithmetic cuts does not change the exact support multiplier on any integer in the progression.

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

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

5. theorem OAI.Ostmann.complexPrimeInterval_congr line 57
6. theorem OAI.Ostmann.movingArithmeticPrimeInterval_cells line 70

   Source documentation

   The exact original arithmetic indicator becomes the constructed root-cell multiplier under the actual prime sum, with every boundary prime included.

   theorem movingArithmeticPrimeInterval_cells {σ : 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)
       (u v : ℝ) (w : ℝ → ℂ) :
       complexPrimeInterval M a u v
         (fun y => movingArithmeticIndicator value childBound pivotBound T ⌊Real.exp y⌋₊ XR * w y) =
       complexPrimeInterval M a u v
         (fun y => movingArithmeticCellValue value hvalue childBound pivotBound T hf XR a M S
           (rootCellCode S (Real.exp y)) * w y) := by
   …

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