MaskedResidueModel.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exact conditional law of the masked arithmetic residue model

abbrev OAI.JointDickman.BlockPrimePatterns line 12
def OAI.JointDickman.primePatternsSites line 14
theorem OAI.JointDickman.primePatternsSites_mem line 18
theorem OAI.JointDickman.primePatterns_empty_iff line 23
def OAI.JointDickman.maskedPrimeRootFamily line 37
theorem OAI.JointDickman.maskedPrimeRootFamily_local line 43

theorem OAI.JointDickman.masked_residue_disintegration line 61

Source documentation

The candidate set may depend on all exposed site patterns. The remaining conditional prime law is still the proved product law.

theorem masked_residue_disintegration {B M : ℕ}
    [∀ p : auxiliaryPrimes B, NeZero p.val]
    (hlarge : ∀ p ∈ auxiliaryPrimes B, M < p)
    (I : BlockPrimePatterns B M → Finset (BlockCandidateIndex M))
    (F : (H : BlockPrimePatterns B M) → (auxiliaryPrimes B → (I H).powerset) → ℝ) :
    (∑ r : ∀ p : auxiliaryPrimes B, ZMod p.val,
      finiteProductMass (fun (p : auxiliaryPrimes B) (_ : ZMod p.val) => 1/(p.val : ℝ)) r *
        F (fun p => blockPrimeHit M p.val (r p))
          (maskedPrimeRootFamily (I (fun p => blockPrimeHit M p.val (r p)))
            (fun p => blockPrimeHit M p.val (r p)) r)) =
    ∑ H : BlockPrimePatterns B M,
      categoricalProductMass univ (fun p : auxiliaryPrimes B => fun _ : Fin M => 1/(p.val : ℝ)) H *
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.BlockPrimePatterns, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.finiteProductMass, OAI.JointDickman.blockPrimeHit, OAI.JointDickman.maskedPrimeRootFamily, OAI.JointDickman.categoricalProductMass

def OAI.JointDickman.arithmeticPrimePatterns line 106
theorem OAI.JointDickman.primePatternsSites_arithmetic line 111
Source documentation
The observed site types are exactly the auxiliary prime divisors of all the translated integers in the block.
```
theorem primePatternsSites_arithmetic (B M u : ℕ) (i : Fin M) :
    primePatternsSites (arithmeticPrimePatterns B M u) i =
      coefficientPrimeSet B (u+(i.val+1)) := by
…
```
Mentions: OAI.JointDickman.primePatternsSites, OAI.JointDickman.arithmeticPrimePatterns, OAI.JointDickman.coefficientPrimeSet

theorem OAI.JointDickman.masked_arithmetic_crt line 130

Source documentation

Exact identification with an average over the actual arithmetic CRT period, still with the explicitly masked root tests.

theorem masked_arithmetic_crt {B M : ℕ}
    (hlarge : ∀ p ∈ auxiliaryPrimes B, M < p)
    (I : BlockPrimePatterns B M → Finset (BlockCandidateIndex M))
    (F : (H : BlockPrimePatterns B M) → (auxiliaryPrimes B → (I H).powerset) → ℝ) :
    (∑ u ∈ range (∏ p ∈ auxiliaryPrimes B, p),
      F (arithmeticPrimePatterns B M u)
        (maskedPrimeRootFamily (I (arithmeticPrimePatterns B M u))
          (arithmeticPrimePatterns B M u) (fun p => (u : ZMod p.val)))) /
      (∏ p ∈ auxiliaryPrimes B, (p : ℝ)) =
    ∑ H : BlockPrimePatterns B M,
      categoricalProductMass univ (fun p : auxiliaryPrimes B => fun _ : Fin M => 1/(p.val : ℝ)) H *
        ∑ R, siteConditionedRootProductMass B (I H) (primePatternsSites H) R * F H R := by
…

Mentions: OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.BlockPrimePatterns, OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.arithmeticPrimePatterns, OAI.JointDickman.maskedPrimeRootFamily, OAI.JointDickman.categoricalProductMass, OAI.JointDickman.siteConditionedRootProductMass, OAI.JointDickman.primePatternsSites