ExposedCorrelation.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.Problem337.norm_character_average_sub line 12

Source documentation

A constant phase has no effect on the norm of a normalized additive-character average. The averaging set is an arbitrary finite type.

lemma norm_character_average_sub {ι : Type*} [Fintype ι]
    {u : ℕ} [NeZero u] (f : ι → ZMod u) (t : ZMod u) (D : ℂ) :
    ‖(∑ i : ι, ZMod.stdAddChar (f i - t)) / D‖ =
      ‖(∑ i : ι, ZMod.stdAddChar (f i)) / D‖ := by
…

Mentions: OAI.Problem337.D

theorem OAI.Problem337.exposed_prime_correlation_bound line 22

Source documentation

The correlation bound after exposing all but two independent prime products. The effective modulus is u / gcd(a,u), and no coprimality of a and u is assumed.

theorem exposed_prime_correlation_bound
    (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (hne : P.Nonempty)
    (s a u : ℕ) (hu : 0 < u) [NeZero u] [NeZero (u / a.gcd u)]
    (hsmall : ∀ w : Fin s → ↥P, (∏ i, (w i : ℕ)) < u / a.gcd u)
    (t : ZMod u) :
    ‖(∑ w₁ : Fin s → ↥P, ∑ w₂ : Fin s → ↥P,
      ZMod.stdAddChar
        (((a * (∏ i, (w₁ i : ℕ)) * (∏ i, (w₂ i : ℕ)) : ℕ) : ZMod u) - t)) /
        ((P.card : ℂ)^s)^2‖ ≤
      Real.sqrt ((u / a.gcd u : ℕ) : ℝ) *
        ((s.factorial : ℝ) / (P.card : ℝ)^s) := by
…

lemma OAI.Problem337.sqrt_mul_atom_le_exp line 58
Source documentation
Numerically, the square-root loss in the modulus changes an atom bound exp(-7 V / 10) into the correlation bound exp(-V / 5).
```
lemma sqrt_mul_atom_le_exp {q A V : ℝ}
    (hq : q ≤ Real.exp V) (hA : A ≤ Real.exp (-7 * V / 10)) (hA0 : 0 ≤ A) :
    Real.sqrt q * A ≤ Real.exp (-V / 5) := by
…
```

theorem OAI.Problem337.exposed_prime_correlation_le_exp line 81

Source documentation

The good-exposure estimate in the random-product argument. The product size and atom decay hypotheses are separated from the algebraic cancellation.

theorem exposed_prime_correlation_le_exp
    (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (hne : P.Nonempty)
    (s a u : ℕ) (hu : 0 < u) [NeZero u] [NeZero (u / a.gcd u)]
    (hsmall : ∀ w : Fin s → ↥P, (∏ i, (w i : ℕ)) < u / a.gcd u)
    (t : ZMod u) (V : ℝ) (huV : (u : ℝ) ≤ Real.exp V)
    (hatom : (s.factorial : ℝ) / (P.card : ℝ)^s ≤ Real.exp (-7 * V / 10)) :
    ‖(∑ w₁ : Fin s → ↥P, ∑ w₂ : Fin s → ↥P,
      ZMod.stdAddChar
        (((a * (∏ i, (w₁ i : ℕ)) * (∏ i, (w₂ i : ℕ)) : ℕ) : ZMod u) - t)) /
        ((P.card : ℂ)^s)^2‖ ≤ Real.exp (-V / 5) := by
…