StoppingFailedStage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The failed first stage of an ordinary stop is a condition on the selected divisor alone; this identifies it with the original prefix.

lemma OAI.CubicFirstMoment.selected_crossing_after_failed_prefix line 12
lemma OAI.CubicFirstMoment.stoppedSideTest_selected_failed_prefix line 33

lemma OAI.CubicFirstMoment.stoppedSideTest_selected_of_failed_prefix line 51

Source documentation

On an original term which failed the first threshold, every later crossing automatically satisfies the selected-side failure predicate.

lemma stoppedSideTest_selected_of_failed_prefix (s : Finset Eisenstein)
    (hs : ∀ p ∈ s, primaryPrime p) (bin : Eisenstein → ℕ) (ell : ℕ → ℝ)
    (hell : ∀ j, 1 ≤ ell j) {h j k : ℕ} {t : Finset Eisenstein}
    (ht : t ⊆ primeBin s bin j) (Z Q : ℝ) (r : Eisenstein)
    (hfailed : norm r*primeSurrogate (primeBinPrefix s bin h) bin ell < Q)
    (hQZ : Q ≤ Z) :
    stoppedSideTest bin ell j k h Z Q false r (∏ p ∈ stoppingSelected s bin j t, p) ↔
      stoppingSideTest bin ell j k Z r (∏ p ∈ stoppingSelected s bin j t, p) := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.primeBin, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primeSurrogate, OAI.CubicFirstMoment.primeBinPrefix, OAI.CubicFirstMoment.stoppedSideTest, OAI.CubicFirstMoment.stoppingSelected, OAI.CubicFirstMoment.stoppingSideTest