OAI/NumberTheory/EgyptianFractions/FourierFailureBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.FourierFailureBounds.failure_fraction_le_exp line 11

   Source documentation

   Frequency union and second-moment Markov bound with the exact scales used in the random-product construction.

   theorem failure_fraction_le_exp {Ω L : Type*} [Fintype Ω] [Nonempty Ω]
       [DecidableEq Ω] (freq : Finset L) (phase : Ω → L → ℂ) (m w : ℝ)
       (hfreq : (freq.card : ℝ) ≤ Real.exp (4 * m / 10000))
       (hmoment : ∀ l ∈ freq, (∑ ω, ‖phase ω l‖ ^ 2) ≤
         (Fintype.card Ω : ℝ) * Real.exp (-w / 100)) :
       ((Finset.univ.filter (fun ω => ∃ l ∈ freq,
         Real.exp (-3 * m / 10000) < ‖phase ω l‖)).card : ℝ) /
         Fintype.card Ω ≤ Real.exp (m / 1000 - w / 100) := by
   …

2. theorem OAI.Problem337.FourierFailureBounds.middle_failure_fraction_le line 48

   Source documentation

   Throughout a middle level, the logarithmic range is at least (1-10⁻⁴)m, giving the uniform single-block failure budget exp(-m/200).

   theorem middle_failure_fraction_le {Ω L : Type*} [Fintype Ω] [Nonempty Ω]
       [DecidableEq Ω] (freq : Finset L) (phase : Ω → L → ℂ) (m w : ℝ)
       (hm : 0 ≤ m) (hw : (9999 / 10000 : ℝ) * m ≤ w)
       (hfreq : (freq.card : ℝ) ≤ Real.exp (4 * m / 10000))
       (hmoment : ∀ l ∈ freq, (∑ ω, ‖phase ω l‖ ^ 2) ≤
         (Fintype.card Ω : ℝ) * Real.exp (-w / 100)) :
       ((Finset.univ.filter (fun ω => ∃ l ∈ freq,
         Real.exp (-3 * m / 10000) < ‖phase ω l‖)).card : ℝ) /
         Fintype.card Ω ≤ Real.exp (-m / 200) := by
   …

3. theorem OAI.Problem337.FourierFailureBounds.terminal_failure_fraction_le line 63

   Source documentation

   At a terminal integer the same Fourier bound gives the power-law failure probability amplified by the one-thousand-block selection lemma.

   theorem terminal_failure_fraction_le {Ω L : Type*} [Fintype Ω] [Nonempty Ω]
       [DecidableEq Ω] (freq : Finset L) (phase : Ω → L → ℂ) (u : ℝ)
       (hu : 1 ≤ u)
       (hfreq : (freq.card : ℝ) ≤ Real.exp (4 * Real.log u / 10000))
       (hmoment : ∀ l ∈ freq, (∑ ω, ‖phase ω l‖ ^ 2) ≤
         (Fintype.card Ω : ℝ) * Real.exp (-Real.log u / 100)) :
       ((Finset.univ.filter (fun ω => ∃ l ∈ freq,
         Real.exp (-3 * Real.log u / 10000) < ‖phase ω l‖)).card : ℝ) /
         Fintype.card Ω ≤ u ^ (-(1 / 200 : ℝ)) := by
   …