StoppingCoefficientShift.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Recovering the smaller-envelope labels on actual nonzero stopped coefficients, and transporting the independent remaining-side coefficient. All finite support and both stopping thresholds stay unchanged.

lemma OAI.CubicFirstMoment.stoppingSideTest_label_shift_bound line 16
lemma OAI.CubicFirstMoment.stoppedBeta_label_shift_bound line 32
theorem OAI.CubicFirstMoment.stoppedBeta_geometric_eq_row_of_bounds line 53

theorem OAI.CubicFirstMoment.stoppedBeta_early_geometric_eq_row line 74

Source documentation

On a surviving early row both original labels have a valid smaller envelope label; the beta is the literal row used in the analytic theorem.

theorem stoppedBeta_early_geometric_eq_row {ρ X F : ℝ} (hρ : 1 < ρ)
    (hX : 0 < X) (hXF : X ≤ F) (W : ι → ℝ → ℂ) (w z Z Q : ℝ)
    {j k h : ℕ} (hk : 1 ≤ k) (hjh : j < h)
    {b : Eisenstein} (hb : primary b) (hbX : norm b ≤ X)
    (hne : stoppedBeta (primaryElementBall F) (primaryElementBall F)
      (distinguishedTupleCoefficient (fun _ : ι => primeCutoff F)
        (fun i p => W i (norm p)) primeDetectorCutoff w z)
      primeDetectorCutoff w
      (stoppedSideTest (geometricPrimeBin ρ F) (geometricBinLower ρ F) j k h Z Q true) b ≠ 0) :
    stoppedBeta (primaryElementBall F) (primaryElementBall F)
      (distinguishedTupleCoefficient (fun _ : ι => primeCutoff F)
        (fun i p => W i (norm p)) primeDetectorCutoff w z)
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.stoppedBeta, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.distinguishedTupleCoefficient, OAI.CubicFirstMoment.primeCutoff, OAI.CubicFirstMoment.primeDetectorCutoff, OAI.CubicFirstMoment.stoppedSideTest, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower

lemma OAI.CubicFirstMoment.geometricStoppingRemainingTest_shift line 97
theorem OAI.CubicFirstMoment.stoppedAlpha_geometric_restrict line 121