OAI/NumberTheory/Ostmann/Arithmetic/SingleHistorySupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.diagonalSplitData line 13
2. def OAI.Ostmann.singleArithmeticSplitTest line 16
3. theorem OAI.Ostmann.diagonalSplitData_test line 21
4. def OAI.Ostmann.singleArithmeticLeafSupport line 26
5. theorem OAI.Ostmann.singleArithmeticLeafSupport_nonneg line 32
6. theorem OAI.Ostmann.single_arithmetic_leaf_support_le line 39

   Source documentation

   The already proved joint root bound, applied twice to the same test, loses no additional frequency choices or support conditions.

   theorem single_arithmetic_leaf_support_le {Q : ℕ} [NeZero Q]
       (data : List (ZMod Q)ˣ → Option (ArithmeticSplitData Q))
       (frequencies : ℕ → NodeFrequencies) (D : ℝ) (hD : 0 ≤ D)
       (hmatch : ∀ past d, data past = some d → d.hasFrequencies (frequencies past.length))
       (hdiv : ∀ j, ((frequencies j).reducedModulus.divisors.card : ℝ) ≤ D)
       (n : ℕ) (P : (ZMod Q)ˣ) :
       (Fintype.card (TreeLeafFiber (ZMod Q)ˣ n P) : ℝ)⁻¹ *
         (∑ x : TreeLeafFiber (ZMod Q)ˣ n P,
           sequentialSupport (fun past y => singleArithmeticSplitTest (data past) y) []
             (2 ^ n - 1) (treeLeafSplitEquiv n P x)) ≤
         ∏ j ∈ Finset.range (2 ^ n - 1), singleFrequencySupportBound D (frequencies j) := by
   …

   Mentions: OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.NodeFrequencies, OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.sequentialSupport, OAI.Ostmann.singleArithmeticSplitTest, OAI.Ostmann.treeLeafSplitEquiv, OAI.Ostmann.singleFrequencySupportBound

7. theorem OAI.Ostmann.single_arithmetic_leaf_average_le line 69

   Source documentation

   Pointwise in the frequency history and independent of the size of Q. This permits the modulus to be chosen separately for each history.

   theorem single_arithmetic_leaf_average_le {Q : ℕ} [NeZero Q]
       (S : Finset ℤ) (N n : ℕ) (D : ℝ) (hD : 0 ≤ D)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N)
       (hdiv : ∀ q : ℕ, q ≠ 0 → q ≤ N ^ 2 → (q.divisors.card : ℝ) ≤ D)
       (t : FrequencyTree S n)
       (data : (ZMod Q)ˣ → List (ZMod Q)ˣ → Option (ArithmeticSplitData Q))
       (hmatch : ∀ P past d, data P past = some d →
         d.hasFrequencies (singleTreeNodeFrequencies S n t past.length)) :
       (Fintype.card (TreeLeafTuple (ZMod Q)ˣ n) : ℝ)⁻¹ *
         (∑ x : TreeLeafTuple (ZMod Q)ˣ n, singleArithmeticLeafSupport n data x) ≤
         ((singleFrequencySplitList S n t).map (singleFrequencySupportBound D)).prod := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.singleTreeNodeFrequencies, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.singleArithmeticLeafSupport, OAI.Ostmann.singleFrequencySplitList, OAI.Ostmann.singleFrequencySupportBound

8. def OAI.Ostmann.singleArithmeticSupportSum line 100
9. theorem OAI.Ostmann.single_arithmetic_support_sum_le line 109

   Source documentation

   The exponent is 2^n, the number of leaves of one history. Thus its initial squared weight cancels the entire leading leaf-frequency cost.

   theorem single_arithmetic_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)
       (data : FrequencyTree S n → (ZMod Q)ˣ → List (ZMod Q)ˣ → Option (ArithmeticSplitData Q))
       (hmatch : ∀ t P past d, data t P past = some d →
         d.hasFrequencies (singleTreeNodeFrequencies S n t past.length)) :
       singleArithmeticSupportSum S V n data ≤
         (4 * D ^ 3 * (1 + Real.log N)) ^ (2 ^ n - 1) * (2 * (V : ℝ)) ^ (2 ^ n) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.singleTreeNodeFrequencies, OAI.Ostmann.singleArithmeticSupportSum