mulPos

formal source

 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]
 125    exact mul_le_mul hx.2 hy.2 (le_of_lt hy_pos) hIhi_pos
 126
 127/-- Scalar multiplication by a positive rational -/
 128def smulPos (q : ℚ) (I : Interval) (hq : 0 < q) : Interval where
 129  lo := q * I.lo
 130  hi := q * I.hi
 131  valid := mul_le_mul_of_nonneg_left I.valid (le_of_lt hq)
 132
 133theorem smulPos_contains_smul {q : ℚ} {x : ℝ} {I : Interval}
 134    (hq : 0 < q) (hx : I.contains x) : (smulPos q I hq).contains ((q : ℝ) * x) := by
 135  have hq_pos : (0 : ℝ) < q := by exact_mod_cast hq