Theorem: dene_anti (Ray/Dynamics/Multibrot/Potential.lean)

State before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
⊢ dene x ≥ dene y
Tactic:
refine Real.exp_le_exp.mpr ?_
State after:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
⊢ y - y.exp ≤ x - x.exp

State before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
a : AntitoneOn (fun x => x - x.exp) (Ici 0)
⊢ y - y.exp ≤ x - x.exp
Tactic:
exact a x0 (le_trans x0 xy) xy
State after:
no goals

State before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)
Tactic:
have hd : ∀ x, HasDerivAt (fun x ↦ x - exp x) (1 - exp x) x :=
  fun x ↦ (hasDerivAt_id x).sub (Real.hasDerivAt_exp x)
State after:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)

State before:
c z : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)
Tactic:
have d : Differentiable ℝ (fun x ↦ x - exp x) := fun x ↦ (hd x).differentiableAt
State after:
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)

State before:
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ AntitoneOn (fun x => x - x.exp) (Ici 0)
Tactic:
apply antitoneOn_of_deriv_nonpos (convex_Ici _)
State after:
case hf
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ ContinuousOn (fun x => x - x.exp) (Ici 0)

case hf'
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ DifferentiableOn ℝ (fun x => x - x.exp) (interior (Ici 0))

case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ ∀ x ∈ interior (Ici 0), deriv (fun x => x - x.exp) x ≤ 0

State before:
case hf
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ ContinuousOn (fun x => x - x.exp) (Ici 0)
Tactic:
exact d.continuous.continuousOn
State after:
no goals

State before:
case hf'
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ DifferentiableOn ℝ (fun x => x - x.exp) (interior (Ici 0))
Tactic:
exact d.differentiableOn
State after:
no goals

State before:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x y : ℝ
x0 : 0 ≤ x
xy : x ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
⊢ ∀ x ∈ interior (Ici 0), deriv (fun x => x - x.exp) x ≤ 0
Tactic:
intro x m
State after:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x✝ y : ℝ
x0 : 0 ≤ x✝
xy : x✝ ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
x : ℝ
m : x ∈ interior (Ici 0)
⊢ deriv (fun x => x - x.exp) x ≤ 0

State before:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x✝ y : ℝ
x0 : 0 ≤ x✝
xy : x✝ ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
x : ℝ
m : x ∈ interior (Ici 0)
⊢ deriv (fun x => x - x.exp) x ≤ 0
Tactic:
simp only [nonempty_Iio, interior_Ici', mem_Ioi] at m
State after:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x✝ y : ℝ
x0 : 0 ≤ x✝
xy : x✝ ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
x : ℝ
m : 0 < x
⊢ deriv (fun x => x - x.exp) x ≤ 0

State before:
case hf'_nonpos
c z : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
x✝ y : ℝ
x0 : 0 ≤ x✝
xy : x✝ ≤ y
hd : ∀ (x : ℝ), HasDerivAt (fun x => x - x.exp) (1 - x.exp) x
d : Differentiable ℝ fun x => x - x.exp
x : ℝ
m : 0 < x
⊢ deriv (fun x => x - x.exp) x ≤ 0
Tactic:
simp only [(hd x).deriv, sub_nonpos, Real.one_le_exp m.le]
State after:
no goals