Theorem: Box.approx_potential_large (Ray/Render/Potential.lean)

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ ⋯.potential c' ↑z' ∈ approx z.potential_large
Tactic:
rw [potential_large]
State after:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ ⋯.potential c' ↑z' ∈
    approx
      (let s := z.normSq;
      let log_s := s.log;
      (-log_s.div2).exp.grow (0.8095 * (log_s * -0.9635).exp).hi)

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ ⋯.potential c' ↑z' ∈
    approx
      (let s := z.normSq;
      let log_s := s.log;
      (-log_s.div2).exp.grow (0.8095 * (log_s * -0.9635).exp).hi)
Tactic:
apply Interval.approx_grow (potential_approx 2 (le_trans (by norm_num) z6) cz)
State after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ (0.8095 * (z.normSq.log * -0.9635).exp).hi ≠ nan →
    potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val

case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 1 / Complex.abs z' ∈ approx (-z.normSq.log.div2).exp

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 4 ≤ 6
Tactic:
norm_num
State after:
no goals

State before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ (0.8095 * (z.normSq.log * -0.9635).exp).hi ≠ nan →
    potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Tactic:
intro n
State after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : (0.8095 * (z.normSq.log * -0.9635).exp).hi ≠ nan
⊢ potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val

State before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : (0.8095 * (z.normSq.log * -0.9635).exp).hi ≠ nan
⊢ potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Tactic:
rw [Ne, Interval.hi_eq_nan] at n
State after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val

State before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ potential_error 2 c' z' ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Tactic:
refine le_trans (potential_error_le_of_z6 _ z6 cz) ?_
State after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 / Complex.abs z' ^ 1.927 ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val

State before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 / Complex.abs z' ^ 1.927 ≤ (0.8095 * (z.normSq.log * -0.9635).exp).hi.val
Tactic:
apply Interval.le_hi n
State after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 / Complex.abs z' ^ 1.927 ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)

State before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 / Complex.abs z' ^ 1.927 ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Tactic:
rw [div_eq_mul_inv, ←Real.rpow_neg (Complex.abs.nonneg _), Real.rpow_def_of_pos (by linarith)]
State after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 * ((Complex.abs z').log * -1.927).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)

State before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0.8095 * ((Complex.abs z').log * -1.927).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Tactic:
have e : Real.log (Complex.abs z') * -1.927 = Real.log (Complex.abs z' ^ 2) * -0.9635 := by
  rw [Real.log_pow, Nat.cast_two, mul_comm (2:ℝ), mul_assoc]; norm_num
State after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
e : (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
⊢ 0.8095 * ((Complex.abs z').log * -1.927).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)

State before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
e : (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
⊢ 0.8095 * ((Complex.abs z').log * -1.927).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Tactic:
rw [e]
State after:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
e : (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
⊢ 0.8095 * ((Complex.abs z' ^ 2).log * -0.9635).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)

State before:
case be
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
e : (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
⊢ 0.8095 * ((Complex.abs z' ^ 2).log * -0.9635).exp ∈ approx (0.8095 * (z.normSq.log * -0.9635).exp)
Tactic:
mono
State after:
no goals

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ 0 < Complex.abs z'
Tactic:
linarith
State after:
no goals

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ (Complex.abs z').log * -1.927 = (Complex.abs z' ^ 2).log * -0.9635
Tactic:
rw [Real.log_pow, Nat.cast_two, mul_comm (2:ℝ), mul_assoc]
State after:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ (Complex.abs z').log * -1.927 = (Complex.abs z').log * (2 * -0.9635)

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
n : ¬0.8095 * (z.normSq.log * -0.9635).exp = nan
⊢ (Complex.abs z').log * -1.927 = (Complex.abs z').log * (2 * -0.9635)
Tactic:
norm_num
State after:
no goals

State before:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 1 / Complex.abs z' ∈ approx (-z.normSq.log.div2).exp
Tactic:
have e : 1 / Complex.abs z' = Real.exp (-(Real.log (Complex.abs z' ^ 2) / 2)) := by
  simp only [one_div, Real.log_pow, Nat.cast_ofNat, neg_mul, Real.rpow_neg zero_le_two,
    Real.rpow_one, ←mul_assoc, mul_comm _ (2:ℝ)⁻¹]
  rw [mul_div_cancel_left₀ _ two_ne_zero, Real.exp_neg, Real.exp_log (by linarith)]
State after:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
e : 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
⊢ 1 / Complex.abs z' ∈ approx (-z.normSq.log.div2).exp

State before:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
e : 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
⊢ 1 / Complex.abs z' ∈ approx (-z.normSq.log.div2).exp
Tactic:
rw [e]
State after:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
e : 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
⊢ (-((Complex.abs z' ^ 2).log / 2)).exp ∈ approx (-z.normSq.log.div2).exp

State before:
case zx
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
e : 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
⊢ (-((Complex.abs z' ^ 2).log / 2)).exp ∈ approx (-z.normSq.log.div2).exp
Tactic:
mono
State after:
no goals

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 1 / Complex.abs z' = (-((Complex.abs z' ^ 2).log / 2)).exp
Tactic:
simp only [one_div, Real.log_pow, Nat.cast_ofNat, neg_mul, Real.rpow_neg zero_le_two,
  Real.rpow_one, ←mul_assoc, mul_comm _ (2:ℝ)⁻¹]
State after:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ (Complex.abs z')⁻¹ = (-(2 * (Complex.abs z').log / 2)).exp

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ (Complex.abs z')⁻¹ = (-(2 * (Complex.abs z').log / 2)).exp
Tactic:
rw [mul_div_cancel_left₀ _ two_ne_zero, Real.exp_neg, Real.exp_log (by linarith)]
State after:
no goals

State before:
c' z' : ℂ
z : Box
cz : Complex.abs c' ≤ Complex.abs z'
z6 : 6 ≤ Complex.abs z'
zm : z' ∈ approx z
⊢ 0 < Complex.abs z'
Tactic:
linarith
State after:
no goals