theorem
proved
tactic proof
rescaleLength_tendsto_zero
show as:
view Lean formalization →
formal statement (Lean)
102theorem rescaleLength_tendsto_zero (a : ℕ → ℝ) (h : Tendsto a atTop atTop) :
103 Tendsto (rescaleLength a) atTop (nhds 0) := by
proof body
Tactic-mode proof.
104 -- Strategy: for any ε > 0, get N so that runningMax a n > (1/ε)², then
105 -- sqrt(runningMax a n) > 1/ε, hence 1/sqrt(runningMax a n) < ε.
106 have h_max := runningMax_tendsto_atTop a h
107 rw [Metric.tendsto_nhds]
108 intro ε hε
109 have hie_pos : (0 : ℝ) < 1 / ε := by positivity
110 rw [Filter.tendsto_atTop_atTop] at h_max
111 obtain ⟨N, hN⟩ := h_max ((1 / ε) ^ 2 + 1)
112 rw [Filter.eventually_atTop]
113 refine ⟨N, fun n hn => ?_⟩
114 have hrun : (1 / ε) ^ 2 + 1 ≤ runningMax a n := hN n hn
115 have hrun_pos : (0 : ℝ) < runningMax a n := by linarith [sq_nonneg (1 / ε)]
116 have hsqrt_pos : (0 : ℝ) < Real.sqrt (runningMax a n) := Real.sqrt_pos.mpr hrun_pos
117 simp only [rescaleLength, Real.dist_eq, sub_zero,
118 abs_of_pos (div_pos one_pos hsqrt_pos)]
119 rw [div_lt_iff₀ hsqrt_pos]
120 have h_sqrt_bound : 1 / ε < Real.sqrt (runningMax a n) := by
121 rw [← Real.sqrt_sq hie_pos.le]
122 exact Real.sqrt_lt_sqrt (sq_nonneg _) (by linarith)
123 calc (1 : ℝ) = ε * (1 / ε) := by field_simp
124 _ < ε * Real.sqrt (runningMax a n) := by
125 exact mul_lt_mul_of_pos_left h_sqrt_bound hε
126
127/-! ## Properties of the Normalized Ancient Element -/
128
129/-- The normalized vorticity satisfies ‖ω̃ₙ‖ ≤ 1 for all n. -/