OAI/NumberTheory/Ostmann/Construction/PhaseGiantInitialStatistic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.phasePrimeAverage line 11
2. theorem OAI.Ostmann.phasePrimeAverage_bound line 16
3. theorem OAI.Ostmann.phasePrimeAverage_endpoint_sum line 32
4. theorem OAI.Ostmann.phasePrimeAverage_initial_statistic line 47

   Source documentation

   The independent nongiant factors have the same positive value at every selected endpoint. Their lower bound is represented by κ; the giant factor uses its genuine inverse transform and its genuine finite prime law.

   theorem phasePrimeAverage_initial_statistic {I : Type*} [Fintype I]
       (p : I → ℕ) [∀ i, NeZero (p i)] (ν : I → ℝ)
       (g : ∀ i, ZMod (p i) → ℂ) (hν : ∀ i, 0 ≤ ν i) (hmass : ∑ i, ν i = 1)
       (N : ℕ) (hN : ∀ i, p i ≤ N)
       (ψ : 𝓢(ℝ, ℂ)) (X : ℝ) (hX : 0 < X) (E : Finset ℤ)
       (c κ δ : ℝ) (hc : 0 ≤ c) (hκ : 0 ≤ κ) (hδ : 0 ≤ δ)
       (hψ : ∀ x, 0 ≤ (ψ x).re)
       (hcE : ∀ a ∈ E, c ≤ (ψ ((a : ℝ) / X)).re)
       (hmean : (E.card : ℝ) * δ ≤
         ∑ i, ν i * ∑ a ∈ E, (phaseGiantPhysical (g i) (a : ZMod (p i))).re) :
       (E.card : ℝ) * (c * (κ * δ) ^ 2) ≤
         ∑' a : ℤ, (ψ ((a : ℝ) / X)).re * ‖(κ : ℂ) * phasePrimeAverage p ν g a‖ ^ 2 := by
   …

   Mentions: OAI.Ostmann.phaseGiantPhysical, OAI.Ostmann.phasePrimeAverage