OAI/NumberTheory/Ostmann/Construction/HalfPrimeStatistic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.physicalTupleTerm_summable line 12
2. def OAI.Ostmann.halfPrimeMean line 27
3. def OAI.Ostmann.doubledHalfWeight line 33
4. theorem OAI.Ostmann.halfPrimeMean_square line 39

   Source documentation

   All positions, including the two giants and the outside spectators, are sampled twice independently in the initial square.

   theorem halfPrimeMean_square {n : ℕ} (P : Finset ℕ) (μ : Fin n → P → ℝ)
       (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
       (w : (Fin n → P) → ℂ) (a : ℤ) :
       halfPrimeMean P μ F w a ^ 2 =
         ∑ x : Fin (n + n) → P, (productPrior (Fin.append μ μ) x : ℂ) * doubledHalfWeight w x *
           ∏ i, Fin.append F F i (x i) (a : ZMod (x i : ℕ)) := by
   …

   Mentions: OAI.Ostmann.halfPrimeMean, OAI.Ostmann.productPrior, OAI.Ostmann.doubledHalfWeight

5. theorem OAI.Ostmann.halfPrimeMean_statistic line 76

   Source documentation

   Exchanging only finite original sample sums with the Schwartz sum gives the exact physical statistic used by the initial Fourier lower bound.

   theorem halfPrimeMean_statistic {n : ℕ}
       (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (μ : Fin n → P → ℝ)
       (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
       (w : (Fin n → P) → ℂ) (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X) :
       (∑' a : ℤ, halfPrimeMean P μ F w a ^ 2 * ψ ((a : ℝ) / X)) =
         ∑ x : Fin (n + n) → P, (productPrior (Fin.append μ μ) x : ℂ) * doubledHalfWeight w x *
           physicalTupleSum P x (Fin.append F F) ψ X := by
   …

   Mentions: OAI.Ostmann.halfPrimeMean, OAI.Ostmann.productPrior, OAI.Ostmann.doubledHalfWeight, OAI.Ostmann.physicalTupleSum

6. def OAI.Ostmann.halfPrimeBound line 98
7. theorem OAI.Ostmann.halfPrimeMean_bound line 103
8. theorem OAI.Ostmann.halfPrimeMean_real line 116
9. theorem OAI.Ostmann.halfPrimeMean_statistic_re line 132
10. theorem OAI.Ostmann.halfPrimeMean_endpoint_lower line 167

    Source documentation

    The selected mean over endpoints gives a lower bound for the full original doubled-list physical statistic.

    theorem halfPrimeMean_endpoint_lower {n : ℕ}
        (P : Finset ℕ) [∀ q : P, NeZero (q : ℕ)] (μ : Fin n → P → ℝ)
        (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
        (w : (Fin n → P) → ℂ) (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X)
        (hreal : ∀ a, (halfPrimeMean P μ F w a).im = 0)
        (E : Finset ℤ) (c δ : ℝ) (hc : 0 ≤ c) (hδ : 0 ≤ δ)
        (hψ : ∀ x, 0 ≤ (ψ x).re) (hcE : ∀ a ∈ E, c ≤ (ψ ((a : ℝ) / X)).re)
        (hmean : (E.card : ℝ) * δ ≤ ∑ a ∈ E, (halfPrimeMean P μ F w a).re) :
        (E.card : ℝ) * (c * δ ^ 2) ≤
          ‖∑ x : Fin (n + n) → P, (productPrior (Fin.append μ μ) x : ℂ) * doubledHalfWeight w x *
            physicalTupleSum P x (Fin.append F F) ψ X‖ := by
    …

    Mentions: OAI.Ostmann.halfPrimeMean, OAI.Ostmann.productPrior, OAI.Ostmann.doubledHalfWeight, OAI.Ostmann.physicalTupleSum