case pos
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x

case neg
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
⊢ Continuous fun ε => gronwallBound δ K ε x
by_cases hK : K = 0
case pos
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => δ + ε * x
case pos
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x
simp only [gronwallBound_K0, hK]
no goals
case pos
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => δ + ε * x
exact continuous_const.add (continuous_id.mul continuous_const)
case neg
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => δ * exp (K * x) + ε / K * (exp (K * x) - 1)
case neg
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x
simp only [gronwallBound_of_K_ne_0 hK]
no goals
case neg
E : Type ?u.31491
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.31587
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => δ * exp (K * x) + ε / K * (exp (K * x) - 1)
exact continuous_const.add ((continuous_id.mul continuous_const).mul continuous_const)