OAI/NumberTheory/Ostmann/Arithmetic/MovingNormalizedStatistic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.movingPrimeCore line 11
2. theorem OAI.Ostmann.movingPrimeCore_interval_eq line 29

   Source documentation

   At prime points, the logarithmic coordinates and the positive-log cutoffs agree with the original statistic on every rectangle.

   theorem movingPrimeCore_interval_eq {σ I B : Type}
       [Fintype σ] [Fintype B] (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ) (ν : B → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (f : ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n m : ℕ) (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool)
       (gLeft gRight u v r w : ℝ) :
       primeExternalAverage ν (V n) u v r w (fun s y x z =>
         (φ (x - gLeft) : ℂ) * (φ (z - gRight) : ℂ) *
           movingPrimeCore q value outside μ childBound pivotBound V f g Dq S ψ X lo hi φ G
   …

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.primeExternalAverage, OAI.Ostmann.movingPrimeCore

3. theorem OAI.Ostmann.movingPrimeCore_normalized_eq line 57

   Source documentation

   Exact identification of the two normalized giant priors with the full-cell moving statistic. All normalizers and both phases remain present.

   theorem movingPrimeCore_normalized_eq {σ I B : Type}
       [Fintype σ] [Fintype B] (q : I → ℕ) [∀ i, Fact (q i).Prime]
       (value : σ → ℕ) (outside : List ℕ) (μ : ℕ → σ → ℝ) (ν : B → σ → ℝ)
       (childBound pivotBound V : ℕ → ℕ) (f : ℤ → ℂ)
       (g : ∀ i, ZMod (q i) → ℂ) (Dq : ∀ i, (ZMod (q i))ˣ) (S : Finset I)
       (ψ : 𝓢(ℝ, ℂ)) (X lo hi : ℝ) (φ : ℝ → ℝ) (G : ℕ → ℝ)
       (n m : ℕ) (small : TreeLeafTuple (List B) n) (slot : (TreeLeafIndex n × Fin m) ↪ B)
       (greg ggiant : ∀ q : ℕ, ZMod q → ℂ) (favorable : ℕ → Bool)
       (gLeft gRight : ℝ) (hout : ∀ x, 1 ≤ |x| → φ x = 0) :
       smoothGiantExternalAverage ν (V n) φ gLeft gRight (fun s y p r =>
         movingPrimeCore q value outside μ childBound pivotBound V f g Dq S ψ X lo hi φ G
           n m small slot greg ggiant favorable s y (Real.log p) (Real.log r)) =
   …

   Mentions: OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.smoothGiantExternalAverage, OAI.Ostmann.movingPrimeCore