RadialErrorUnits.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform natural units for the actual radial correction error

def OAI.RegularPointCoordinates.radialCorrectionConstant line 11
theorem OAI.RegularPointCoordinates.radialCorrectionConstant_pos line 16

theorem OAI.RegularPointCoordinates.radial_correction_error_units line 25

Source documentation

The scale-dependent span bound and the radius-squared Poincare constant give one uniform coefficient for the complete Poisson defect.

theorem radial_correction_error_units {K epsilon A B J Cχ s κ σ V L : ℝ} {n : ℕ}
    (hs1 : s ≤ 1) (hκ : 0 ≤ κ) (hσ : 0 ≤ σ) (hV : 0 ≤ V)
    (hB : 0 ≤ B) (hJ : 0 ≤ J) (hA : 0 ≤ A) (hε : 0 ≤ epsilon) (hCχ : 0 ≤ Cχ)
    (hL : L = ((n + 2 : ℕ) : ℝ) * max (1 + epsilon) (A * s)) :
    2 * (1 + epsilon) ^ 2 * (σ * (B * s ^ 2)) +
      8 * (annularPoincareConstant K n * (s / 64) ^ 2) * L ^ 2 *
        (4096 * Cχ * (J + B / 2) * σ + κ * A ^ 2 * s ^ 2 * V) ≤
      radialCorrectionConstant K n epsilon A B J Cχ * s ^ 2 * (σ + κ * s ^ 2 * V) := by
…

Mentions: OAI.RegularPointCoordinates.annularPoincareConstant, OAI.RegularPointCoordinates.radialCorrectionConstant