pith. machine review for the scientific record. sign in
def definition def or abbrev

regge_riemann_convergence_axiom

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  89def regge_riemann_convergence_axiom : Prop :=

proof body

Definition body.

  90  ∀ (R_component : ℝ) (a : ℝ), 0 < a → a < 1 →
  91    ∃ (holonomy_deviation : ℝ) (C : ℝ), 0 < C ∧
  92      |holonomy_deviation - a ^ 2 * R_component| ≤ C * a ^ 4
  93
  94/-! ## Convergence Rate -/
  95
  96/-- The convergence rate is second order: error = O(a^2).
  97    This means halving the mesh size quarters the error. -/

depends on (4)

Lean names referenced from this declaration's body.