OAI/NumberTheory/Ostmann/Construction/WordPrimeCheckBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.WordPrimeDecoration.checkAt line 13
2. theorem OAI.Ostmann.WordPrimeDecoration.checkAt_mem line 19
3. theorem OAI.Ostmann.WordPrimeDecoration.checkAt_all line 24
4. theorem OAI.Ostmann.word_prime_checks_bound line 41

   Source documentation

   W may already contain the other history, all range/unit gates and the graph phase. Its support supplies the literal validity of this history. The right side uses the derived number and degree of the prime checks.

   theorem word_prime_checks_bound
       {A : Type*} [Fintype A] [Nonempty A] {m n : ℕ}
       (prime : A → ℕ) (hpInj : Function.Injective prime) (hprime : ∀ a, (prime a).Prime)
       (D : WordPrimeDecoration (Fin (m + 1)) n)
       (template : WordTransferTemplate (ExpandedScheduledVariable (Fin (m + 1)) n) n)
       (t : FrequencyTree ℤ n) (ht : NonzeroInternalFrequencies n t)
       (B : ℕ) (hB : 1 ≤ B) (hwords : template.WordsBounded B)
       (μ : Fin (m + 1) → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a) (hmass : ∀ i, ∑ a, μ i a = 1)
       (α β V R : ℝ) (hα : 0 ≤ α) (hβ : 0 ≤ β) (hV : 0 < V) (hR : 3 ≤ R)
       (hmax : ∀ i a, μ i a ≤ α) (hpmax : ∀ i a, μ i a ≤ β)
       (hlower : ∀ a, V ≤ Real.log (prime a : ℝ)) (hupper : ∀ a, (prime a : ℝ) ≤ R)
       (hfreq : ∀ s ∈ allFrequencyList n t, |(s : ℝ)| ≤ R)
   …

   Mentions: OAI.Ostmann.WordPrimeDecoration, OAI.Ostmann.WordTransferTemplate, OAI.Ostmann.ExpandedScheduledVariable, OAI.Ostmann.FrequencyTree, OAI.Ostmann.NonzeroInternalFrequencies, OAI.Ostmann.allFrequencyList