OAI/NumberTheory/Ostmann/Tree/ArrangementTreeComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.arrangement_tree_component_count line 12
2. theorem OAI.Ostmann.arrangement_tree_comparison line 23

   Source documentation

   All component maps and their nonempty fibers are obtained from the actual bulk permutation; only the local Fourier bound is supplied.

   theorem arrangement_tree_comparison {p : ℕ} [Fact p.Prime]
       (hp : 3 ≤ p) (g : ZMod p → ℂ) (hg : g 0 = 0)
       (henergy : (∑ x : ZMod p, ‖g x‖ ^ 2) ≤ (p : ℝ))
       (ε : ℝ) (hε : 0 ≤ ε) (hflat : MixedFourierBound g ε)
       (n m : ℕ) (hm : 0 < m)
       (e : Equiv.Perm (TreeLeafIndex (n + 2) × Fin m))
       (hgood : 4 * Fintype.card (arrangementGraph m e).ConnectedComponent ≤
         3 * Fintype.card (TreeLeafIndex (n + 2)))
       (D₁ D₂ : (ZMod p)ˣ) {K₁ K₂ : (ZMod p)ˣ}
       (T₁ : RationalTreeData (ZMod p)ˣ (n + 2) K₁)
       (T₂ : RationalTreeData (ZMod p)ˣ (n + 2) K₂)
       (XL₁ XR₁ XL₂ XR₂ : (ZMod p)ˣ) (c₁ c₂ : TreeLeafTuple Bool (n + 2))
   …

   Mentions: OAI.Ostmann.MixedFourierBound, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.arrangementGraph, OAI.Ostmann.RationalTreeData, OAI.Ostmann.TreeLeafTuple