Theorem: multibrot_eq_le_two (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ multibrot d = ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2
Tactic:
apply Set.ext
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℂ), x ∈ multibrot d ↔ x ∈ ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℂ), x ∈ multibrot d ↔ x ∈ ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2
Tactic:
intro c
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d ↔ c ∈ ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d ↔ c ∈ ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2
Tactic:
simp only [mem_iInter, mem_preimage, mem_closedBall, Complex.dist_eq, sub_zero]
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d ↔ ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d ↔ ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
Tactic:
constructor
State after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2

case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2) → c ∈ multibrot d

State before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
Tactic:
intro m n
State after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
n : ℕ
⊢ Complex.abs ((f' d c)^[n] c) ≤ 2

State before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
n : ℕ
⊢ Complex.abs ((f' d c)^[n] c) ≤ 2
Tactic:
contrapose m
State after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
m : ¬Complex.abs ((f' d c)^[n] c) ≤ 2
⊢ c ∉ multibrot d

State before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
m : ¬Complex.abs ((f' d c)^[n] c) ≤ 2
⊢ c ∉ multibrot d
Tactic:
simp only [not_le] at m
State after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
m : 2 < Complex.abs ((f' d c)^[n] c)
⊢ c ∉ multibrot d

State before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
m : 2 < Complex.abs ((f' d c)^[n] c)
⊢ c ∉ multibrot d
Tactic:
exact not_multibrot_of_two_lt m
State after:
no goals

State before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2) → c ∈ multibrot d
Tactic:
intro h
State after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
⊢ c ∈ multibrot d

State before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
⊢ c ∈ multibrot d
Tactic:
contrapose h
State after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : c ∉ multibrot d
⊢ ¬∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2

State before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : c ∉ multibrot d
⊢ ¬∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
Tactic:
simp only [multibrot_coe, tendsto_atInf_iff_norm_tendsto_atTop, Complex.norm_eq_abs,
  not_not, not_forall, not_le, Filter.tendsto_atTop, not_exists] at h ⊢
State after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
⊢ ∃ x, 2 < Complex.abs ((f' d c)^[x] c)

State before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
⊢ ∃ x, 2 < Complex.abs ((f' d c)^[x] c)
Tactic:
rcases(h 3).exists with ⟨n, h⟩
State after:
case h.mpr.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h✝ : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
n : ℕ
h : 3 ≤ Complex.abs ((f' d c)^[n] c)
⊢ ∃ x, 2 < Complex.abs ((f' d c)^[x] c)

State before:
case h.mpr.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h✝ : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
n : ℕ
h : 3 ≤ Complex.abs ((f' d c)^[n] c)
⊢ ∃ x, 2 < Complex.abs ((f' d c)^[x] c)
Tactic:
use n
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h✝ : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
n : ℕ
h : 3 ≤ Complex.abs ((f' d c)^[n] c)
⊢ 2 < Complex.abs ((f' d c)^[n] c)

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h✝ : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
n : ℕ
h : 3 ≤ Complex.abs ((f' d c)^[n] c)
⊢ 2 < Complex.abs ((f' d c)^[n] c)
Tactic:
linarith
State after:
no goals