OAI/NumberTheory/Ostmann/Arithmetic/MovingPatternPrimeSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.movingPattern_nonzero_prior line 15

   Source documentation

   The original coefficient can only be nonzero on its representative product prior. This implication does not replace repeated samples by independent ones.

   theorem movingPattern_nonzero_prior {A B C : Type*}
       [Fintype A] [Fintype B] [Fintype C] {N n : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (μ : ℕ → A → ℝ) (ν : B → A → ℝ)
       (prime : A → ℕ) (pattern : Bool × MovingSampleIndex n → C)
       (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c}) (E : ℝ)
       (hprime : ∀ a, (prime a).Prime) (hμ : ∀ j a, 0 ≤ μ j a) (hν : ∀ j a, 0 ≤ ν j a)
       (hbound : ∀ j a, (prime a : ℝ) * μ j a ≤ E)
       (G : (Fin (N + 1) → A) → ℂ) (x : Fin (N + 1) → A)
       (hx : movingOriginalPatternWeight e μ ν prime n pattern G x ≠ 0) :
       productPrior (fun i => Sum.elim ν
         (fun c => μ (movingSampleTier (rep c).val.2)) (e i)) x ≠ 0 := by
   …

   Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingOriginalPatternWeight, OAI.Ostmann.productPrior, OAI.Ostmann.movingSampleTier

2. theorem OAI.Ostmann.movingPattern_nonzero_internal_injective line 33
3. theorem OAI.Ostmann.movingPattern_prior_frequency_coprime line 45

   Source documentation

   All prime coprimality conditions against the actual history modulus follow from the lower endpoint of the original product prior.

   theorem movingPattern_prior_frequency_coprime {A B C : Type*}
       {N n : ℕ} (e : Fin (N + 1) ≃ B ⊕ C)
       (μ : ℕ → A → ℝ) (ν : B → A → ℝ) (prime : A → ℕ)
       (hprime : ∀ a, (prime a).Prime)
       (pattern : Bool × MovingSampleIndex n → C)
       (rep : ∀ c, {i : Bool × MovingSampleIndex n // pattern i = c})
       (S : Finset ℤ) (V : ℕ) (t : FrequencyTree (S × S) n)
       (hS : ∀ s ∈ S, s ≠ 0 ∧ s.natAbs ≤ V)
       (hμ : ∀ j a, μ j a ≠ 0 → V < prime a)
       (hν : ∀ j a, ν j a ≠ 0 → V < prime a)
       (x : Fin (N + 1) → A)
       (hx : productPrior (fun i => Sum.elim ν
   …

   Mentions: OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.FrequencyTree, OAI.Ostmann.productPrior

4. def OAI.Ostmann.movingPatternInternalPrimes line 67
5. theorem OAI.Ostmann.movingPatternInternalPrimes_prime line 71
6. theorem OAI.Ostmann.movingPattern_prime_moduli_coprime line 81

   Source documentation

   Distinct spectators and the prior's elementary prime coprimality give pairwise coprimality of every actual giant CRT block.

   theorem movingPattern_prime_moduli_coprime {A B C I : Type*} [Fintype C] [Fintype I] {N : ℕ}
       (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ) (hprime : ∀ a, (prime a).Prime)
       (x : Fin (N + 1) → A) (r : ℕ) (p : I → ℕ)
       (hp : ∀ i, (p i).Prime) (hinj : Function.Injective p)
       (hr : ∀ i, r.Coprime (prime (x i))) (hrp : ∀ i, r.Coprime (p i))
       (hsep : ∀ i j, prime (x j) ≠ p i) :
       Pairwise (fun a b =>
         (movingArithmeticModuli r p (movingPatternInternalPrimes e prime x) Finset.univ a).Coprime
         (movingArithmeticModuli r p (movingPatternInternalPrimes e prime x) Finset.univ b)) := by
   …

   Mentions: OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.movingPatternInternalPrimes