MovingPatternMixedCRT.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Identifying the actual mixed-giant pattern with its corrected CRT mean

theorem OAI.Ostmann.movingPatternHaarProduct_eq_image line 13

Source documentation

Each equality class contributes exactly one prime-square factor.

theorem movingPatternHaarProduct_eq_image {A B C : Type*} [Fintype C] {N n : ℕ}
    (e : Fin (N + 1) ≃ B ⊕ C) (prime : A → ℕ) (hprime : ∀ a, (prime a).Prime)
    (t : Bool → FrequencyTree ℤ n) (small bulk : Bool → TreeLeafTuple (List B) n)
    (pattern : Bool × MovingSampleIndex n → C) (x : Fin (N + 1) → A)
    (P : Finset ℕ) [∀ p : P, Fact p.val.Prime]
    (hP : P = Finset.univ.image (fun c : C => prime (x (e.symm (.inr c)))))
    (hinj : Function.Injective (fun c : C => prime (x (e.symm (.inr c))))) :
    movingPatternHaarProduct e prime hprime n t small bulk pattern x =
      ∏ p : P, movingInternalHaarAverage (fun i => prime (x i))
        (movingPatternFinData e n t small bulk pattern) p.val := by
…

Mentions: OAI.Ostmann.FrequencyTree, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.MovingSampleIndex, OAI.Ostmann.movingPatternHaarProduct, OAI.Ostmann.movingInternalHaarAverage, OAI.Ostmann.movingPatternFinData

theorem OAI.Ostmann.movingPatternPrimeObservable_crt line 59

Source documentation

The original mixed-prime observable, including its internal Haar factors, is the corrected mean of the separated residue coefficient.

theorem movingPatternPrimeObservable_crt (x : Fin (N + 1) → primes)
    (P : Finset ℕ) [∀ q : P, Fact q.val.Prime]
    [∀ b, NeZero (movingArithmeticModuli r p P Finset.univ b)]
    [NeZero (∏ b, movingArithmeticModuli r p P Finset.univ b)]
    (hP : P = Finset.univ.image (fun c : C => (x (e.symm (.inr c)) : ℕ)))
    (hinj : Function.Injective (fun c : C => (x (e.symm (.inr c)) : ℕ)))
    (hR : ∀ b, (movingPatternFinBulkData e n m t small slot perm pattern b).frequencyProduct ∣ R)
    (hprecision : R ^ (n + 1) ∣ (r : ℤ))
    (hcover : ∀ b, ∀ o ∈ (movingPatternFinBulkData e n m t small slot perm pattern b).occurrences,
      ∀ i ∈ o.current.compensationSlots, (x i : ℕ) ∈ P)
    (hc : Pairwise (fun b c => (movingArithmeticModuli r p P Finset.univ b).Coprime
      (movingArithmeticModuli r p P Finset.univ c)))
…

Mentions: OAI.Ostmann.primes, OAI.Ostmann.movingArithmeticModuli, OAI.Ostmann.movingPatternFinBulkData