continuous_no_isolated_zero_defect

formal source

 323
 324    Note: The actual proof requires the intermediate value theorem and connectedness.
 325    We use ℝ as the configuration space for concreteness. -/
 326theorem continuous_no_isolated_zero_defect :
 327    ∀ x : ℝ, 0 < x → defect x = 0 →
 328    ∀ ε > 0, ∃ z : ℝ, z ≠ x ∧ |z - x| < ε ∧ defect z < ε := by
 329  intro x hx_pos hx ε hε
 330  -- Since defect = 0 implies x = 1, we work at x = 1
 331  have hx_eq_1 : x = 1 := (defect_zero_iff_one hx_pos).mp hx
 332  subst hx_eq_1
 333  -- Take z = 1 + min(ε/2, 1/2) to ensure z > 0 and close to 1
 334  let t := min (ε / 2) (1 / 2 : ℝ)
 335  have ht_pos : t > 0 := by positivity
 336  have ht_le_half : t ≤ 1 / 2 := min_le_right _ _
 337  use 1 + t
 338  constructor
 339  · linarith
 340  constructor
 341  · simp only [add_sub_cancel_left, abs_of_pos ht_pos]
 342    calc t ≤ ε / 2 := min_le_left _ _
 343      _ < ε := by linarith
 344  · -- defect(1 + t) = J(1 + t) = t²/(2(1+t)) for small t > 0
 345    -- For t ≤ min(ε/2, 1/2), we show this is less than ε
 346    simp only [defect, J]
 347    have ht_pos' : 1 + t > 0 := by linarith
 348    have hne : 1 + t ≠ 0 := ht_pos'.ne'
 349    -- Compute J(1+t) = ((1+t) + (1+t)⁻¹)/2 - 1 = t²/(2(1+t))
 350    have key : (1 + t + (1 + t)⁻¹) / 2 - 1 = t^2 / (2 * (1 + t)) := by
 351      field_simp
 352      ring
 353    rw [key]
 354    -- Now show t²/(2(1+t)) < ε
 355    have h1t_ge1 : 1 + t ≥ 1 := by linarith
 356    have h2 : 2 * (1 + t) ≥ 2 := by linarith