ArithmeticSplitData.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Fixed residue data at an exposed arithmetic split

structure OAI.Ostmann.ArithmeticSplitData line 15
Source documentation
All entries are known before the child product is exposed. The units contain the current giants and the nonbulk constants.
```
structure ArithmeticSplitData (Q : ℕ) where
…
```
instance OAI.Ostmann.ArithmeticSplitData.modulusNeZero line 25
def OAI.Ostmann.ArithmeticSplitData.reducedModulus line 28
def OAI.Ostmann.ArithmeticSplitData.test line 31
theorem OAI.Ostmann.ArithmeticSplitData.pair_probability_le line 38
def OAI.Ostmann.arithmeticPairSplitTest line 59
Source documentation
none means a preceding unit or support test failed. It has zero weight and does not impose any condition on an unexposed split.
```
def arithmeticPairSplitTest {Q : ℕ} (d : Option (ArithmeticSplitData Q × ArithmeticSplitData Q))
    (x : (ZMod Q)ˣ) : Prop :=
…
```
Mentions: OAI.Ostmann.ArithmeticSplitData
theorem OAI.Ostmann.arithmeticPairSplit_probability_le line 65

theorem OAI.Ostmann.arithmetic_sequential_support_le line 87

Source documentation

All residue data are functions of the exposed prefix alone. This derives the product bound for the actual two-history congruence tests.

theorem arithmetic_sequential_support_le {Q : ℕ} [NeZero Q]
    (data : List (ZMod Q)ˣ → Option (ArithmeticSplitData Q × ArithmeticSplitData Q))
    (B : ℕ → ℝ) (hB : ∀ j, 0 ≤ B j)
    (hbound : ∀ past d e, data past = some (d, e) →
      2 * ((d.reducedModulus.lcm e.reducedModulus).divisors.card : ℝ) ^ 2 /
        d.reducedModulus.lcm e.reducedModulus ≤ B past.length)
    (n : ℕ) :
    (Fintype.card (ZMod Q)ˣ : ℝ)⁻¹ ^ n *
        (∑ x : SplitSamples (ZMod Q)ˣ n,
          sequentialSupport (fun past y => arithmeticPairSplitTest (data past) y) [] n x) ≤
      ∏ j ∈ Finset.range n, B j := by
…

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