reductionFactor_pos

formal source

  32/-- The J-cost reduction factor: `1 - J(φ) = 1 - (φ - 3/2) = 5/2 - φ`. -/
  33def reductionFactor : ℝ := 5/2 - phi
  34
  35theorem reductionFactor_pos : 0 < reductionFactor := by
  36  unfold reductionFactor
  37  have := phi_lt_onePointSixTwo; linarith
  38
  39theorem reductionFactor_lt_one : reductionFactor < 1 := by
  40  unfold reductionFactor
  41  have := phi_gt_onePointFive; linarith
  42
  43theorem reductionFactor_band :
  44    (0.87 : ℝ) < reductionFactor ∧ reductionFactor < 0.89 := by
  45  unfold reductionFactor
  46  have h1 := phi_gt_onePointSixOne
  47  have h2 := phi_lt_onePointSixTwo
  48  refine ⟨by linarith, by linarith⟩
  49
  50/-! ## §2. Residual fraction after n cycles -/
  51
  52/-- Residual contaminant fraction after `n` cycles. -/
  53def residualFraction (n : ℕ) : ℝ := reductionFactor ^ n
  54
  55theorem residualFraction_zero : residualFraction 0 = 1 := by
  56  unfold residualFraction; simp
  57
  58theorem residualFraction_pos (n : ℕ) : 0 < residualFraction n :=
  59  pow_pos reductionFactor_pos _
  60
  61theorem residualFraction_lt_one_of_pos {n : ℕ} (h : 1 ≤ n) :
  62    residualFraction n < 1 := by
  63  unfold residualFraction
  64  exact pow_lt_one₀ (le_of_lt reductionFactor_pos) reductionFactor_lt_one (by omega)
  65