OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateAmplitudeRestore.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTemplateRestoredPrior line 10
2. theorem OAI.Ostmann.movingTemplatePrimeAmplitude_restore line 17

   Source documentation

   The original current amplitude is the giant-transfer expression with one shared compensation draw outside its two giant and frequency sums.

   theorem movingTemplatePrimeAmplitude_restore {σ : 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) : ℝ) : ℂ) *
         ∑ XL : Pg, (ρ XL : ℂ) * ∑ XR : Pg, (ρ XR : ℂ) *
           ∑ s : transferFrequencyRange (V n),
             ∑ y : MovingRegularSlot n r m → σ, ((∏ i, ν i (y i) : ℝ) : ℂ) *
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplatePrimeAmplitude, OAI.Ostmann.movingTemplateRestoredPrior, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.transferFrequencyRange