OAI/NumberTheory/Ostmann/Arithmetic/SampledHistoryEnergy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.treeIntegerResidues_prime_sample line 13
2. def OAI.Ostmann.sampledPrimeHistory line 24
3. theorem OAI.Ostmann.sampledPrimeHistory_residue line 33
4. theorem OAI.Ostmann.sampled_history_square_sum_le line 44

   Source documentation

   No new support probability is assumed: it is computed from the literal integer reversal equations of each nonzero sampled history.

   theorem sampled_history_square_sum_le (P : Finset ℕ) (S : Finset ℤ) (V n k : ℕ)
       (R : FrequencyTree S n → ℕ) [∀ t, NeZero (R t ^ (k + 2))]
       (D : FrequencyTree S n → PivotDependencyScheme (2 ^ n - 1))
       (hdepth : ∀ t i, (D t).depth i ≤ k)
       (hs : ∀ t i, ((D t).frequencies i).root ≠ 0)
       (hsR : ∀ t i, ((D t).frequencies i).root.natAbs ∣ R t)
       (T : TreeLeafIndex n → Finset ℕ)
       (hunit : ∀ t, ∀ p : P, (p : ℕ).Coprime (R t ^ (k + 2)))
       (pivots : FrequencyTree S n → (TreeLeafIndex n → P) → Fin (2 ^ n - 1) → ℤ)
       (W : FrequencyTree S n → (TreeLeafIndex n → P) → ℂ)
       (B : ℝ) (hB : 0 ≤ B)
       (hsize : ∀ t x, ‖W t x‖ ^ 2 ≤ B * frequencyLeafWeight (singleFrequencyLeaf S V) n t)
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.PivotDependencyScheme, OAI.Ostmann.TreeLeafIndex, OAI.Ostmann.frequencyLeafWeight, OAI.Ostmann.singleFrequencyLeaf