PolynomialScaleSelection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Choose a single power of the geometric parameter for the finitely many smallness conditions in the initial correction block. The exponent is chosen before the multiplicative constants.

lemma OAI.ClosedSurfaceR4.ExactCorrection.polynomial_scale_smallness line 13

theorem OAI.ClosedSurfaceR4.ExactCorrection.finite_polynomial_scale_selection line 35

Source documentation

The first correction block uses finitely many strict positive powers of its scale. Polynomial geometric losses determine an exponent; the numerical bounds determine only the final parameter threshold.

theorem finite_polynomial_scale_selection {ι : Type*} [Fintype ι]
    (p q : ι → ℝ) (hq : ∀ i, 0 < q i) :
    ∃ μ : ℝ, 1 < μ ∧ ∀ C d : ι → ℝ, (∀ i, 0 ≤ C i) → (∀ i, 0 < d i) →
      ∃ η : ℝ, 0 < η ∧ η ≤ 1 ∧ ∀ z t : ℝ, 0 < z → z < η →
        0 < t → t ≤ z^μ → ∀ i, C i*z^(-p i)*t^(q i) < d i*z^(p i) := by
…