OAI/NumberTheory/Ostmann/Construction/InitialSpectatorProduct.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.initialMovingCutoffWeight_spectator_product line 11
2. theorem OAI.Ostmann.initialMovingOriginalLeaf_spectator_product line 20
3. theorem OAI.Ostmann.initialTemplateAmplitude_spectator_product line 43

   Source documentation

   A nonzero initial statistic certifies the fixed spectator product, with no assumption on an individual sampled summand.

   theorem initialTemplateAmplitude_spectator_product {A I : Type} [Fintype A]
       (value : A → ℕ) (hvalue : ∀ x, 0 < value x)
       (b d r a : ℕ) (cb cd : ℝ) (sl sr : Fin d → A) (fallback : A)
       (q : I → ℕ) [∀ i, Fact (q i).Prime] (g : ∀ i, ZMod (q i) → ℂ)
       (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I) (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ)
       (outside : List ℕ) (μ : ℕ → A → ℝ) (childBound pivotBound V : ℕ → ℕ)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (Pg : Finset ℕ) (ρ : Pg → ℝ)
       (ν : MovingRegularSlot 0 a (b + b) → A → ℝ)
       (greg ggiant : ∀ p : ℕ, ZMod p → ℂ) (fav : ℕ → Bool)
       (h : movingTemplatePrimeAmplitude value outside μ childBound pivotBound V
         (movingOriginalLeaf value q
           (initialMovingDataCutoff value b d r cb cd sl sr fallback) g Dq S ψ X lo hi)
   …

   Mentions: OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplatePrimeAmplitude, OAI.Ostmann.movingOriginalLeaf, OAI.Ostmann.initialMovingDataCutoff