RandomFourierSelection.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RandomProducts.sampledFourierMean line 13
Source documentation
The actual Boolean product Fourier average, extended by zero at modulus zero only to permit a single function on all natural moduli.
```
def sampledFourierMean {m : ℕ} {P : Finset ℕ}
    (p : (Fin m × Bool) → P) (u l : ℕ) : ℂ :=
…
```
theorem OAI.Problem337.RandomProducts.sampledFourierMean_eq line 19
def OAI.Problem337.RandomProducts.fourierFrequencySet line 25
Source documentation
The positive frequencies required by the discrepancy stage.
```
def fourierFrequencySet (t : ℝ) : Finset ℕ :=
…
```
theorem OAI.Problem337.RandomProducts.mem_fourierFrequencySet line 28
theorem OAI.Problem337.RandomProducts.card_fourierFrequencySet line 35

theorem OAI.Problem337.RandomProducts.sampledFourierMean_second_moment line 43

Source documentation

Normalized finite-sum form of the proved random-product second moment.

theorem sampledFourierMean_second_moment
    (S : ℝ) (hS : 3 ≤ S) (P : Finset ℕ)
    (hprime : ∀ p ∈ P, Nat.Prime p)
    (hinterval : ∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101)
    (hsize : S ^ 99 ≤ (P.card : ℝ)) (u l : ℕ) (hu : 0 < u)
    (hV : 100000 * Real.log S ≤ Real.log (u : ℝ))
    (hVS : Real.log (u : ℝ) ≤ S) (hl : 0 < l)
    (hlbound : (l : ℝ) ≤ Real.exp (min (blockLength S : ℝ) (Real.log (u : ℝ)) / 200)) :
    (∑ p : (Fin (blockLength S) × Bool) → P, ‖sampledFourierMean p u l‖ ^ 2) /
      Fintype.card ((Fin (blockLength S) × Bool) → P) ≤
        Real.exp (-min (blockLength S : ℝ) (Real.log (u : ℝ)) / 100) := by
…

Mentions: OAI.Problem337.RandomProducts.blockLength, OAI.Problem337.RandomProducts.sampledFourierMean

theorem OAI.Problem337.RandomProducts.modulus_pos_of_random_cutoff line 59

theorem OAI.Problem337.RandomProducts.exists_common_sampled_fourier line 70

Source documentation

One common collection of a thousand actual prime-sample blocks. All second-moment and frequency-union premises are discharged; only prime-pool, finite-level size, and the explicit modulus-range hypotheses remain.

theorem exists_common_sampled_fourier :
    ∃ N : ℕ, ∀ (S : ℝ), 3 ≤ S → ∀ (P : Finset ℕ),
      (∀ p ∈ P, Nat.Prime p) →
      (∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101) →
      S ^ 99 ≤ (P.card : ℝ) →
      ∀ (J : Type) (tests : Finset J) (level : J → Finset ℕ) (X : J → ℝ)
        (terminal : Finset ℕ),
      500000 ≤ (blockLength S : ℝ) →
      (tests.card : ℝ) ≤ (blockLength S : ℝ) →
      (∀ j ∈ tests, 0 < X j) →
      (∀ j ∈ tests, ((level j).card : ℝ) ≤ X j) →
      (∀ j ∈ tests, ∀ u ∈ level j,
…

Mentions: OAI.Problem337.RandomProducts.blockLength