Theorem: isPathConnected_potential_levelset (Ray/Dynamics/Multibrot/Connected.lean)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ IsPathConnected (potential d ⁻¹' {p})
Tactic:
rw [e]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ IsPathConnected (ray d '' sphere 0 p)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ IsPathConnected (ray d '' sphere 0 p)
Tactic:
apply (isPathConnected_sphere p0).image_of_continuousOn
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ ContinuousOn (ray d) (sphere 0 p)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
e : potential d ⁻¹' {p} = ray d '' sphere 0 p
⊢ ContinuousOn (ray d) (sphere 0 p)
Tactic:
exact (rayHolomorphic d).continuousOn.mono (Metric.sphere_subset_ball p1)
State after:
no goals

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
⊢ potential d ⁻¹' {p} = ray d '' sphere 0 p
Tactic:
apply Set.ext
State after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
⊢ ∀ (x : 𝕊), x ∈ potential d ⁻¹' {p} ↔ x ∈ ray d '' sphere 0 p

State before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
⊢ ∀ (x : 𝕊), x ∈ potential d ⁻¹' {p} ↔ x ∈ ray d '' sphere 0 p
Tactic:
intro c
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ c ∈ potential d ⁻¹' {p} ↔ c ∈ ray d '' sphere 0 p

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ c ∈ potential d ⁻¹' {p} ↔ c ∈ ray d '' sphere 0 p
Tactic:
simp only [mem_preimage, mem_singleton_iff, ← abs_bottcher, mem_image, mem_sphere,
  Complex.dist_eq, sub_zero]
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ Complex.abs (bottcher d c) = p ↔ ∃ x, Complex.abs x = p ∧ ray d x = c

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ Complex.abs (bottcher d c) = p ↔ ∃ x, Complex.abs x = p ∧ ray d x = c
Tactic:
constructor
State after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ Complex.abs (bottcher d c) = p → ∃ x, Complex.abs x = p ∧ ray d x = c

case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ (∃ x, Complex.abs x = p ∧ ray d x = c) → Complex.abs (bottcher d c) = p

State before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ Complex.abs (bottcher d c) = p → ∃ x, Complex.abs x = p ∧ ray d x = c
Tactic:
intro h
State after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ ∃ x, Complex.abs x = p ∧ ray d x = c

State before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ ∃ x, Complex.abs x = p ∧ ray d x = c
Tactic:
use bottcher d c
State after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ Complex.abs (bottcher d c) = p ∧ ray d (bottcher d c) = c

State before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ Complex.abs (bottcher d c) = p ∧ ray d (bottcher d c) = c
Tactic:
use h
State after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ ray d (bottcher d c) = c

State before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ ray d (bottcher d c) = c
Tactic:
rw [ray_bottcher]
State after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ c ∈ multibrotExt d

State before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ c ∈ multibrotExt d
Tactic:
rw [← potential_lt_one, ← abs_bottcher, h]
State after:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ p < 1

State before:
case right
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
h : Complex.abs (bottcher d c) = p
⊢ p < 1
Tactic:
exact p1
State after:
no goals

State before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
⊢ (∃ x, Complex.abs x = p ∧ ray d x = c) → Complex.abs (bottcher d c) = p
Tactic:
intro ⟨e, ep, ec⟩
State after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ Complex.abs (bottcher d c) = p

State before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ Complex.abs (bottcher d c) = p
Tactic:
rw [← ec, bottcher_ray]
State after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ Complex.abs e = p

case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ e ∈ ball 0 1

State before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ Complex.abs e = p

case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ e ∈ ball 0 1
Tactic:
exact ep
State after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ e ∈ ball 0 1

State before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
p : ℝ
p0 : 0 ≤ p
p1 : p < 1
c : 𝕊
e : ℂ
ep : Complex.abs e = p
ec : ray d e = c
⊢ e ∈ ball 0 1
Tactic:
simp only [mem_ball, Complex.dist_eq, sub_zero, ep, p1]
State after:
no goals