OAI/NumberTheory/Ostmann/Arithmetic/MovingPrimeSquareBudget.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingOriginalPrimePairMean line 13

   Source documentation

   The original external average of two sampled histories. The external weights may in particular be the unchanged product of harmonic prime priors.

   noncomputable def movingOriginalPrimePairMean {σ I Ω : Type}
       [Fintype σ] [Fintype Ω] (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ)
       (childBound pivotBound : ℕ → ℕ)
       (F : {n : ℕ} → MovingSlotData σ n → ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n : ℕ) (ν : Ω → ℝ) (small bulk : Ω → TreeLeafTuple (List σ) n)
       (u v r w : ℝ) (l h : FrequencyTree ℤ n) : ℂ :=
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.FrequencyTree

2. theorem OAI.Ostmann.movingFrequencyCoefficient_original_mean_square line 39
3. theorem OAI.Ostmann.movingFrequencyCoefficient_original_arithmetic_budget line 61

   Source documentation

   This uses the actual two-history mean and the exact coefficient-square identity. Only the negligible error receives the full history count.

   theorem movingFrequencyCoefficient_original_arithmetic_budget
       (hV : Monotone V) (hF : ∀ d (T : MovingSlotData σ d), F T 0 = 0)
       (D K err : ℝ) (hD : 0 ≤ D) (hK : 0 ≤ K)
       (hdiv : ∀ a : ℕ, a ≠ 0 → a ≤ V n ^ 2 → (a.divisors.card : ℝ) ≤ D) :
       let M := movingOriginalPrimePairMean q value outside μ childBound pivotBound F g Dq S
   …

   Mentions: OAI.Ostmann.MovingSlotData, OAI.Ostmann.movingOriginalPrimePairMean