FiniteSpectralTree.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-tree spectral obstruction

The sparse/dense counting and Fourier-mass estimates give the spectral bound used in prop:finite-lower for the cyclic leaf coordinates and cheap translations.

theorem OAI.TreeEdit.BinaryLower.FiniteActivity.finite_tree_spectral_bound line 24

Source documentation

The complete sparse/dense spectral estimate on a finite tree. For the manuscript instantiate h=b=k, m=20*k, and C=(2*J/T)*M. The conclusion then reproduces eq:finite-root-upper before the final numerical estimate.

theorem finite_tree_spectral_bound {A σ : Type*}
    [AddCommGroup A] [Fintype A] [Fintype σ] [Nonempty σ]
    (m b h : ℕ) (hm : m ≠ 0) (hb : 0 < b)
    (w : List (Fin m) → A)
    (Q : (Fin h → Fin m) → ℕ) [∀ f, NeZero (Q f)]
    (φ : ∀ f, ZMod (Q f) →+ A)
    (hgen : ∀ f : Fin h → Fin m, w (List.ofFn f) = φ f 1)
    (H : AddChar A ℂ → ℝ) (hH : ∀ χ, 0 ≤ H χ)
    (shift : InternalNode (Fin m) h → σ → A) (M C : ℝ)
    (hleaf : ∀ f (z : ZMod (Q f)),
      (∑ χ, ‖1 - χ (φ f z)‖ ^ 2 * H χ) ≤ M / (m : ℝ) ^ h)
    (hdetect : ∀ v χ, characterSparse w b v χ →
…

Mentions: OAI.TreeEdit.BinaryLower.FiniteActivity.InternalNode, OAI.TreeEdit.BinaryLower.FiniteActivity.characterSparse