residualFraction_strict_anti

formal source

  63  unfold residualFraction
  64  exact pow_lt_one₀ (le_of_lt reductionFactor_pos) reductionFactor_lt_one (by omega)
  65
  66theorem residualFraction_strict_anti {n m : ℕ} (h : n < m) :
  67    residualFraction m < residualFraction n := by
  68  unfold residualFraction
  69  exact pow_lt_pow_right_of_lt_one₀ reductionFactor_pos
  70    reductionFactor_lt_one h
  71
  72theorem residualFraction_succ (n : ℕ) :
  73    residualFraction (n + 1) = residualFraction n * reductionFactor := by
  74  unfold residualFraction
  75  rw [pow_succ]
  76
  77/-! ## §3. Master certificate -/
  78
  79structure IdentityTickBioremediationPilotCert where
  80  factor_pos : 0 < reductionFactor
  81  factor_lt_one : reductionFactor < 1
  82  factor_band : (0.87 : ℝ) < reductionFactor ∧ reductionFactor < 0.89
  83  residual_zero : residualFraction 0 = 1
  84  residual_pos : ∀ n, 0 < residualFraction n
  85  residual_lt_one_pos : ∀ {n : ℕ}, 1 ≤ n → residualFraction n < 1
  86  residual_strict_anti : ∀ {n m : ℕ}, n < m → residualFraction m < residualFraction n
  87  residual_succ : ∀ n, residualFraction (n + 1) = residualFraction n * reductionFactor
  88
  89def identityTickBioremediationPilotCert :
  90    IdentityTickBioremediationPilotCert where
  91  factor_pos := reductionFactor_pos
  92  factor_lt_one := reductionFactor_lt_one
  93  factor_band := reductionFactor_band
  94  residual_zero := residualFraction_zero
  95  residual_pos := residualFraction_pos
  96  residual_lt_one_pos := @residualFraction_lt_one_of_pos