internlm/Lean-Github huggingface dataset:
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro.z4
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.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ w' ∈ approx i.z
Tactic:
rw [←hw', ←hi]
Proof state after:
case neg.intro.intro.z4
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.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ (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:
case neg.intro.intro.z4
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.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16
c4 : c.normSq.hi.val ≤ 16
csn : ¬c.normSq = nan
w' : ℂ
hw' : (f' 2 c')^[i.n] z' = w'
le4 : √16 ≤ 4
⊢ (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:
case neg.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
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large 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:
generalize hj : iterate c i.z ((r.mul r true).max (cs.max 36)) 1000 = j
Proof state after:
case neg.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
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.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
Theorem: Box.mem_approx_potential
Proof state before:
case neg.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
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.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 [hj]
Proof state after:
case neg.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
⊢ s.potential c' ↑z' ∈
    approx
      (match j.exit with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Theorem: Box.mem_approx_potential
Proof state before:
case neg.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
⊢ s.potential c' ↑z' ∈
    approx
      (match j.exit with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
generalize hje : j.exit = je
Proof state after:
case neg.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
je : Exit
hje : j.exit = je
⊢ s.potential c' ↑z' ∈
    approx
      (match je with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Theorem: Box.mem_approx_potential
Proof state before:
case neg.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
je : Exit
hje : j.exit = je
⊢ s.potential c' ↑z' ∈
    approx
      (match je with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
induction je
Proof state after:
case neg.large.count
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.count
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1

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
hje : j.exit = Exit.large
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1

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
Theorem: Box.mem_approx_potential
Proof state before:
case neg.large.count
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.count
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count 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.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
hje : j.exit = Exit.large
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.large with
        | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
        | x => (nan, PotentialMode.nan)).1
Tactic:
simp only
Proof state after:
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
hje : j.exit = Exit.large
⊢ s.potential c' ↑z' ∈ approx (j.z.potential_large.iter_sqrt (i.n + j.n))
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
hje : j.exit = Exit.large
⊢ s.potential c' ↑z' ∈ approx (j.z.potential_large.iter_sqrt (i.n + j.n))
Tactic:
generalize hn : i.n + j.n = n
Proof state after:
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
hje : j.exit = Exit.large
n : ℕ
hn : i.n + j.n = n
⊢ s.potential c' ↑z' ∈ approx (j.z.potential_large.iter_sqrt n)
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
hje : j.exit = Exit.large
n : ℕ
hn : i.n + j.n = n
⊢ s.potential c' ↑z' ∈ approx (j.z.potential_large.iter_sqrt n)
Tactic:
apply Interval.mem_approx_iter_sqrt' s.potential_nonneg
Proof state after:
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
hje : j.exit = Exit.large
n : ℕ
hn : i.n + j.n = n
⊢ s.potential c' ↑z' ^ 2 ^ n ∈ approx j.z.potential_large
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
hje : j.exit = Exit.large
n : ℕ
hn : i.n + j.n = n
⊢ s.potential c' ↑z' ^ 2 ^ n ∈ approx j.z.potential_large
Tactic:
simp only [←s.potential_eqn_iter, f_f'_iter, ←hj] at hje ⊢
Proof state after:
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
⊢ s.potential c' ↑((f' 2 c')^[n] z') ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
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
⊢ s.potential c' ↑((f' 2 c')^[n] z') ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
generalize hw' : (f' 2 c')^[n] z' = w'
Proof state after:
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'
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
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'
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
have izm : (f' 2 c')^[i.n] z' ∈ approx i.z := by rw [←hi]; exact mem_approx_iterate cm zm _
Proof state after:
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
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
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
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
have jl := iterate_large cm izm hje
Proof state after:
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).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
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
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).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
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
have jrn := ne_nan_of_iterate (hje.trans_ne (by decide))
Proof state after:
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).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
jrn : (r.mul r true).max (cs.max 36) ≠ nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
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).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
jrn : (r.mul r true).max (cs.max 36) ≠ nan
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
simp only [hj, ← Function.iterate_add_apply, add_comm _ i.n, hn, hw'] at jl
Proof state after:
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
jrn : (r.mul r true).max (cs.max 36) ≠ nan
jl : ((r.mul r true).max (cs.max 36)).val < Complex.abs w' ^ 2
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
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
jrn : (r.mul r true).max (cs.max 36) ≠ nan
jl : ((r.mul r true).max (cs.max 36)).val < Complex.abs w' ^ 2
⊢ s.potential c' ↑w' ∈ approx (iterate c i.z ((r.mul r true).max (cs.max 36)) 1000).z.potential_large
Tactic:
simp only [ne_eq, Floating.max_eq_nan, not_or] at jrn
Proof state after:
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).max (cs.max 36)).val < 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
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).max (cs.max 36)).val < 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:
rw [Floating.val_max jrn.1 (Floating.max_ne_nan.mpr jrn.2),
  Floating.val_max jrn.2.1 jrn.2.2, max_lt_iff, max_lt_iff, Floating.val_ofNat,
  Nat.cast_eq_ofNat] at jl
Proof state after:
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