internlm/Lean-Github huggingface dataset:
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
apply approx_potential_large
Proof state after:
case neg.large.large.cz
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ Complex.abs c' ≤ Complex.abs w'

case neg.large.large.z6
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 6 ≤ Complex.abs w'

case neg.large.large.zm
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
⊢ (f' 2 c')^[i.n] z' ∈ approx i.z
Tactic:
rw [←hi]
Proof state after:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
⊢ (f' 2 c')^[(iterate c z (cs.max 9) n✝).n] z' ∈ approx (iterate c z (cs.max 9) n✝).z
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
⊢ (f' 2 c')^[(iterate c z (cs.max 9) n✝).n] z' ∈ approx (iterate c z (cs.max 9) n✝).z
Tactic:
exact mem_approx_iterate cm zm _
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl :
  ((r.mul r true).max (cs.max 36)).val <
    Complex.abs ((f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z')) ^ 2
⊢ Exit.large ≠ Exit.nan
Tactic:
decide
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.cz
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ Complex.abs c' ≤ Complex.abs w'
Tactic:
refine le_trans ?_ (le_trans (Real.sqrt_le_sqrt jl.2.1.le) ?_)
Proof state after:
case neg.large.large.cz.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ Complex.abs c' ≤ cs.val.sqrt

case neg.large.large.cz.refine_2
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (Complex.abs w' ^ 2).sqrt ≤ Complex.abs w'
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.cz.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ Complex.abs c' ≤ cs.val.sqrt
Tactic:
simp only [← hcs, Interval.hi_eq_nan] at csn ⊢
Proof state after:
case neg.large.large.cz.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
csn : ¬c.normSq = nan
⊢ Complex.abs c' ≤ c.normSq.hi.val.sqrt
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.cz.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
csn : ¬c.normSq = nan
⊢ Complex.abs c' ≤ c.normSq.hi.val.sqrt
Tactic:
exact abs_le_sqrt_normSq cm csn
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.cz.refine_2
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (Complex.abs w' ^ 2).sqrt ≤ Complex.abs w'
Tactic:
simp only [apply_nonneg, Real.sqrt_sq, le_refl]
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.z6
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 6 ≤ Complex.abs w'
Tactic:
refine le_trans ?_ (le_trans (Real.sqrt_le_sqrt jl.2.2.le) ?_)
Proof state after:
case neg.large.large.z6.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 6 ≤ √36

case neg.large.large.z6.refine_2
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (Complex.abs w' ^ 2).sqrt ≤ Complex.abs w'
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.z6.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 6 ≤ √36
Tactic:
have e : (36 : ℝ) = 6 ^ 2 := by norm_num
Proof state after:
case neg.large.large.z6.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
e : 36 = 6 ^ 2
⊢ 6 ≤ √36
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.z6.refine_1
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
e : 36 = 6 ^ 2
⊢ 6 ≤ √36
Tactic:
rw [e, Real.sqrt_sq (by norm_num)]
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ 36 = 6 ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
e : 36 = 6 ^ 2
⊢ 0 ≤ 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.z6.refine_2
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (Complex.abs w' ^ 2).sqrt ≤ Complex.abs w'
Tactic:
simp only [apply_nonneg, Real.sqrt_sq, le_refl]
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.zm
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z
Tactic:
rw [←hw', ←hn, add_comm _ j.n, Function.iterate_add_apply, ←hj]
Proof state after:
case neg.large.large.zm
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z') ∈
    approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.large.zm
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n✝ : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n✝ = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
n : ℕ
hn : i.n + j.n = n
hje : (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit = Exit.large
w' : ℂ
hw' : (f' 2 c')^[n] z' = w'
izm : (f' 2 c')^[i.n] z' ∈ approx i.z
jl : (r.mul r true).val < Complex.abs w' ^ 2 ∧ cs.val < Complex.abs w' ^ 2 ∧ 36 < Complex.abs w' ^ 2
jrn : ¬r.mul r true = nan ∧ ¬cs = nan ∧ ¬36 = nan
⊢ (f' 2 c')^[(iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n] ((f' 2 c')^[i.n] z') ∈
    approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z
Tactic:
exact mem_approx_iterate cm izm _
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.nan
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.large
j : Iter
hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
hje : j.exit = Exit.nan
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.nan with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
simp only [Interval.approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.nan
c' z' : ℂ
c z : Box
cm : c' ∈ approx c
zm : z' ∈ approx z
n : ℕ
r : Floating
s : Super (f 2) 2 OnePoint.infty := superF 2
cs : Floating
hcs : c.normSq.hi = cs
i : Iter
hi : iterate c z (cs.max 9) n = i
csn : ¬cs = nan
hie : i.exit = Exit.nan
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.nan with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).exit with
          | Exit.large =>
            ((iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large.iter_sqrt
                (i.n + (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).n),
              PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          if i.z.normSq = nan ∨ 16.val < i.z.normSq.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [Interval.approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Box.mem_approx_potential'
Proof state before:
c' : ℂ
c : Box
cm : c' ∈ approx c
n : ℕ
r : Floating
⊢ _root_.potential 2 ↑c' ∈ approx (c.potential c n r).1
Tactic:
simp only [_root_.potential, RiemannSphere.fill_coe, mem_approx_potential cm cm]
Proof state after:
no goals
Theorem: Bound.pow_le_pow_right_of_le_one_or_one_le
Proof state before:
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
h : 1 ≤ a ∧ n ≤ m ∨ 0 ≤ a ∧ a ≤ 1 ∧ m ≤ n
⊢ a ^ n ≤ a ^ m
Tactic:
rcases h with ⟨a1, nm⟩ | ⟨a0, a1, mn⟩
Proof state after:
case inl.intro
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m

case inr.intro.intro
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m
Theorem: Bound.pow_le_pow_right_of_le_one_or_one_le
Proof state before:
case inl.intro
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
a1 : 1 ≤ a
nm : n ≤ m
⊢ a ^ n ≤ a ^ m
Tactic:
exact pow_le_pow_right a1 nm
Proof state after:
no goals
Theorem: Bound.pow_le_pow_right_of_le_one_or_one_le
Proof state before:
case inr.intro.intro
α : Type
inst✝¹ : LinearOrder α
a✝ b c : α
R : Type
inst✝ : OrderedSemiring R
a : R
n m : ℕ
a0 : 0 ≤ a
a1 : a ≤ 1
mn : m ≤ n
⊢ a ^ n ≤ a ^ m
Tactic:
exact pow_le_pow_of_le_one a0 a1 mn
Proof state after:
no goals
Theorem: Bound.Real.rpow_le_rpow_of_exponent_le_or_ge
Proof state before:
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
h : 1 ≤ x ∧ y ≤ z ∨ 0 < x ∧ x ≤ 1 ∧ z ≤ y
⊢ x ^ y ≤ x ^ z
Tactic:
rcases h with ⟨x1, yz⟩ | ⟨x0, x1, zy⟩
Proof state after:
case inl.intro
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
x1 : 1 ≤ x
yz : y ≤ z
⊢ x ^ y ≤ x ^ z

case inr.intro.intro
α : Type
inst✝ : LinearOrder α
a b c : α
x y z : ℝ
x0 : 0 < x
x1 : x ≤ 1
zy : z ≤ y
⊢ x ^ y ≤ x ^ z