OAI/NumberTheory/Ostmann/Arithmetic/MovingAmplitudeIndex.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.MovingAmplitudeIndex line 11
2. def OAI.Ostmann.movingAmplitudePrior line 14
3. theorem OAI.Ostmann.movingTemplatePrimeAmplitude_index line 21

   Source documentation

   The frequency is part of the transfer index and has counting measure. Only the giant and regular prime coordinates carry probability weights.

   theorem movingTemplatePrimeAmplitude_index {σ : Type} [Fintype σ]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState σ → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ)
       (Pg : Finset ℕ) (ρ : Pg → ℝ) (ν : MovingRegularSlot n r m → σ → ℝ)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool) :
       movingTemplatePrimeAmplitude value outside μ childBound pivotBound V F φ G n (4 + r) m
         Pg ρ (movingTemplateRestoredPrior n r m (μ n) ν) greg ggiant favorable =
       ∑ u : TreeLeafIndex n × Fin 4 → σ, ((∏ i, μ n (u i) : ℝ) : ℂ) *
         ∑ p : Pg, (ρ p : ℂ) * ∑ a : MovingAmplitudeIndex σ Pg n r m V,
           movingTemplateTransferWeight value outside μ childBound pivotBound V F φ G n r m
             (fun a => a.2.2.val) (fun a => (movingAmplitudePrior Pg n r m V ρ ν a : ℂ))
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplatePrimeAmplitude, OAI.Ostmann.movingTemplateRestoredPrior, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.MovingAmplitudeIndex, OAI.Ostmann.movingTemplateTransferWeight, OAI.Ostmann.movingAmplitudePrior