smulPos

formal source

 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
 136  constructor
 137  · simp only [smulPos, Rat.cast_mul]
 138    exact mul_le_mul_of_nonneg_left hx.1 (le_of_lt hq_pos)
 139  · simp only [smulPos, Rat.cast_mul]
 140    exact mul_le_mul_of_nonneg_left hx.2 (le_of_lt hq_pos)
 141
 142/-- Power by natural number for positive intervals -/
 143def npow (I : Interval) (n : ℕ) (hI : 0 < I.lo) : Interval where
 144  lo := I.lo ^ n
 145  hi := I.hi ^ n
 146  valid := by
 147    apply pow_le_pow_left₀ (le_of_lt hI) I.valid
 148
 149theorem npow_contains_pow {x : ℝ} {I : Interval} {n : ℕ}
 150    (hIpos : 0 < I.lo) (hx : I.contains x) : (npow I n hIpos).contains (x ^ n) := by
 151  have hIlo_pos : (0 : ℝ) < I.lo := by exact_mod_cast hIpos
 152  have hx_pos : 0 < x := lt_of_lt_of_le hIlo_pos hx.1
 153  constructor
 154  · simp only [npow, Rat.cast_pow]
 155    exact pow_le_pow_left₀ (le_of_lt hIlo_pos) hx.1 n
 156  · simp only [npow, Rat.cast_pow]
 157    exact pow_le_pow_left₀ (le_of_lt hx_pos) hx.2 n
 158