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

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ potential d c < 1 ↔ c ∈ multibrotExt d
Tactic:
set s := superF d
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
s : Super (f d) d ∞ := superF d
⊢ potential d c < 1 ↔ c ∈ multibrotExt d

State before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
s : Super (f d) d ∞ := superF d
⊢ potential d c < 1 ↔ c ∈ multibrotExt d
Tactic:
induction c using OnePoint.rec
State after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ potential d ∞ < 1 ↔ ∞ ∈ multibrotExt d

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ potential d ↑x✝ < 1 ↔ ↑x✝ ∈ multibrotExt d

State before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ potential d ∞ < 1 ↔ ∞ ∈ multibrotExt d
Tactic:
simp only [potential, bottcher, fill_inf, zero_lt_one, multibrotExt_inf]
State after:
no goals

State before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ potential d ↑x✝ < 1 ↔ ↑x✝ ∈ multibrotExt d
Tactic:
constructor
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ potential d ↑x✝ < 1 → ↑x✝ ∈ multibrotExt d

case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ ↑x✝ ∈ multibrotExt d → potential d ↑x✝ < 1

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ potential d ↑x✝ < 1 → ↑x✝ ∈ multibrotExt d
Tactic:
intro h
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : potential d ↑x✝ < 1
⊢ ↑x✝ ∈ multibrotExt d

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : potential d ↑x✝ < 1
⊢ ↑x✝ ∈ multibrotExt d
Tactic:
contrapose h
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ↑x✝ ∉ multibrotExt d
⊢ ¬potential d ↑x✝ < 1

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ↑x✝ ∉ multibrotExt d
⊢ ¬potential d ↑x✝ < 1
Tactic:
simp only [not_not, not_lt, multibrot_basin', potential, fill_coe, Super.basin,
  mem_setOf, not_exists, multibrotExt_coe] at h ⊢
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ∀ (x : ℕ), (x✝, (f d x✝)^[x] ↑x✝) ∉ ⋯.near
⊢ 1 ≤ ⋯.potential x✝ ↑x✝

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ∀ (x : ℕ), (x✝, (f d x✝)^[x] ↑x✝) ∉ ⋯.near
⊢ 1 ≤ ⋯.potential x✝ ↑x✝
Tactic:
rw [s.potential_eq_one]
State after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ∀ (x : ℕ), (x✝, (f d x✝)^[x] ↑x✝) ∉ ⋯.near
⊢ ∀ (n : ℕ), (x✝, (f d x✝)^[n] ↑x✝) ∉ s.near

State before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ∀ (x : ℕ), (x✝, (f d x✝)^[x] ↑x✝) ∉ ⋯.near
⊢ ∀ (n : ℕ), (x✝, (f d x✝)^[n] ↑x✝) ∉ s.near
Tactic:
exact h
State after:
no goals

State before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ ↑x✝ ∈ multibrotExt d → potential d ↑x✝ < 1
Tactic:
intro m
State after:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ potential d ↑x✝ < 1

State before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ potential d ↑x✝ < 1
Tactic:
rw [← abs_bottcher]
State after:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ Complex.abs (bottcher d ↑x✝) < 1

State before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ Complex.abs (bottcher d ↑x✝) < 1
Tactic:
simp only [bottcher, fill_coe]
State after:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ Complex.abs (bottcher' d x✝) < 1

State before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ Complex.abs (bottcher' d x✝) < 1
Tactic:
simp only [multibrotExt_coe] at m
State after:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ Complex.abs (bottcher' d x✝) < 1

State before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ Complex.abs (bottcher' d x✝) < 1
Tactic:
exact s.bottcher_lt_one (multibrotPost m)
State after:
no goals