theorem
proved
tactic proof
rungPhaseDelay_band
show as:
view Lean formalization →
formal statement (Lean)
109theorem rungPhaseDelay_band :
110 (0.30 : ℝ) < rungPhaseDelay ∧ rungPhaseDelay < 0.70 := by
proof body
Tactic-mode proof.
111 unfold rungPhaseDelay
112 refine ⟨?_, ?_⟩
113 · -- log φ > 0.30: from 2 log φ = log (phi^2) > log 2.5 > log 2 > 0.6931
114 have hsq : (2 : ℝ) < phi ^ 2 := by
115 have hb := phi_squared_bounds
116 linarith
117 have hlog : Real.log 2 < Real.log (phi ^ 2) :=
118 Real.log_lt_log (by norm_num) hsq
119 rw [Real.log_pow] at hlog
120 push_cast at hlog
121 have hlog2 : (0.69 : ℝ) < Real.log 2 := by
122 have := Real.log_two_gt_d9
123 linarith
124 linarith
125 · -- log φ < 0.70: from φ < 2 ⇒ log φ < log 2 < 0.6932
126 have h1 : Real.log phi < Real.log 2 :=
127 Real.log_lt_log phi_pos phi_lt_two
128 have h2 : Real.log 2 < (0.6932 : ℝ) := by
129 have := Real.log_two_lt_d9
130 linarith
131 linarith
132
133/-- RS echo delay for a bounce at radius `r_min`: `Δt = 2 r_min log φ`. -/