OAI/NumberTheory/Ostmann/Arithmetic/MovingSeparatedPageDeletion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingArithmeticModuli_coprime_product line 13

   Source documentation

   Prime factors in a regular block are disjoint from the frequency, internal and spectator factors of the separated modulus.

   theorem movingArithmeticModuli_coprime_product {I J : Type*} [Fintype I] [Fintype J]
       (r : ℕ) (p : I → ℕ) (P : Finset ℕ) (reg : J → ℕ)
       (hp : ∀ i, (p i).Prime) (hP : ∀ q ∈ P, q.Prime) (hreg : ∀ j, (reg j).Prime)
       (hr : ∀ j, (reg j).Coprime r)
       (hregP : ∀ j q, q ∈ P → reg j ≠ q) (hregp : ∀ j i, reg j ≠ p i) :
       (∏ j, reg j).Coprime (∏ b, movingArithmeticModuli r p P Finset.univ b) := by
   …

   Mentions: OAI.Ostmann.movingArithmeticModuli

2. theorem OAI.Ostmann.frequencyModel_deleted_prime_coprime line 36

   Source documentation

   The prescribed deleted conductor prime is coprime to the full separated arithmetic block. The frequency part is smaller than the deletion threshold.

   theorem frequencyModel_deleted_prime_coprime {I : Type*} [Fintype I]
       (S : Finset ℤ) (n V cutoff : ℕ) (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ V) (hcut : V < cutoff)
       (P : Finset ℕ) (p : I → ℕ) (hP : ∀ q ∈ P, q.Prime) (hp : ∀ i, (p i).Prime)
       (q : ℕ) (hq : q.Prime) (hlarge : cutoff ≤ q)
       (hneqP : q ∉ P) (hneqp : ∀ i, q ≠ p i) :
       q.Coprime (∏ b, movingArithmeticModuli (frequencyModelBase S n t ^ (n - 1 + 2))
         p P Finset.univ b) := by
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.frequencyModelBase

3. theorem OAI.Ostmann.frequencyModel_regular_page_projection line 60

   Source documentation

   The regular block contributes no Page correction under exactly the conductor-prime deletion used to construct the original priors.

   theorem frequencyModel_regular_page_projection {I J : Type*} [Fintype I] [Fintype J]
       (S : Finset ℤ) (n V cutoff : ℕ) (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ V) (hcut : V < cutoff)
       (P : Finset ℕ) (p : I → ℕ) (reg : J → ℕ) (z : Option PrimitiveRealZero)
       (hP : ∀ q ∈ P, q.Prime) (hp : ∀ i, (p i).Prime)
       (hreg : ∀ j, (reg j).Prime ∧ cutoff ≤ reg j)
       (hdeleteP : ∀ e, z = some e → ∀ q,
         deletedConductorPrime e.modulus cutoff = some q → q ∉ P)
       (hdeletep : ∀ e, z = some e → ∀ q,
         deletedConductorPrime e.modulus cutoff = some q → ∀ i, q ≠ p i)
       (hdeletereg : ∀ e, z = some e → ∀ q,
         deletedConductorPrime e.modulus cutoff = some q → ∀ j, q ≠ reg j) :
   …

   Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.deletedConductorPrime