E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ gronwallBound δ K ε (x - a)
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x ≤ gronwallBound δ K ε (x - a)
intro x hx
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ gronwallBound δ K ε (x - a)
change f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε
case convert_2
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ ε ∈ closure (Ioi ε)

case convert_3
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ ContinuousWithinAt (fun y => gronwallBound δ K y (x - a)) (Ioi ε) ε
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε
convert continuousWithinAt_const.closure_le _ _ (H x hx)
no goals
case convert_3
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ ContinuousWithinAt (fun y => gronwallBound δ K y (x - a)) (Ioi ε) ε
exact (gronwallBound_continuous_ε δ K (x - a)).continuousWithinAt
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ f x ≤ gronwallBound δ K ε' (x - a)
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
⊢ ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
intro x hx ε' hε'
case ha
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ f a ≤ gronwallBound δ K ε' (a - a)

case hB
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ∀ (x : ℝ), HasDerivAt (fun x => gronwallBound δ K ε' (x - a)) (?m.35638 x) x

case bound
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ∀ (x : ℝ), x ∈ Ico a b → f x = gronwallBound δ K ε' (x - a) → f' x < ?m.35638 x

case a
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ x ∈ Icc a b

E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ℝ → ℝ
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ f x ≤ gronwallBound δ K ε' (x - a)
apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
no goals
case ha
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ f a ≤ gronwallBound δ K ε' (a - a)
rwa [sub_self, gronwallBound_x0]
no goals
case hB
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ∀ (x : ℝ), HasDerivAt (fun x => gronwallBound δ K ε' (x - a)) (?m.35638 x) x
exact fun x => hasDerivAt_gronwallBound_shift δ K ε' x a
case bound
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ f' x < K * gronwallBound δ K ε' (x - a) + ε'
case bound
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ∀ (x : ℝ), x ∈ Ico a b → f x = gronwallBound δ K ε' (x - a) → f' x < K * gronwallBound δ K ε' (x - a) + ε'
intro x hx hfB
case bound
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ f' x < K * f x + ε'
case bound
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ f' x < K * gronwallBound δ K ε' (x - a) + ε'
rw [← hfB]
case bound
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ K * f x + ε < K * f x + ε'
case bound
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ f' x < K * f x + ε'
apply lt_of_le_of_lt (bound x hx)
no goals
case bound
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ K * f x + ε < K * f x + ε'
exact add_lt_add_left (mem_Ioi.1 hε') _
no goals
case a
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ x ∈ Icc a b
exact hx
no goals
case convert_2
E : Type ?u.34313
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.34409
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ ε ∈ closure (Ioi ε)
simp only [closure_Ioi, left_mem_Ici]