PrimePaddingFactorization.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Exact independence of tuple-prime and padding-prime observables under the actual union residue law.

lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_sum_product line 17
def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.tupleRestriction line 47
def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.tupleResidueLaw line 50
lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residue_average_tuple_padding line 56

lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residue_average_prime_boolean_padding line 96

Source documentation

Prime divisibility observables and an arbitrary padding-periodic integer weight are independent at the same translated CRT origin.

lemma residue_average_prime_boolean_padding
    (hB : ∀ p ∈ data.P ∪ data.Q, p ≤ B) (site : ℤ)
    (F : (data.P → Bool) → ℝ) (g : ℤ → ℝ)
    (hg : ∀ n m : ℤ, (∀ q ∈ data.Q, (n : ZMod q) = (m : ZMod q)) → g n = g m) :
    (data.residueLaw B hB).average (fun x =>
      F (fun p : data.P => decide ((p.val : ℤ) ∣ data.residueOrigin x + site)) *
        g (data.residueOrigin x + site)) =
      (paddingOriginalLaw data.P (fun p hp => (data.primeP p hp).two_le)).average F *
        (data.paddingResidueLaw B hB).average (fun z =>
          g (data.paddingResidueOrigin z + site)) := by
…

Mentions: OAI.TwoPointCorrelations.paddingOriginalLaw

lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.positive_prime_padding_average line 140
theorem OAI.TwoPointCorrelations.ProhibitedPrimeFamily.positive_prime_padding_degree_tail line 163