tetStep_band

proof body

Tactic-mode proof.

  55  unfold tetStep
  56  refine ⟨?lo, ?hi⟩
  57  · have h : (1.059 : ℝ) ^ 12 < 2 := by norm_num
  58    have hpos : (0 : ℝ) < 1.059 := by norm_num
  59    calc (1.059 : ℝ) = (1.059 ^ 12) ^ ((1 : ℝ) / 12) := by
  60            rw [← Real.rpow_natCast, ← Real.rpow_mul (le_of_lt hpos)]
  61            norm_num
  62      _ < (2 : ℝ) ^ ((1 : ℝ) / 12) := by
  63            apply Real.rpow_lt_rpow (pow_nonneg (le_of_lt hpos) 12) h
  64            norm_num
  65  · have h : (2 : ℝ) < 1.060 ^ 12 := by norm_num
  66    have hpos : (0 : ℝ) < 1.060 := by norm_num
  67    calc (2 : ℝ) ^ ((1 : ℝ) / 12) < (1.060 ^ 12) ^ ((1 : ℝ) / 12) := by
  68            apply Real.rpow_lt_rpow (le_of_lt (by norm_num : (0 : ℝ) < 2)) h
  69            norm_num
  70      _ = (1.060 : ℝ) := by
  71            rw [← Real.rpow_natCast 1.060, ← Real.rpow_mul (le_of_lt hpos)]
  72            norm_num
  73
  74/-- 12-TET step J-cost > 0. -/