edge_deviation_bound

formal source

  56  nlinarith [sq_nonneg δ]
  57
  58/-- **EDGE DEVIATION BOUND**: If J(r) ≤ δ for r > 0, then (r-1)² ≤ 4δ(1+δ). -/
  59theorem edge_deviation_bound {r : ℝ} (hr : 0 < r) {δ : ℝ} (hδ : 0 ≤ δ)
  60    (hJ : Jcost r ≤ δ) : (r - 1) ^ 2 ≤ 4 * δ * (1 + δ) := by
  61  have hsq := sq_deviation_le_of_Jcost_le hr hδ hJ
  62  have hub := upper_bound_of_Jcost_le hr hδ hJ
  63  calc (r - 1) ^ 2 ≤ 2 * r * δ := hsq
  64    _ ≤ 2 * (2 + 2 * δ) * δ := by nlinarith
  65    _ = 4 * δ * (1 + δ) := by ring
  66
  67/-- For small δ (≤ 1), the edge deviation simplifies to (r-1)² ≤ 8δ. -/
  68theorem edge_deviation_small {r : ℝ} (hr : 0 < r) {δ : ℝ} (hδ : 0 ≤ δ)
  69    (hδ_small : δ ≤ 1) (hJ : Jcost r ≤ δ) : (r - 1) ^ 2 ≤ 8 * δ := by
  70  have h := edge_deviation_bound hr hδ hJ
  71  calc (r - 1) ^ 2 ≤ 4 * δ * (1 + δ) := h
  72    _ ≤ 4 * δ * (1 + 1) := by nlinarith
  73    _ = 8 * δ := by ring
  74
  75/-- Absolute deviation bound: |r - 1| ≤ √(8δ) for δ ≤ 1. -/
  76theorem abs_deviation_small {r : ℝ} (hr : 0 < r) {δ : ℝ} (hδ : 0 ≤ δ)
  77    (hδ_small : δ ≤ 1) (hJ : Jcost r ≤ δ) :
  78    |r - 1| ≤ Real.sqrt (8 * δ) := by
  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). -/