OAI/NumberTheory/Ostmann/Construction/HalfPrimeInitialAmplitude.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.primeHalfTests line 10
2. theorem OAI.Ostmann.primeHalfTests_sum line 16
3. theorem OAI.Ostmann.primeHalfTests_energy line 23
4. theorem OAI.Ostmann.primeHalfTests_statistic_lower line 33

   Source documentation

   This is (7.5) before the asymptotic constants are absorbed: the only mean premise is the selected actual giant mean, and the nongiant factors are the manuscript's exact normalized residue indicators.

   theorem primeHalfTests_statistic_lower {n : ℕ}
       (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime)
       (S : (q : P) → Finset (ZMod (q : ℕ))) (favorable : P → Bool)
       (μ₀ : P → ℝ) (μ : Fin n → P → ℝ) (w : (Fin n → P) → ℝ)
       (hμ : ∀ i q, 0 ≤ μ i q) (hw : ∀ x, 0 ≤ w x)
       (E : Finset ℤ) (B : Finset (Fin n → P)) (β δ c : ℝ)
       (hβ : 0 ≤ β) (hδ : 0 ≤ δ) (hc : 0 ≤ c)
       (hmass : β ≤ ∑ x ∈ B, productPrior μ x * w x)
       (hbalance : ∀ x ∈ B, ∀ i, (1 / 3 : ℝ) ≤ residueDensity (S (x i)) ∧
         residueDensity (S (x i)) ≤ 2 / 3)
       (hendpoint : ∀ a ∈ E, ∀ q : P, (a : ZMod (q : ℕ)) ∈ S q)
       (hmean : (E.card : ℝ) * δ ≤ ∑ a ∈ E,
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.residueDensity

5. theorem OAI.Ostmann.primeHalfTests_initialAmplitude_lower line 71

   Source documentation

   The endpoint construction gives the Fourier lower bound. The error allowance is the proved repeated-prime bound under the original mixed marginals.

   theorem primeHalfTests_initialAmplitude_lower {n : ℕ}
       (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (hP : ∀ q ∈ P, q.Prime)
       (S : (q : P) → Finset (ZMod (q : ℕ))) (favorable : P → Bool)
       (ν : Fin (n + 1) → P → ℝ) (C : Fin (n + 1) → ℝ)
       (hν : ∀ i q, 0 ≤ ν i q) (hC : ∀ i, 0 ≤ C i)
       (hbound : ∀ i (q : P), (q : ℝ) * ν i q ≤ C i)
       (w : (Fin n → P) → ℝ) (hw : ∀ x, 0 ≤ w x) (hw1 : ∀ x, w x ≤ 1)
       (E : Finset ℤ) (B : Finset (Fin n → P)) (β δ c : ℝ)
       (hβ : 0 ≤ β) (hδ : 0 ≤ δ) (hc : 0 ≤ c)
       (hmass : β ≤ ∑ x ∈ B, productPrior (Fin.tail ν) x * w x)
       (hbalance : ∀ x ∈ B, ∀ i, (1 / 3 : ℝ) ≤ residueDensity (S (x i)) ∧
         residueDensity (S (x i)) ≤ 2 / 3)
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.residueDensity