PrimeStoppingPairs.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Inverting the independent stopping predicates reconstructs the exact selected divisor and complementary divisor of the original squarefree term.

lemma OAI.CubicFirstMoment.primeFactors_disjoint_of_squarefree_mul line 13

theorem OAI.CubicFirstMoment.stopping_pair_reconstruction line 26

Source documentation

The independent selected and remaining predicates give an actual selection in the original factor set, with the exact two products and exact inverse-binomial denominator.

theorem stopping_pair_reconstruction {d e r : Eisenstein}
    (hd : primary d) (he : primary e) (hs : Squarefree (d*e))
    (bin : Eisenstein → ℕ) (ell : ℕ → ℝ) (j k l : ℕ) (Z : ℝ)
    (hselected : stoppingSideTest bin ell j k Z r d)
    (hremaining : stoppingRemainingTest bin j l e) :
    ∃ t ∈ (primeBin (primaryPrimeFactors (d*e)) bin j).powersetCard k,
      (∏ p ∈ stoppingSelected (primaryPrimeFactors (d*e)) bin j t, p) = d ∧
      (∏ p ∈ stoppingRemainder (primaryPrimeFactors (d*e)) bin j t, p) = e ∧
      (primeBin (primaryPrimeFactors (d*e)) bin j).card = k+l ∧
      (norm r*primeSurrogate
          (stoppingSelected (primaryPrimeFactors (d*e)) bin j t) bin ell/ell j < Z ∧
        Z ≤ norm r*primeSurrogate
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.stoppingSideTest, OAI.CubicFirstMoment.stoppingRemainingTest, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.stoppingSelected, OAI.CubicFirstMoment.stoppingRemainder, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeSurrogate