OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeNodeSubstitution.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPrimeNodeFactor_valid line 13

   Source documentation

   Every nonzero original node factor comes from the unique positive integer substitution in its cutoff range.

   theorem movingPrimeNodeFactor_valid {σ : Type*}
       (value : σ → ℕ) (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ) (CL CR u : List σ)
       (XL XR : ℕ) (s v w : ℤ) (I : Finset ℕ)
       (hI : ∀ p : ℕ, 0 < p → φ (Real.log p - G (n + 1)) ≠ 0 → p ∈ I)
       (hf : movingPrimeNodeFactor value outside childBound pivotBound φ G n CL CR u XL XR s v w ≠ 0) :
       validTransferredPivot I
         (v * (XR * MovingSlotReversal.naturalProduct value CR : ℕ) -
           w * (XL * MovingSlotReversal.naturalProduct value CL : ℕ))
         (s * MovingSlotReversal.naturalProduct value u) := by
   …

   Mentions: OAI.Ostmann.movingPrimeNodeFactor, OAI.Ostmann.validTransferredPivot, OAI.Ostmann.MovingSlotReversal.naturalProduct

2. theorem OAI.Ostmann.movingPrimeNodeFactor_valid_cell line 45

   Source documentation

   For the concrete giant cell, the original node's support gives exactly its integer pivot range; endpoint primes and integers are retained.

   theorem movingPrimeNodeFactor_valid_cell {σ : Type*}
       (value : σ → ℕ) (outside : List ℕ) (childBound pivotBound : ℕ → ℕ)
       (φ : ℝ → ℝ) (hout : ∀ x, 1 ≤ |x| → φ x = 0) (G : ℕ → ℝ)
       (n : ℕ) (CL CR u : List σ) (XL XR : ℕ) (s v w : ℤ)
       (hf : movingPrimeNodeFactor value outside childBound pivotBound φ G n CL CR u XL XR s v w ≠ 0) :
       validTransferredPivot
         (Finset.Ioc ⌊Real.exp (G (n + 1) - 1)⌋₊ ⌊Real.exp (G (n + 1) + 1)⌋₊)
         (v * (XR * MovingSlotReversal.naturalProduct value CR : ℕ) -
           w * (XL * MovingSlotReversal.naturalProduct value CL : ℕ))
         (s * MovingSlotReversal.naturalProduct value u) :=
   …

   Mentions: OAI.Ostmann.movingPrimeNodeFactor, OAI.Ostmann.validTransferredPivot, OAI.Ostmann.MovingSlotReversal.naturalProduct

3. theorem OAI.Ostmann.movingPrimeNodeFactor_substitution line 60

   Source documentation

   The new coefficient term is exactly the off-diagonal integer-substitution term from the full transform transfer, with its original two child factors.

   theorem movingPrimeNodeFactor_substitution {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n : ℕ)
       (u : TreeLeafTuple (List σ) n) (small bulk : TreeLeafTuple (List σ) (n + 1))
       (XL XR : ℕ) (s v w : ℤ) (I : Finset ℕ)
       (hI : ∀ p ∈ I, 0 < p)
       (hφ : ∀ p : ℕ, 0 < p → φ (Real.log p - G (n + 1)) ≠ 0 → p ∈ I)
       (hsV : s.natAbs ≤ V (n + 1))
       (hv : v.natAbs ≤ childBound (n + 1)) (hw : w.natAbs ≤ childBound (n + 1)) :
       let U := MovingSlotReversal.naturalProduct value (flattenMovingSlots n u)
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSlotReversal.naturalProduct, OAI.Ostmann.flattenMovingSlots