OAI/Combinatorics/BinaryEdit/FiniteVectorDetection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TreeEdit.BinaryLower.FiniteVectors.sparse_node_detection line 24

   Source documentation

   The actual finite-tree cheap vector detects any active distinguished vector whose children have support smaller than k. Exact orders and primality are unnecessary here: the proved annihilating periods suffice.

   theorem sparse_node_detection {m k : ℕ}
       (p : Fin k → Fin m → ℕ) (hk : 1 ≤ k)
       (hppos : ∀ q i, 0 < p q i) (hp : ∀ q i, p q i ≤ k ^ 5)
       (j : ℕ) (hj : j < k) (a : Leaf m k) (χ : AddChar (State p) ℂ)
       (hactive : χ (w p j a) ≠ 1)
       (hsparse : (Finset.univ.filter fun i : Fin m =>
         χ (w p (j + 1) (Function.update a ⟨j, hj⟩ i)) ≠ 1).card < k) :
       ((4 * k ^ (10 * k) : ℕ) : ℝ) ≤
         ∑ s : Fin (4 * k ^ (10 * k)), ‖1 - χ ((s.val + 1) • u p j a)‖ ^ 2 := by
   …

   Mentions: OAI.TreeEdit.BinaryLower.FiniteVectors.Leaf, OAI.TreeEdit.BinaryLower.FiniteVectors.State, OAI.TreeEdit.BinaryLower.FiniteVectors.w, OAI.TreeEdit.BinaryLower.FiniteVectors.u

2. theorem OAI.TreeEdit.BinaryLower.FiniteActivity.characterSparse_detection line 63

   Source documentation

   The exact unnormalized finite-sample detector required by finite_tree_spectral_bound, with the sparse predicate and child list indices unchanged. All hypotheses are local vector/period identities.

   theorem characterSparse_detection {α A : Type*}
       [Fintype α] [AddCommGroup A] [Finite A] {k : ℕ}
       (w : List α → A) (v : InternalNode α k) (u : A)
       (Q R : ℕ) (p : α → ℕ) (hk : 1 ≤ k)
       (hQpos : 0 < Q) (hQ : Q ≤ 2 * k ^ (5 * v.1.val))
       (hppos : ∀ i, 0 < p i) (hp : ∀ i, p i ≤ k ^ 5)
       (hroot : w (List.ofFn v.2) = R • u)
       (hsum : u = ∑ i, w (List.ofFn v.2 ++ [i]))
       (hchild : ∀ i, (Q * p i) • w (List.ofFn v.2 ++ [i]) = 0)
       (χ : AddChar A ℂ) (hsparse : characterSparse w k v χ) :
       ((4 * k ^ (10 * k) : ℕ) : ℝ) ≤
         ∑ s : Fin (4 * k ^ (10 * k)), ‖1 - χ ((s.val + 1) • u)‖ ^ 2 := by
   …

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