SparseCharacterPeriod.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Periods of products supported on few children

This is the period estimate used for sparse active frequencies in prop:finite-lower. An annihilating period suffices; no exact order or lcm calculation is needed for this step.

lemma OAI.TreeEdit.BinaryLower.FinitePeriod.product_period line 18
lemma OAI.TreeEdit.BinaryLower.FinitePeriod.product_period_pos line 28
lemma OAI.TreeEdit.BinaryLower.FinitePeriod.product_period_upper line 33
lemma OAI.TreeEdit.BinaryLower.FinitePeriod.character_finset_sum line 49

lemma OAI.TreeEdit.BinaryLower.FinitePeriod.character_supported_period line 60

Source documentation

The product period annihilates the character of the sum, even when the underlying vectors outside the active set are nonzero.

lemma character_supported_period {ι A : Type*} [Fintype ι] [AddCommGroup A]
    (χ : AddChar A ℂ) (s : Finset ι) (w : ι → A) (Q : ℕ) (p : ι → ℕ)
    (houtside : ∀ i, i ∉ s → χ (w i) = 1)
    (hchild : ∀ i ∈ s, (Q * p i) • w i = 0) :
    χ ((Q * ∏ i ∈ s, p i) • ∑ i, w i) = 1 := by
…

theorem OAI.TreeEdit.BinaryLower.FinitePeriod.sparse_character_detection line 77

Source documentation

Sparse active children are detected by the source's fixed short averaging interval. All stated inputs are local period and support facts; no Fourier identity or edit-distance conclusion is assumed here.

theorem sparse_character_detection {ι A : Type*} [Fintype ι]
    [AddCommGroup A] [Finite A]
    (χ : AddChar A ℂ) (s : Finset ι) (w : ι → A)
    {k j Q R : ℕ} (p : ι → ℕ)
    (hk : 1 ≤ k) (hj : j < k) (hs : s.card < k)
    (hQpos : 0 < Q) (hQ : Q ≤ 2 * k ^ (5 * j))
    (hppos : ∀ i ∈ s, 0 < p i) (hp : ∀ i ∈ s, p i ≤ k ^ 5)
    (houtside : ∀ i, i ∉ s → χ (w i) = 1)
    (hchild : ∀ i ∈ s, (Q * p i) • w i = 0)
    (hactive : χ (R • ∑ i, w i) ≠ 1) :
    1 ≤ (∑ a ∈ Finset.range (4 * k ^ (10 * k)),
      ‖1 - χ ((a + 1) • ∑ i, w i)‖ ^ 2) / (4 * k ^ (10 * k) : ℕ) := by
…