ScaledRegularizer.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A regularizer threshold fixed before the physical radius

theorem OAI.RegularPointCoordinates.exists_scaled_regularizer_threshold line 17

Source documentation

A bound on |lambda| R^2, rather than on lambda, is enough to choose the scale threshold before the radius or regularizer is chosen.

theorem exists_scaled_regularizer_threshold {B Lambda η : ℝ}
    (hB : 0 ≤ B) (hη : 0 < η) :
    ∃ N : ℕ, ∀ (R lambda : ℝ), |lambda| * R ^ 2 ≤ Lambda →
      ∀ k, N ≤ k → ∀ r, 0 ≤ r → (2 : ℝ) ^ k * r ≤ R →
      ∀ T : E →L[ℝ] E, ‖T‖ ^ 2 ≤ B →
        |lambda * r ^ 2| * ‖T‖ ^ 2 * (2 : ℝ) ^ k < η := by
…