DirectionSmallness.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

One scale-independent tolerance for actual direction recovery

theorem OAI.RegularPointCoordinates.direction_smallness_parameters line 11

Source documentation

A single tolerance controls the two Gram restrictions, the radial matrix error, and the absorption term at every positive physical radius.

theorem direction_smallness_parameters (n : ℕ) (Ca D Q V G : ℝ)
    (hQ : 0 ≤ Q) (hV : 0 ≤ V) (hG : 0 ≤ G) :
    ∃ tau : ℝ, 0 < tau ∧ tau ≤ 1 ∧
      (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * (2 : ℝ) ^ n) * tau) ≤ 1 / 3 ∧
      (n : ℝ) ^ 2 * (((5 / 3 : ℝ) * (8192 : ℝ) ^ n) * tau) ≤ 1 / 2 ∧
      ∀ z E : ℝ, 0 ≤ z → z ≤ tau → 0 ≤ E → E ≤ tau →
        2 * ((n : ℝ) ^ 4 * Real.sqrt (2 * Ca ^ 2 * (D ^ 2 * E + Q * z))) ≤ 1 / 4 ∧
        ∀ s : ℝ, 0 < s →
          (4 * (G / (s / 2048))) * Real.sqrt (V * s ^ 2 * E) ≤ 1 / 2 := by
…

Mentions: OAI.RegularPointCoordinates.tau