OAI/Probability/ThorpShuffle/FirstFourier.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Thorp.Current.low_degree_first line 17

   Source documentation

   The first inverse-degree moment yields a D^(3/8) orbit bound. The filter is precisely degree ≤ D^(1/8), written without a root.

   lemma low_degree_first {H : Type} [Group H] [Fintype H]
       (F : Fourier.Family H) (D : ℕ) :
       (∑ b ∈ Finset.univ.filter (fun b => F.degree b ^ 8 ≤ D), (F.degree b : ℝ)^2) ≤
         (D : ℝ) ^ (3 / 8 : ℝ) * ∑ b, (F.degree b : ℝ)⁻¹ := by
   …

   Mentions: OAI.Thorp.Fourier.Family

2. lemma OAI.Thorp.Current.eight_block_of_cap line 45

   Source documentation

   The integrated operator norm bound for an eight-fold block action with a common probability mass function satisfying all eight coset caps.

   lemma eight_block_of_cap {G : Type} [Group G] [Fintype G]
       (s : ℕ) (hs : 1 ≤ s)
       {E : Type uE} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
       [FiniteDimensional ℂ E]
       (ρ : Representation ℂ G E) [Representation.IsIrreducible ρ]
       (hu : ∀ g x y, ⟪ρ g x, ρ g y⟫_ℂ = ⟪x, y⟫_ℂ)
       (ψ : (Fin 8 → Equiv.Perm (Fin s)) →* G)
       (ν : G → ℝ) (hν : ∀ g, 0 ≤ ν g) (h1 : ∑ g, ν g = 1)
       (hcoset : ∀ (i : Fin 8) g,
         ∑ h : Equiv.Perm (Fin s), ν (g * ψ (Pi.mulSingle i h)) ≤
           4 * (Fintype.card (Equiv.Perm (Fin s)) : ℝ) / Fintype.card G) :
       ‖LinearMap.toContinuousLinearMap (integrated ρ (fun g => (ν g : ℂ)))‖ ≤
   …

3. theorem OAI.Thorp.Current.eight_block_fourier_bound line 97

   Source documentation

   The integrated operator norm bound for permutations of binary positions under any equivalence with eight equal blocks.

   theorem eight_block_fourier_bound
       (d : ℕ) (_hd : 3 ≤ d)
       (e : Position d ≃ Fin 8 × Fin (2 ^ (d - 3)))
       {E : Type uE} [NormedAddCommGroup E] [InnerProductSpace ℂ E]
       [FiniteDimensional ℂ E]
       (ρ : Representation ℂ (Equiv.Perm (Position d)) E)
       [Representation.IsIrreducible ρ]
       (hu : ∀ g x y, ⟪ρ g x, ρ g y⟫_ℂ = ⟪x, y⟫_ℂ)
       (ν : Equiv.Perm (Position d) → ℝ)
       (hν : ∀ g, 0 ≤ ν g) (h1 : ∑ g, ν g = 1)
       (hcoset : ∀ (i : Fin 8) (g : Equiv.Perm (Position d)),
         ∑ h : Equiv.Perm (Fin (2 ^ (d - 3))),
   …

   Mentions: OAI.Thorp.Position