OAI/NumberTheory/Ostmann/Arithmetic/MovingTemplateAmplitude.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingTemplatePrimeAmplitude line 13

   Source documentation

   The finite prime amplitude, with both giants and every regular slot sampled from their original laws. The root frequency is not renormalized.

   noncomputable def movingTemplatePrimeAmplitude {σ : 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) : ℂ :=
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot

2. theorem OAI.Ostmann.movingTemplatePrimeAmplitude_next line 31

   Source documentation

   The next amplitude is exactly the extended integer off-diagonal, including its original compensation factors and the two inherited regular laws. No prime is reweighted or resampled by this identity.

   theorem movingTemplatePrimeAmplitude_next {σ : Type} [Fintype σ]
       (value : σ → ℕ) (hvalue : ∀ a, (value a).Prime) (outside : List ℕ)
       (μ : ℕ → σ → ℝ) (childBound pivotBound V : ℕ → ℕ) (hV : Monotone V)
       (F : MovingSlotState σ → ℤ → ℂ) (hF : ∀ x, F x 0 = 0)
       (φ : ℝ → ℝ) (G : ℕ → ℝ) (n r m : ℕ)
       (Pg : Finset ℕ) (hPg : ∀ q ∈ Pg, q.Prime) (ρ : Pg → ℝ)
       (ν : MovingRegularSlot (n + 1) r m → σ → ℝ)
       (hlarge : ∀ q : Pg, V (n + 1) < (q : ℕ))
       (I : Finset ℕ) (hI : ∀ p ∈ I, 0 < p)
       (hφ : ∀ p : ℕ, 0 < p → φ (Real.log p - G (n + 1)) ≠ 0 → p ∈ I)
       (hchild : V n ≤ childBound (n + 1))
       (hgap : ∀ XR : Pg, ∀ right, movingTemplateSidePrior n r m ν false right ≠ 0 →
   …

   Mentions: OAI.Ostmann.MovingSlotState, OAI.Ostmann.MovingRegularSlot, OAI.Ostmann.movingTemplateSidePrior