OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplatePrimeStatistic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTemplatePrimeStatistic line 11
2. theorem OAI.Ostmann.movingTemplatePrimeStatistic_energy_integrand line 29

   Source documentation

   The exterior factor agrees with the literal template multiplier wherever its bulk-symmetrized coefficient is nonzero.

   theorem movingTemplatePrimeStatistic_energy_integrand
       (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (outside : List ℕ) (μ : ℕ → P → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (F : MovingSlotState P → ℤ → ℂ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ)
       (greg : ∀ q : ℕ, ZMod q → ℂ) (H : ℝ) (s : ℤ)
       (y : MovingRegularSlot n r m → P) (x z : ℝ) :
       (‖movingBulkAveragedTemplateCoefficient Subtype.val outside μ childBound pivotBound V F φ G
         n r m s y ⌊Real.exp x⌋₊ ⌊Real.exp z⌋₊‖ ^ 2 : ℂ) *
         ((giantOuterWeight φ H H false ⌊Real.exp x⌋₊ ⌊Real.exp z⌋₊) *
           (‖movingExternalRegularFactor Subtype.val outside (movingTemplateSmall n r m)
             (bulkSlotLeaves n m (movingTemplateBulk n r m)) greg s y x z‖ ^ 2 : ℝ)) =
       (‖movingBulkAveragedTemplateCoefficient Subtype.val outside μ childBound pivotBound V F φ G
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingBulkAveragedTemplateCoefficient, OAI.Ostmann.giantOuterWeight, OAI.Ostmann.movingExternalRegularFactor, OAI.Ostmann.movingTemplateSmall, OAI.Ostmann.bulkSlotLeaves, OAI.Ostmann.movingTemplateBulk

3. theorem OAI.Ostmann.movingTemplatePrimeStatistic_cauchy line 63