sub_hi

formal source

  91  sub := sub
  92
  93@[simp] theorem sub_lo (I J : Interval) : (I - J).lo = I.lo - J.hi := rfl
  94@[simp] theorem sub_hi (I J : Interval) : (I - J).hi = I.hi - J.lo := rfl
  95
  96theorem sub_contains_sub {x y : ℝ} {I J : Interval}
  97    (hx : I.contains x) (hy : J.contains y) : (I - J).contains (x - y) := by
  98  constructor
  99  · simp only [sub_lo, Rat.cast_sub]
 100    exact sub_le_sub hx.1 hy.2
 101  · simp only [sub_hi, Rat.cast_sub]
 102    exact sub_le_sub hx.2 hy.1
 103
 104/-- Multiplication for positive intervals -/
 105def mulPos (I J : Interval) (hI : 0 < I.lo) (hJ : 0 < J.lo) : Interval where
 106  lo := I.lo * J.lo
 107  hi := I.hi * J.hi
 108  valid := by
 109    apply mul_le_mul I.valid J.valid
 110    · exact le_of_lt hJ
 111    · linarith [I.valid]
 112
 113theorem mulPos_contains_mul {x y : ℝ} {I J : Interval}
 114    (hIpos : 0 < I.lo) (hJpos : 0 < J.lo)
 115    (hx : I.contains x) (hy : J.contains y) : (mulPos I J hIpos hJpos).contains (x * y) := by
 116  have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hIpos
 117  have hJlo_pos : (0 : ℝ) < J.lo := by exact_mod_cast hJpos
 118  have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx.1
 119  have hy_pos : 0 < y := lt_of_lt_of_le hJlo_pos hy.1
 120  have hIhi_pos : (0 : ℝ) ≤ I.hi := le_trans (le_of_lt hIlo_pos) (by exact_mod_cast I.valid)
 121  constructor
 122  · simp only [mulPos, Rat.cast_mul]
 123    exact mul_le_mul hx.1 hy.1 (le_of_lt hJlo_pos) (le_trans (le_of_lt hIlo_pos) hx.1)
 124  · simp only [mulPos, Rat.cast_mul]