OAI/NumberTheory/EgyptianFractions/FourierCommonRealization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.FourierCommonRealization.exists_common_fourier_realization line 12

   Source documentation

   The random-product second moment hypotheses imply one common collection of 1000 sample blocks, simultaneously good at all middle and terminal scales. This is stated directly in normalized Fourier averages.

   theorem exists_common_fourier_realization :
       ∃ N : ℕ, ∀ (Ω J : Type) [Fintype Ω] [Nonempty Ω]
         (tests : Finset J) (level : J → Finset ℕ) (X : J → ℝ) (m : ℝ)
         (freq : Finset ℕ) (terminalFreq : ℕ → Finset ℕ)
         (phase : Ω → ℕ → ℕ → ℂ) (w : ℕ → ℝ) (terminal : Finset ℕ),
         500000 ≤ m → (tests.card : ℝ) ≤ m →
         (∀ j ∈ tests, 0 < X j) →
         (∀ j ∈ tests, ((level j).card : ℝ) ≤ X j) →
         ((freq.card : ℝ) ≤ Real.exp (4 * m / 10000)) →
         (∀ j ∈ tests, ∀ u ∈ level j, (9999 / 10000 : ℝ) * m ≤ w u) →
         (∀ j ∈ tests, ∀ u ∈ level j, ∀ l ∈ freq,
           (∑ ω, ‖phase ω u l‖ ^ 2) / Fintype.card Ω ≤ Real.exp (-w u / 100)) →
   …