stepCost_nonneg

formal source

  38
  39theorem stepCost_zero_at_just : stepCost 1 = 0 := Cost.Jcost_unit0
  40
  41theorem stepCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ stepCost r :=
  42  Cost.Jcost_nonneg hr
  43
  44/-- JI reference cost (exact integer ratio: J-cost zero). -/
  45def jiCost : ℝ := stepCost 1
  46theorem jiCost_zero : jiCost = 0 := stepCost_zero_at_just
  47
  48/-- 12-TET per-semitone cost approximation: step = 2^(1/12).
  49    Using quadratic form `J(r) = (r-1)²/(2r)`, with `r = 2^(1/12)`.
  50    We use the lower bound `r - 1 > 0.059` and upper bound `r - 1 < 0.060`. -/
  51noncomputable def tetStep : ℝ := 2 ^ ((1 : ℝ) / 12)
  52
  53/-- 12-TET step is in `(1.059, 1.060)`. -/
  54theorem tetStep_band : 1.059 < tetStep ∧ tetStep < 1.060 := by
  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)]