MovingPatternMixedIntegralCRT.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating the exact mixed CRT identity with its original outer factors

theorem OAI.Ostmann.movingPatternPrimeObservable_weighted_integral_crt line 30

Source documentation

Any outer factor can be retained through the finite CRT identity and both giant integrals. The physical integer measure is exp(z-center) dz.

theorem movingPatternPrimeObservable_weighted_integral_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

theorem OAI.Ostmann.movingPatternPrimeObservable_outer_integral_crt line 83

Source documentation

The ideal diagonal environment is exactly the same CRT integral, with the two outer cutoffs and remaining inactive regular density retained.

theorem movingPatternPrimeObservable_outer_integral_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