OAI/NumberTheory/Ostmann/Arithmetic/BulkSpectatorNorm.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.bulkBlockProductHom line 11
2. theorem OAI.Ostmann.bulkBlockProductHom_surjective line 17
3. theorem OAI.Ostmann.bulkBlockProduct_average line 27

   Source documentation

   A nonempty set of independent slots gives a uniform product in each leaf. This is the marginal used before exposing any frequency conditions.

   theorem bulkBlockProduct_average {L G : Type*} [Fintype L] [CommGroup G] [Fintype G]
       {m : ℕ} (hm : 0 < m) (F : (L → G) → ℝ) :
       (Fintype.card (L × Fin m → G) : ℝ)⁻¹ * ∑ x : L × Fin m → G, F (bulkBlockProduct x) =
         (Fintype.card (L → G) : ℝ)⁻¹ * ∑ y, F y :=
   …

   Mentions: OAI.Ostmann.bulkBlockProduct

4. theorem OAI.Ostmann.SpectatorDiagram.bulk_l2_bound line 33
5. theorem OAI.Ostmann.spectator_bulk_absolute_le line 52
6. theorem OAI.Ostmann.spectator_bulk_product_absolute_le line 74

   Source documentation

   All spectators retain the paper's 3^(r m) bound under the bulk-slot law, even for an arbitrary matching of the two assignments.

   theorem spectator_bulk_product_absolute_le {I : Type*} [Fintype I]
       (p : I → ℕ) [∀ i, Fact (p i).Prime] (n m : ℕ) (hm : 0 < m)
       (hp : ∀ i, 3 ≤ p i) (g : ∀ i, ZMod (p i) → ℂ) (hg : ∀ i, g i 0 = 0)
       (henergy : ∀ i, ∑ x : ZMod (p i), ‖g i x‖ ^ 2 ≤ (p i : ℝ))
       (d₁ d₂ : ∀ i, SpectatorDiagram (p i) n)
       (e : Equiv.Perm (TreeLeafIndex n × Fin m)) :
       (Fintype.card (∀ i, TreeLeafIndex n × Fin m → (ZMod (p i))ˣ) : ℝ)⁻¹ *
         (∑ x : ∀ i, TreeLeafIndex n × Fin m → (ZMod (p i))ˣ, ∏ i, ‖(d₁ i).bulkValue (g i) (x i) *
           conj ((d₂ i).bulkValue (g i) (x i ∘ e.symm))‖) ≤
         (3 : ℝ) ^ (2 ^ n * Fintype.card I) := by
   …

   Mentions: OAI.Ostmann.SpectatorDiagram, OAI.Ostmann.TreeLeafIndex