defect_one

formal source

  93  · intro h; subst h; exact ⟨one_pos, defect_at_one⟩
  94
  95/-- Alias for `defect_at_one`. -/
  96theorem defect_one : defect 1 = 0 := defect_at_one
  97
  98/-- Defect is strictly positive for x ≠ 1. -/
  99theorem defect_pos_of_ne_one {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) : 0 < defect x := by
 100  have h_nn := defect_nonneg hx
 101  have h_ne_zero : defect x ≠ 0 := fun h => hne ((defect_zero_iff_one hx).mp h)
 102  exact lt_of_le_of_ne h_nn (Ne.symm h_ne_zero)
 103
 104/-! ## Nothing Cannot Exist: J(0) → ∞ -/
 105
 106/-- As x → 0⁺, defect(x) → +∞.
 107
 108Technical proof: J(x) = (x + 1/x)/2 - 1 ≥ 1/(2x) - 1 → +∞ as x → 0⁺. -/
 109theorem defect_tendsto_atTop_at_zero :
 110    Filter.Tendsto defect (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop := by
 111  unfold defect J
 112  -- The proof uses that 1/x → +∞ as x → 0⁺, and (x + 1/x)/2 - 1 ≥ 1/(2x) - 1
 113  have hinv : Filter.Tendsto (fun x : ℝ => x⁻¹) (nhdsWithin 0 (Set.Ioi 0)) Filter.atTop :=
 114    tendsto_inv_nhdsGT_zero
 115  rw [Filter.tendsto_atTop]
 116  intro r
 117  rw [Filter.tendsto_atTop] at hinv
 118  have hev := hinv (2 * (r + 2))
 119  -- On nhdsWithin 0 (Ioi 0), x is positive. Combine with x⁻¹ ≥ 2(r+2)
 120  have hpos : ∀ᶠ x in nhdsWithin (0 : ℝ) (Set.Ioi 0), 0 < x := eventually_mem_nhdsWithin
 121  apply Filter.Eventually.mono (hev.and hpos)
 122  intro x ⟨hinvx, hx0⟩
 123  have h1 : (x + x⁻¹) / 2 - 1 ≥ x⁻¹ / 2 - 1 := by linarith
 124  have h2 : x⁻¹ / 2 - 1 ≥ (2 * (r + 2)) / 2 - 1 := by linarith
 125  linarith
 126