add

formal source

  43/-! ## Interval Arithmetic Operations -/
  44
  45/-- Addition of intervals: [a,b] + [c,d] = [a+c, b+d] -/
  46def add (I J : Interval) : Interval where
  47  lo := I.lo + J.lo
  48  hi := I.hi + J.hi
  49  valid := add_le_add I.valid J.valid
  50
  51instance : Add Interval where
  52  add := add
  53
  54@[simp] theorem add_lo (I J : Interval) : (I + J).lo = I.lo + J.lo := rfl
  55@[simp] theorem add_hi (I J : Interval) : (I + J).hi = I.hi + J.hi := rfl
  56
  57theorem add_contains_add {x y : ℝ} {I J : Interval}
  58    (hx : I.contains x) (hy : J.contains y) : (I + J).contains (x + y) := by
  59  constructor
  60  · simp only [add_lo, Rat.cast_add]
  61    exact add_le_add hx.1 hy.1
  62  · simp only [add_hi, Rat.cast_add]
  63    exact add_le_add hx.2 hy.2
  64
  65/-- Negation of intervals: -[a,b] = [-b, -a] -/
  66def neg (I : Interval) : Interval where
  67  lo := -I.hi
  68  hi := -I.lo
  69  valid := neg_le_neg I.valid
  70
  71instance : Neg Interval where
  72  neg := neg
  73
  74@[simp] theorem neg_lo (I : Interval) : (-I).lo = -I.hi := rfl
  75@[simp] theorem neg_hi (I : Interval) : (-I).hi = -I.lo := rfl
  76