OAI/NumberTheory/Ostmann/Arithmetic/MovingNodeCutoffFactor.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingNaturalNodeCutoff line 11
2. theorem OAI.Ostmann.movingNaturalNodeCutoff_star line 19
3. def OAI.Ostmann.movingPhiExtra line 29
4. theorem OAI.Ostmann.movingSlotWeight_node_cutoff line 37

   Source documentation

   The smooth cutoff is factored out of the original recursion, even when an arithmetic guard vanishes. All other node factors remain in extra.

   theorem movingSlotWeight_node_cutoff {σ : Type*} (value : σ → ℕ)
       (childBound pivotBound : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (extra : MovingSlotState σ → ℤ → ℤ → ℤ → ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       {n : ℕ} (T : MovingSlotData σ n) (t : FrequencyTree ℤ n) (hT : T.Follows t) (L R : ℕ) :
       recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
         (movingSlotCutoff value childBound pivotBound (movingPhiExtra value childBound pivotBound extra φ G))
           n ⟨n, T, L, R⟩ t =
         recursiveTransferWeight (movingSlotSystem value childBound pivotBound) F
           (movingSlotCutoff value childBound pivotBound extra) n ⟨n, T, L, R⟩ t *
             movingNaturalNodeCutoff value φ G T L R := by
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingSlotData, OAI.Ostmann.FrequencyTree, OAI.Ostmann.recursiveTransferWeight, OAI.Ostmann.movingSlotSystem, OAI.Ostmann.movingSlotCutoff, OAI.Ostmann.movingPhiExtra, OAI.Ostmann.movingNaturalNodeCutoff

5. theorem OAI.Ostmann.movingNaturalNodeCutoff_eq_real line 83