SharpNeighborhoodParameters.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Choosing the simultaneous smallness parameters for sharp projection

theorem OAI.RegularPointCoordinates.sharp_neighborhood_parameters line 11

Source documentation

One positive choice satisfies the coordinate, source, and curvature requirements, while making the two-center square budget arbitrarily small.

theorem sharp_neighborhood_parameters {epsilon delta tau c g a K budget : ℝ}
    (hepsilon : 0 < epsilon) (hdelta : 0 < delta) (htau : 0 < tau)
    (hc : 0 ≤ c) (hg : 0 ≤ g) (ha : 0 ≤ a) (hbudget : 0 < budget) :
    ∃ zeta eta cap : ℝ, 0 < zeta ∧ 0 < eta ∧ 0 < cap ∧
      zeta ≤ epsilon ∧ zeta ≤ delta ∧ c * zeta ≤ 1 ∧ g * zeta ≤ 1 / 64 ∧
      eta ≤ tau ∧ 128 * (a * zeta + eta) ≤ budget ∧ |K| * cap ^ 2 ≤ delta / 32 := by
…

Mentions: OAI.RegularPointCoordinates.tau