Theorem: approx_bad_potential_image (Ray/Render/Mandelbrot.lean)

State before:
c : ℚ × ℚ
n : ℕ
r : Floating
⊢ potential_image ↑c ∈ approx (bad_potential_image n r c)
Tactic:
rw [potential_image, bad_potential_image]
State after:
c : ℚ × ℚ
n : ℕ
r : Floating
⊢ (let p := potential 2 ↑↑c;
    let t := p ^ 16;
    lerp t ↑clear ↑outside) ∈
    approx
      (let c := Box.ofRat c;
      let p := c.potential c n r;
      let t := p.1.sqr.sqr.sqr.sqr;
      let i := lerp t clear' outside';
      i.quantize)

State before:
c : ℚ × ℚ
n : ℕ
r : Floating
⊢ (let p := potential 2 ↑↑c;
    let t := p ^ 16;
    lerp t ↑clear ↑outside) ∈
    approx
      (let c := Box.ofRat c;
      let p := c.potential c n r;
      let t := p.1.sqr.sqr.sqr.sqr;
      let i := lerp t clear' outside';
      i.quantize)
Tactic:
have e : ∀ p : ℝ, p^16 = (((p^2)^2)^2)^2 := by intro p; rw [←pow_mul, ←pow_mul, ←pow_mul]
State after:
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (let p := potential 2 ↑↑c;
    let t := p ^ 16;
    lerp t ↑clear ↑outside) ∈
    approx
      (let c := Box.ofRat c;
      let p := c.potential c n r;
      let t := p.1.sqr.sqr.sqr.sqr;
      let i := lerp t clear' outside';
      i.quantize)

State before:
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (let p := potential 2 ↑↑c;
    let t := p ^ 16;
    lerp t ↑clear ↑outside) ∈
    approx
      (let c := Box.ofRat c;
      let p := c.potential c n r;
      let t := p.1.sqr.sqr.sqr.sqr;
      let i := lerp t clear' outside';
      i.quantize)
Tactic:
simp only [far', outside', clear', green', e]
State after:
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ lerp ((((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2) ↑clear ↑outside ∈
    approx (lerp ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr clear.ofRat outside.ofRat).quantize

State before:
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ lerp ((((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2) ↑clear ↑outside ∈
    approx (lerp ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr clear.ofRat outside.ofRat).quantize
Tactic:
apply Color.mem_approx_quantize
State after:
case cm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ lerp ((((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2) ↑clear ↑outside ∈
    approx (lerp ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr clear.ofRat outside.ofRat)

State before:
case cm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ lerp ((((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2) ↑clear ↑outside ∈
    approx (lerp ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr clear.ofRat outside.ofRat)
Tactic:
apply mem_approx_lerp
State after:
case cm.tm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr

case cm.xm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ↑clear ∈ approx clear.ofRat

case cm.ym
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ↑outside ∈ approx outside.ofRat

State before:
c : ℚ × ℚ
n : ℕ
r : Floating
⊢ ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
Tactic:
intro p
State after:
c : ℚ × ℚ
n : ℕ
r : Floating
p : ℝ
⊢ p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2

State before:
c : ℚ × ℚ
n : ℕ
r : Floating
p : ℝ
⊢ p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
Tactic:
rw [←pow_mul, ←pow_mul, ←pow_mul]
State after:
no goals

State before:
case cm.tm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (((potential 2 ↑↑c ^ 2) ^ 2) ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr.sqr
Tactic:
apply Interval.mem_approx_sqr
State after:
case cm.tm.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ((potential 2 ↑↑c ^ 2) ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr

State before:
case cm.tm.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ((potential 2 ↑↑c ^ 2) ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr.sqr
Tactic:
apply Interval.mem_approx_sqr
State after:
case cm.tm.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (potential 2 ↑↑c ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr

State before:
case cm.tm.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ (potential 2 ↑↑c ^ 2) ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr.sqr
Tactic:
apply Interval.mem_approx_sqr
State after:
case cm.tm.ax.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ potential 2 ↑↑c ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr

State before:
case cm.tm.ax.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ potential 2 ↑↑c ^ 2 ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1.sqr
Tactic:
apply Interval.mem_approx_sqr
State after:
case cm.tm.ax.ax.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ potential 2 ↑↑c ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1

State before:
case cm.tm.ax.ax.ax.ax
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ potential 2 ↑↑c ∈ approx ((Box.ofRat c).potential (Box.ofRat c) n r).1
Tactic:
mono
State after:
no goals

State before:
case cm.xm
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ↑clear ∈ approx clear.ofRat
Tactic:
mono
State after:
no goals

State before:
case cm.ym
c : ℚ × ℚ
n : ℕ
r : Floating
e : ∀ (p : ℝ), p ^ 16 = (((p ^ 2) ^ 2) ^ 2) ^ 2
⊢ ↑outside ∈ approx outside.ofRat
Tactic:
mono
State after:
no goals