coolingFraction_band

formal source

  34  unfold coolingFraction
  35  have := phi_gt_onePointFive; linarith
  36
  37theorem coolingFraction_band :
  38    (0.11 : ℝ) < coolingFraction ∧ coolingFraction < 0.13 := by
  39  unfold coolingFraction
  40  have h1 := phi_gt_onePointSixOne
  41  have h2 := phi_lt_onePointSixTwo
  42  refine ⟨by linarith, by linarith⟩
  43
  44/-- Cumulative cooling after `n` cycles (in cooling-fraction units of
  45`k_B · T_bath`). -/
  46def cumulativeCooling (n : ℕ) : ℝ := (n : ℝ) * coolingFraction
  47
  48theorem cumulativeCooling_zero : cumulativeCooling 0 = 0 := by
  49  unfold cumulativeCooling; simp
  50
  51theorem cumulativeCooling_succ (n : ℕ) :
  52    cumulativeCooling (n + 1) = cumulativeCooling n + coolingFraction := by
  53  unfold cumulativeCooling; push_cast; ring
  54
  55theorem cumulativeCooling_pos {n : ℕ} (h : 1 ≤ n) :
  56    0 < cumulativeCooling n := by
  57  unfold cumulativeCooling
  58  exact mul_pos (by exact_mod_cast (by omega : 0 < n)) coolingFraction_pos
  59
  60theorem cumulativeCooling_strict_mono {n m : ℕ} (h : n < m) :
  61    cumulativeCooling n < cumulativeCooling m := by
  62  unfold cumulativeCooling
  63  have h_real : (n : ℝ) < (m : ℝ) := by exact_mod_cast h
  64  exact (mul_lt_mul_iff_of_pos_right coolingFraction_pos).mpr h_real
  65
  66/-! ## §2. Master certificate -/
  67