ConditionedPrimeResidues.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Identifying conditional residue fibers with the candidate root model

def OAI.JointDickman.emptyBlockPrimeHit line 11
theorem OAI.JointDickman.blockPrimeHit_empty_iff line 14
theorem OAI.JointDickman.blockPrimeFiber_empty line 32
theorem OAI.JointDickman.emptyBlockPrimeFiber_pos line 39
theorem OAI.JointDickman.blockPrimeImageMass line 45
def OAI.JointDickman.maskedCandidatePrimeHit line 52
theorem OAI.JointDickman.emptySite_candidate_push line 60
Source documentation
At the empty site pattern, the conditional root law is exactly the uniform residue law outside the forbidden classes.
```
theorem emptySite_candidate_push {M p : ℕ} [Fact p.Prime]
    (I : Finset (BlockCandidateIndex M)) (hp : M < p) (R : I.powerset) :
    finitePushMass (totalUniformConditionalMass (blockPrimeHit M p) (emptyBlockPrimeHit M))
      (rootHitType I (candidateModRoot p)) R = outsideCandidatePrimeMass I p R := by
…
```
Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.finitePushMass, OAI.JointDickman.totalUniformConditionalMass, OAI.JointDickman.blockPrimeHit, OAI.JointDickman.emptyBlockPrimeHit, OAI.JointDickman.rootHitType, OAI.JointDickman.candidateModRoot, OAI.JointDickman.outsideCandidatePrimeMass
theorem OAI.JointDickman.maskedCandidatePrimeHit_push line 94
Source documentation
Occupied classes have zero masked tests; empty classes retain their actual conditional residue law. Both branches are exact identities.
```
theorem maskedCandidatePrimeHit_push {M p : ℕ} [Fact p.Prime]
    (I : Finset (BlockCandidateIndex M)) (hp : M < p)
    (H : (univ : Finset (Fin M)).powerset) (R : I.powerset) :
    finitePushMass (totalUniformConditionalMass (blockPrimeHit M p) H)
      (maskedCandidatePrimeHit I p H) R =
    if H = emptyBlockPrimeHit M then outsideCandidatePrimeMass I p R else
      (if R.val = ∅ then 1 else 0) := by
…
```
Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.finitePushMass, OAI.JointDickman.totalUniformConditionalMass, OAI.JointDickman.blockPrimeHit, OAI.JointDickman.maskedCandidatePrimeHit, OAI.JointDickman.emptyBlockPrimeHit, OAI.JointDickman.outsideCandidatePrimeMass