unity_unique_existent

formal source

  86   fun h => ⟨hx, (defect_zero_iff_one hx).mpr h⟩⟩
  87
  88/-- **Unity is Unique Existent**: ∀ x, Exists x ⟺ x = 1. -/
  89theorem unity_unique_existent : ∀ x : ℝ, Exists x ↔ x = 1 := by
  90  intro x
  91  constructor
  92  · intro ⟨hpos, hdef⟩; exact (defect_zero_iff_one hpos).mp hdef
  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)