divergence_at_zero_direction

formal source

  53  Jcost_pos_of_ne_one x hx hne
  54
  55/-- The unique "nothing" reference: cost is unbounded on (0,∞). -/
  56theorem divergence_at_zero_direction :
  57    ¬ ∃ (C : ℝ), ∀ (ε : ℝ), 0 < ε → Jcost ε ≤ C := by
  58  intro ⟨C, hC⟩
  59  -- Pick ε = 1/(2*(|C|+2)); then J(ε) > |C|+1 > C
  60  -- Actual proof: pick ε = 1/4, then J(1/4) = (1/4-1)²/(2·1/4) = (9/16)/(1/2) = 9/8
  61  -- That only bounds J away from C when C < 9/8.
  62  -- For large C, pick ε = 1/(C+2):
  63  -- J(1/(C+2)) = (1/(C+2)-1)²/(2/(C+2)) = (C+1)²/(C+2)²·(C+2)/2 = (C+1)²/(2(C+2))
  64  -- For C ≥ 0: (C+1)²/(2(C+2)) > C ↔ (C+1)² > 2C(C+2) = 2C²+4C ↔ C²+2C+1 > 2C²+4C ↔ 0 > C²+2C-1
  65  -- This fails for C ≥ 1. Need a better choice. Use ε = 1/(2C+4):
  66  -- J(1/(2C+4)) = (1/(2C+4)-1)²/(2/(2C+4)) = ((2C+3)/(2C+4))²·(2C+4)/2 = (2C+3)²/(2(2C+4))
  67  -- Compare with C: (2C+3)²/(2(2C+4)) > C ↔ (2C+3)² > 2C(2C+4) = 4C²+8C
  68  -- = 4C²+12C+9 > 4C²+8C ↔ 4C+9 > 0, which holds for C > -9/4.
  69  -- For C ≤ -3, J(ε) ≥ 0 > C since C < 0. Done by cases.
  70  -- Use J(1) = 0 to handle C < 0, and a direct computation for C ≥ 0
  71  by_cases hC_neg : C < 0
  72  · linarith [hC 1 one_pos, Jcost_unit0]
  73  push_neg at hC_neg  -- C ≥ 0
  74  -- J(1/(2C+4)) = (2C+3)²/(2(2C+4)) > C for C ≥ 0
  75  have h2C4 : (0 : ℝ) < 2 * C + 4 := by linarith
  76  have hε := hC (1 / (2 * C + 4)) (div_pos one_pos h2C4)
  77  have hJval : Jcost (1 / (2 * C + 4)) = (2 * C + 3) ^ 2 / (2 * (2 * C + 4)) := by
  78    rw [Jcost_eq_sq (by positivity)]
  79    field_simp
  80    ring
  81  rw [hJval] at hε
  82  have hnum : 0 ≤ (2 * C + 3) ^ 2 := sq_nonneg _
  83  -- (2C+3)²/(2(2C+4)) ≤ C ↔ (2C+3)² ≤ 2C(2C+4) = 4C²+8C
  84  -- But (2C+3)² = 4C²+12C+9 > 4C²+8C = 2C(2C+4) for C ≥ 0 (since 4C+9 > 0)
  85  have hrewrite : (2 * C + 3) ^ 2 / (2 * (2 * C + 4)) ≤ C ↔
  86      (2 * C + 3) ^ 2 ≤ C * (2 * (2 * C + 4)) := by