OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticSplitTreeSupport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Ostmann.NodeFrequencies line 11
2. def OAI.Ostmann.NodeFrequencies.reducedModulus line 16
3. def OAI.Ostmann.ArithmeticSplitData.hasFrequencies line 19
4. theorem OAI.Ostmann.ArithmeticSplitData.reducedModulus_eq line 23
5. def OAI.Ostmann.pairFrequencySupportBound line 27
6. theorem OAI.Ostmann.pairFrequencySupportBound_nonneg line 30
7. theorem OAI.Ostmann.arithmetic_support_fixed_frequencies line 35

   Source documentation

   The reduced moduli depend only on the fixed frequencies. All pivot and unit data may still vary with the previously exposed split products.

   theorem arithmetic_support_fixed_frequencies {Q : ℕ} [NeZero Q]
       (data : List (ZMod Q)ˣ → Option (ArithmeticSplitData Q × ArithmeticSplitData Q))
       (frequencies : ℕ → NodeFrequencies × NodeFrequencies) (D : ℝ) (_hD : 0 ≤ D)
       (hmatch : ∀ past d e, data past = some (d, e) →
         d.hasFrequencies (frequencies past.length).1 ∧
           e.hasFrequencies (frequencies past.length).2)
       (hdiv : ∀ j, (((frequencies j).1.reducedModulus.lcm
         (frequencies j).2.reducedModulus).divisors.card : ℝ) ≤ D)
       (n : ℕ) :
       (Fintype.card (ZMod Q)ˣ : ℝ)⁻¹ ^ n *
           (∑ x : SplitSamples (ZMod Q)ˣ n,
             sequentialSupport (fun past y => arithmeticPairSplitTest (data past) y) [] n x) ≤
   …

   Mentions: OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.NodeFrequencies, OAI.Ostmann.SplitSamples, OAI.Ostmann.sequentialSupport, OAI.Ostmann.arithmeticPairSplitTest

8. theorem OAI.Ostmann.arithmetic_leaf_support_fixed_frequencies line 59

   Source documentation

   The same product estimate on the original uniformly sampled leaf tuples, conditional only on their total product.

   theorem arithmetic_leaf_support_fixed_frequencies {Q : ℕ} [NeZero Q]
       (data : List (ZMod Q)ˣ → Option (ArithmeticSplitData Q × ArithmeticSplitData Q))
       (frequencies : ℕ → NodeFrequencies × NodeFrequencies) (D : ℝ) (hD : 0 ≤ D)
       (hmatch : ∀ past d e, data past = some (d, e) →
         d.hasFrequencies (frequencies past.length).1 ∧
           e.hasFrequencies (frequencies past.length).2)
       (hdiv : ∀ j, (((frequencies j).1.reducedModulus.lcm
         (frequencies j).2.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 => arithmeticPairSplitTest (data past) y) []
   …

   Mentions: OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.NodeFrequencies, OAI.Ostmann.TreeLeafFiber, OAI.Ostmann.sequentialSupport, OAI.Ostmann.arithmeticPairSplitTest