OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticHistorySupportSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.gcd_frequency_divisor_bound line 11
2. theorem OAI.Ostmann.arithmetic_history_support_sum_le line 28

   Source documentation

   The bulk residue variables are still sampled from the original Haar law. Data at each node depend only on earlier split products; the only extra weights are the restrictions on the leaf frequencies.

   theorem arithmetic_history_support_sum_le {Q : ℕ} [NeZero Q]
       (S : Finset ℤ) (N V n : ℕ) (D : ℝ) (hD : 0 ≤ D)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N)
       (hdiv : ∀ q : ℕ, q ≠ 0 → q ≤ N ^ 2 → (q.divisors.card : ℝ) ≤ D)
       (P : FrequencyTree (S × S) n → (ZMod Q)ˣ)
       (data : FrequencyTree (S × S) n → List (ZMod Q)ˣ →
         Option (ArithmeticSplitData Q × ArithmeticSplitData Q))
       (hmatch : ∀ t past d e, data t past = some (d, e) →
         d.hasFrequencies (treeNodeFrequencies S n t past.length).1 ∧
           e.hasFrequencies (treeNodeFrequencies S n t past.length).2) :
       (∑ t : FrequencyTree (S × S) n,
         frequencyLeafWeight (pairedFrequencyLeaf S V) n t *
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.treeNodeFrequencies, OAI.Ostmann.frequencyLeafWeight, OAI.Ostmann.pairedFrequencyLeaf