FinitePeriod.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Short-period detection for the finite-tree obstruction

Complete-period averaging gives the short-period detection estimate in prop:finite-lower.

lemma OAI.TreeEdit.BinaryLower.FinitePeriod.sum_range_period_mul line 16

lemma OAI.TreeEdit.BinaryLower.FinitePeriod.periodic_sum_lower line 35

Source documentation

Full periods occupy at least half of any interval of length at least twice its positive period. No divisibility of J by q is required.

lemma periodic_sum_lower {f : ℕ → ℝ} {q J : ℕ}
    (hq : 0 < q) (hJ : 2 * q ≤ J)
    (hperiod : Function.Periodic f q) (hnonneg : ∀ s, 0 ≤ f s)
    (hcycle : ∑ s ∈ Finset.range q, f s = 2 * (q : ℝ)) :
    (J : ℝ) ≤ ∑ s ∈ Finset.range J, f s := by
…

lemma OAI.TreeEdit.BinaryLower.FinitePeriod.norm_one_sub_sq line 59
lemma OAI.TreeEdit.BinaryLower.FinitePeriod.root_cycle_sum line 67
Source documentation
Complete nontrivial root-of-unity periods have mean squared displacement exactly two. Primitivity is unnecessary: any positive period works.
```
lemma root_cycle_sum {z : ℂ} {q : ℕ} (hz : ‖z‖ = 1)
    (hne : z ≠ 1) (hroot : z ^ q = 1) :
    ∑ s ∈ Finset.range q, ‖1 - z ^ (s + 1)‖ ^ 2 = 2 * (q : ℝ) := by
…
```

theorem OAI.TreeEdit.BinaryLower.FinitePeriod.root_short_average line 84

Source documentation

Short-period detection used at every sparse active internal node.

theorem root_short_average {z : ℂ} {q J : ℕ}
    (hq : 0 < q) (hJ : 2 * q ≤ J) (hz : ‖z‖ = 1)
    (hne : z ≠ 1) (hroot : z ^ q = 1) :
    1 ≤ (∑ s ∈ Finset.range J, ‖1 - z ^ (s + 1)‖ ^ 2) / (J : ℝ) := by
…

theorem OAI.TreeEdit.BinaryLower.FinitePeriod.character_short_average line 101

Source documentation

A character specialization in exactly the source's cheap-shift notation. Only a period of the character value is required; it need not be a period of u itself. Activity after multiplying by R guarantees nontriviality.

theorem character_short_average {A : Type*} [AddCommGroup A] [Finite A]
    (χ : AddChar A ℂ) (u : A) {q J R : ℕ}
    (hq : 0 < q) (hJ : 2 * q ≤ J)
    (hactive : χ (R • u) ≠ 1) (hperiod : χ (q • u) = 1) :
    1 ≤ (∑ s ∈ Finset.range J, ‖1 - χ ((s + 1) • u)‖ ^ 2) / (J : ℝ) := by
…