f_RG_upper

formal source

  44def f_RG_lower (f : Fermion) : ℚ := f_RG_certified f - f_RG_tolerance
  45
  46/-- Upper endpoint of the certified enclosure interval. -/
  47def f_RG_upper (f : Fermion) : ℚ := f_RG_certified f + f_RG_tolerance
  48
  49theorem f_RG_tolerance_nonneg : (0 : ℚ) ≤ f_RG_tolerance := by
  50  norm_num [f_RG_tolerance]
  51
  52theorem f_RG_interval_nonempty (f : Fermion) : f_RG_lower f ≤ f_RG_upper f := by
  53  unfold f_RG_lower f_RG_upper
  54  nlinarith [f_RG_tolerance_nonneg]
  55
  56/-- Equivalent absolute-error enclosure form for certified transport values. -/
  57theorem is_certified_iff_abs_error_le (f : Fermion) (val : ℝ) :
  58    is_certified f val ↔
  59      |val - (f_RG_certified f : ℝ)| ≤ (f_RG_tolerance : ℝ) := by
  60  constructor
  61  · intro h
  62    rcases h with ⟨hlo, hhi⟩
  63    have h1 : -((f_RG_tolerance : ℚ) : ℝ) ≤ val - (f_RG_certified f : ℚ) := by
  64      linarith
  65    have h2 : val - (f_RG_certified f : ℚ) ≤ ((f_RG_tolerance : ℚ) : ℝ) := by
  66      linarith
  67    exact abs_le.mpr ⟨h1, h2⟩
  68  · intro h
  69    have h' := abs_le.mp h
  70    constructor <;> linarith [h'.1, h'.2]
  71
  72/-- The certified center value is enclosed for every fermion. -/
  73theorem certified_center_enclosed (f : Fermion) :
  74    is_certified f (f_RG_certified f) := by
  75  unfold is_certified
  76  have htol_nonneg : (0 : ℝ) ≤ (f_RG_tolerance : ℝ) := by
  77    exact_mod_cast f_RG_tolerance_nonneg