pith. machine review for the scientific record. sign in
theorem proved tactic proof

abs_deviation_small

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)

  76theorem abs_deviation_small {r : ℝ} (hr : 0 < r) {δ : ℝ} (hδ : 0 ≤ δ)
  77    (hδ_small : δ ≤ 1) (hJ : Jcost r ≤ δ) :
  78    |r - 1| ≤ Real.sqrt (8 * δ) := by

proof body

Tactic-mode proof.

  79  have hsq := edge_deviation_small hr hδ hδ_small hJ
  80  have h8δ_nn : 0 ≤ 8 * δ := by nlinarith
  81  rw [← Real.sqrt_sq (abs_nonneg (r - 1))]
  82  apply Real.sqrt_le_sqrt
  83  rw [sq_abs]
  84  exact hsq
  85
  86/-! ## Part 2: Exact Case Recovery -/
  87
  88/-- **EXACT CASE RECOVERY**: When δ = 0, approximate holography recovers
  89    exact holography (GCIC rigidity). -/

depends on (1)

Lean names referenced from this declaration's body.