StoppingSelectedScale.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual selected-side size bounds. A nonzero cutoff bounds the final selected prime, while the stopping inequalities and geometric distortion bound the complete coefficient scale.

lemma OAI.CubicFirstMoment.cutoffMoebius_prime_norm_lt line 15
lemma OAI.CubicFirstMoment.geometric_selected_norm_distortion line 27
theorem OAI.CubicFirstMoment.stoppingSideTest_norm_bounds line 57
theorem OAI.CubicFirstMoment.stoppedBeta_norm_bounds line 107
theorem OAI.CubicFirstMoment.eventually_two_stage_stopped_dyad_range line 132

theorem OAI.CubicFirstMoment.eventually_two_stage_stopped_dyad_range_dilation line 165

Source documentation

A fixed ambient dilation has the same strict selected-scale range. The cutoff parameter remains X^ξ while the geometric distortion is measured on the actual ambient envelope C*X.

theorem eventually_two_stage_stopped_dyad_range_dilation {ξ ε C : ℝ}
    (hC : 0 < C) (hgap : ξ+ε < 1/100) :
    ∀ᶠ X : ℝ in atTop, ∀ (b Z N : ℝ),
      (Z = X^(36/100:ℝ) ∨ Z = X^(38/100:ℝ)) →
      Z ≤ N → N ≤ 2*(C*X)^ε*X^ξ*Z → b/2 ≤ N → N ≤ b →
      X^(35/100:ℝ) ≤ b ∧ b ≤ X^(39/100:ℝ) := by
…