OAI/NumberTheory/Ostmann/Arithmetic/CompensatedHistoryEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.compensated_history_square_sum_le line 14

   Source documentation

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

   theorem compensated_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))
       (U : FrequencyTree S n → Fin (2 ^ n - 1) → ℤ)
       (hU : ∀ t i, IsCoprime (U t i) (R t : ℤ))
       (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) → ℂ)
   …

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