cumulativeCooling_zero

formal source

  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
  68structure IdentityTickRefrigeratorCert where
  69  fraction_pos : 0 < coolingFraction
  70  fraction_band : (0.11 : ℝ) < coolingFraction ∧ coolingFraction < 0.13
  71  cumulative_zero : cumulativeCooling 0 = 0
  72  cumulative_succ : ∀ n, cumulativeCooling (n + 1) = cumulativeCooling n + coolingFraction
  73  cumulative_pos : ∀ {n : ℕ}, 1 ≤ n → 0 < cumulativeCooling n
  74  cumulative_strict_mono : ∀ {n m : ℕ}, n < m →
  75    cumulativeCooling n < cumulativeCooling m
  76
  77def identityTickRefrigeratorCert : IdentityTickRefrigeratorCert where
  78  fraction_pos := coolingFraction_pos