Theorem: weak_to_strong_small (Ray/Misc/Bounds.lean)

State before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
⊢ Complex.abs (f z) ≤ c * Complex.abs z
Tactic:
by_cases nz : z = 0
State after:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs (f z) ≤ c * Complex.abs z

case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
⊢ Complex.abs (f z) ≤ c * Complex.abs z

State before:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
⊢ Complex.abs (f z) ≤ c * Complex.abs z
Tactic:
apply le_of_forall_small_le_add zero_lt_one
State after:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
⊢ ∀ (e : ℝ), 0 < e → e < 1 → Complex.abs (f z) ≤ c * Complex.abs z + e

State before:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
⊢ ∀ (e : ℝ), 0 < e → e < 1 → Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
intro e ep _
State after:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e

State before:
case neg
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
rcases Metric.continuous_near fc rp e ep with ⟨s,sp,_,sc⟩
State after:
case neg.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e

State before:
case neg.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
rcases slightly_smaller nz sp with ⟨w,wz,awz⟩
State after:
case neg.intro.intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e

State before:
case neg.intro.intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
have wr : abs w < r := lt_of_lt_of_le awz zr
State after:
case neg.intro.intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e

State before:
case neg.intro.intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f z) ≤ c * Complex.abs z + e
Tactic:
calc abs (f z) = abs (f w - (f w - f z)) := by ring_nf
  _ ≤ abs (f w) + abs (f w - f z) := by bound
  _ ≤ c * abs w + e := by bound [h w wr, sc wz]
  _ ≤ c * abs z + e := by bound
State after:
no goals

State before:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs (f z) ≤ c * Complex.abs z
Tactic:
refine h z ?_
State after:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs z < r

State before:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs z < r
Tactic:
rw [nz]
State after:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs 0 < r

State before:
case pos
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : z = 0
⊢ Complex.abs 0 < r
Tactic:
simpa
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f z) = Complex.abs (f w - (f w - f z))
Tactic:
ring_nf
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f w - (f w - f z)) ≤ Complex.abs (f w) + Complex.abs (f w - f z)
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ Complex.abs (f w) + Complex.abs (f w - f z) ≤ c * Complex.abs w + e
Tactic:
bound [h w wr, sc wz]
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
r c : ℝ
rp : r > 0
cp : c > 0
zr : Complex.abs z ≤ r
fc : ContinuousAt f z
h : ∀ (z : ℂ), Complex.abs z < r → Complex.abs (f z) ≤ c * Complex.abs z
nz : ¬z = 0
e : ℝ
ep : 0 < e
a✝ : e < 1
s : ℝ
sp : 0 < s
left✝ : s ≤ r
sc : ∀ {w : ℂ}, Complex.abs (w - z) < s → Complex.abs (f w - f z) < e
w : ℂ
wz : Complex.abs (w - z) < s
awz : Complex.abs w < Complex.abs z
wr : Complex.abs w < r
⊢ c * Complex.abs w + e ≤ c * Complex.abs z + e
Tactic:
bound
State after:
no goals