npow_contains_pow

formal source

 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
 159/-! ## Bounds Checking -/
 160
 161/-- If b < I.lo, then all x in I satisfy b < x -/
 162theorem lo_gt_implies_contains_gt {I : Interval} {b : ℚ} (h : b < I.lo) {x : ℝ}
 163    (hx : I.contains x) : (b : ℝ) < x :=
 164  lt_of_lt_of_le (by exact_mod_cast h) hx.1
 165
 166/-- If I.hi < b, then all x in I satisfy x < b -/
 167theorem hi_lt_implies_contains_lt {I : Interval} {b : ℚ} (h : I.hi < b) {x : ℝ}
 168    (hx : I.contains x) : x < (b : ℝ) :=
 169  lt_of_le_of_lt hx.2 (by exact_mod_cast h)
 170
 171/-- If b ≤ I.lo, then all x in I satisfy b ≤ x -/
 172theorem lo_ge_implies_contains_ge {I : Interval} {b : ℚ} (h : b ≤ I.lo) {x : ℝ}
 173    (hx : I.contains x) : (b : ℝ) ≤ x :=
 174  le_trans (by exact_mod_cast h) hx.1
 175
 176/-- If I.hi ≤ b, then all x in I satisfy x ≤ b -/
 177theorem hi_le_implies_contains_le {I : Interval} {b : ℚ} (h : I.hi ≤ b) {x : ℝ}
 178    (hx : I.contains x) : x ≤ (b : ℝ) :=
 179  le_trans hx.2 (by exact_mod_cast h)