OAI/NumberTheory/EgyptianFractions/UniformSecondMoment.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.norm_expect_sq_eq_expect_pairs line 9
2. theorem OAI.Problem337.uniform_second_moment_identity line 15
3. theorem OAI.Problem337.uniform_boolean_second_moment_bound line 26

   Source documentation

   Uniform finite-average version of the Hamming second-moment reduction.

   theorem uniform_boolean_second_moment_bound {Ω : Type*} [Fintype Ω] [Nonempty Ω]
       (m : ℕ) (z : Ω → (Fin m → Bool) → ℂ)
       (hz : ∀ ω i, ‖z ω i‖ ≤ 1) (δ : ℝ) (hδ : 0 ≤ δ)
       (hgood : ∀ i j, (m : ℝ) / 4 ≤ (hammingDist i j : ℝ) →
         ‖𝔼 ω, z ω i * star (z ω j)‖ ≤ δ) :
       (𝔼 ω, ‖𝔼 i, z ω i‖ ^ 2) ≤ Real.exp (-(m : ℝ) / 16) + δ := by
   …

4. theorem OAI.Problem337.uniform_boolean_random_second_moment_bound line 74

   Source documentation

   Uniform-mean final random estimate, directly matching the second moment of the sampled Boolean-product exponential average.

   theorem uniform_boolean_random_second_moment_bound {Ω : Type*}
       [Fintype Ω] [Nonempty Ω] (m : ℕ) (V : ℝ)
       (z : Ω → (Fin m → Bool) → ℂ) (hz : ∀ ω i, ‖z ω i‖ ≤ 1)
       (hlarge : 50 ≤ min (m : ℝ) V)
       (hgood : ∀ i j, (m : ℝ) / 4 ≤ (hammingDist i j : ℝ) →
         ‖𝔼 ω, z ω i * star (z ω j)‖ ≤ Real.exp (-V / 20) + Real.exp (-V / 5)) :
       (𝔼 ω, ‖𝔼 i, z ω i‖ ^ 2) ≤ Real.exp (-min (m : ℝ) V / 100) := by
   …