OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticProductSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.arithmeticProductSupportSum line 13
2. theorem OAI.Ostmann.arithmeticProductSupportSum_eq line 25
3. theorem OAI.Ostmann.arithmetic_product_support_rate line 60

   Source documentation

   No restriction on the total leaf product appears here: this is the original independent product measure on all bulk leaf products.

   theorem arithmetic_product_support_rate {Q : ℕ} [NeZero Q]
       (n : ℕ) (K C ε : ℝ) (hC : 0 ≤ C) (hε : 0 < ε) :
       ∀ᶠ m : ℝ in atTop, ∀ N V : ℕ, ∀ Δ : ℝ, ∀ S : Finset ℤ,
         (N : ℝ) ≤ Real.exp (C * m) →
         (V : ℝ) ≤ Real.exp (Δ + Real.sqrt m) →
         (∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ N) →
         ∀ data : FrequencyTree (S × S) n → (ZMod Q)ˣ → List (ZMod Q)ˣ →
           Option (ArithmeticSplitData Q × ArithmeticSplitData Q),
         (∀ t P past d e, data t P past = some (d, e) →
           d.hasFrequencies (treeNodeFrequencies S n t past.length).1 ∧
             e.hasFrequencies (treeNodeFrequencies S n t past.length).2) →
         Real.exp (-(2 ^ n : ℕ) * Δ + K) * arithmeticProductSupportSum S V n data ≤
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.ArithmeticSplitData, OAI.Ostmann.treeNodeFrequencies, OAI.Ostmann.arithmeticProductSupportSum