StoppedRowRestriction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact finite-envelope changes for the actual stopped coefficient. Every factor in a fibre divides its prescribed product. Thus a bounded product uses only the smaller prime and divisor cutoffs. The selected-side predicate is retained verbatim, including any extra restriction.

lemma OAI.CubicFirstMoment.stoppedBeta_selected_congr line 15
lemma OAI.CubicFirstMoment.primaryPairFiber_ball_restrict line 28
lemma OAI.CubicFirstMoment.primeTupleFiber_restrict line 48
lemma OAI.CubicFirstMoment.distinguishedTupleCoefficient_restrict line 63
lemma OAI.CubicFirstMoment.stoppedBeta_restrict_left line 71
lemma OAI.CubicFirstMoment.stoppedBeta_tuple_ball_restrict line 82
lemma OAI.CubicFirstMoment.stoppedBeta_tuple_support line 101
theorem OAI.CubicFirstMoment.stoppedBeta_eq_stoppedRowCoefficient line 138
Source documentation
The actual finite-envelope beta, with its exact selected predicate, is the analytic row at norm twist zero on every bounded primary product.
```
theorem stoppedBeta_eq_stoppedRowCoefficient {X F : ℝ} (hXF : X ≤ F)
    (W : ι → ℝ → ℂ) (w z : ℝ)
    (selected : Eisenstein → Eisenstein → Prop)
    {b : Eisenstein} (hb : primary b) (hbX : norm b ≤ X) :
    stoppedBeta (primaryElementBall F) (primaryElementBall F)
      (distinguishedTupleCoefficient (fun _ : ι => primeCutoff F)
        (fun i p => W i (norm p)) primeDetectorCutoff w z)
      primeDetectorCutoff w selected b =
      stoppedRowCoefficient X w z 0 W selected b := by
…
```
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.stoppedRowCoefficient