c_RS

formal source

 103def correctionFactor : ℝ := 1 - phi ^ (-8 : ℤ)
 104
 105/-- The two-sided 8-tick washout prefactor: `c_RS = (1 − φ^(−8))^2`. -/
 106def c_RS : ℝ := correctionFactor ^ 2
 107
 108theorem c_RS_expanded : c_RS = (1 - phi ^ (-8 : ℤ)) ^ 2 := by
 109  unfold c_RS correctionFactor
 110
 111theorem one_minus_phi_neg8_lower : (1 - phi ^ (-8 : ℤ)) > 0.978 := by
 112  have h := phi_zpow_neg8_upper
 113  linarith
 114
 115theorem one_minus_phi_neg8_upper : (1 - phi ^ (-8 : ℤ)) < 0.979 := by
 116  have h := phi_zpow_neg8_lower
 117  linarith
 118
 119theorem c_RS_pos : 0 < c_RS := by
 120  unfold c_RS correctionFactor
 121  have h := one_minus_phi_neg8_lower
 122  positivity
 123
 124theorem c_RS_lt_one : c_RS < 1 := by
 125  rw [c_RS_expanded]
 126  have hl : (1 - phi ^ (-8 : ℤ)) > 0.978 := one_minus_phi_neg8_lower
 127  have hu : (1 - phi ^ (-8 : ℤ)) < 0.979 := one_minus_phi_neg8_upper
 128  nlinarith [hl, hu]
 129
 130/-- `c_RS > 0.956`. -/
 131theorem c_RS_lower : c_RS > 0.956 := by
 132  rw [c_RS_expanded]
 133  have hl : (1 - phi ^ (-8 : ℤ)) > 0.978 := one_minus_phi_neg8_lower
 134  have hu : (1 - phi ^ (-8 : ℤ)) < 0.979 := one_minus_phi_neg8_upper
 135  nlinarith [hl, hu]
 136