internlm/Lean-Github huggingface dataset:
Theorem: Box.mem_approx_potential
Proof state before:
case neg
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
⊢ s.potential c' ↑z' ∈
    approx
      (match i.exit 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 hie : i.exit = ie
Proof state after:
case neg
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
ie : Exit
hie : i.exit = ie
⊢ s.potential c' ↑z' ∈
    approx
      (match ie 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
Theorem: Box.mem_approx_potential
Proof state before:
case pos
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
⊢ s.potential c' ↑z' ∈
    approx
      (let cs := cs;
        let i := iterate c z (cs.max 9) n;
        match i.exit with
        | Exit.nan => (nan, PotentialMode.nan)
        | Exit.large =>
          let rc := (r.mul r true).max (cs.max 36);
          let j := iterate c i.z rc 1000;
          match j.exit with
          | Exit.large => (j.z.potential_large.iter_sqrt (i.n + j.n), PotentialMode.large)
          | x => (nan, PotentialMode.nan)
        | Exit.count =>
          let zs := i.z.normSq.hi;
          if zs = nan ∨ 16 < zs ∨ 16 < cs then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [csn, Floating.nan_max, iterate_nan, Interval.approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.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.count
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count 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 hzs : (normSq i.z) = zs
Proof state after:
case neg.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.count
zs : Interval
hzs : i.z.normSq = zs
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count 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 zs = nan ∨ 16.val < zs.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.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.count
zs : Interval
hzs : i.z.normSq = zs
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count 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 zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
by_cases bad : zs = nan ∨ (16 : Floating).val < zs.hi.val ∨ (16 : Floating).val < cs.val
Proof state after:
case pos
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.count
zs : Interval
hzs : i.z.normSq = zs
bad : zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count 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 zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1

case neg
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.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬(zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val)
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count 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 zs = nan ∨ 16.val < zs.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 pos
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.count
zs : Interval
hzs : i.z.normSq = zs
bad : zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count 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 zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [Floating.val_lt_val, bad, ↓reduceIte, Interval.approx_nan, mem_univ]
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg
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.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬(zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val)
⊢ s.potential c' ↑z' ∈
    approx
      (match Exit.count 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 zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val then (nan, PotentialMode.nan)
          else (potential_small.iter_sqrt i.n, PotentialMode.small)).1
Tactic:
simp only [bad, ↓reduceIte]
Proof state after:
case neg
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.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬(zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val)
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Theorem: Box.mem_approx_potential
Proof state before:
case neg
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.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬(zs = nan ∨ 16.val < zs.hi.val ∨ 16.val < cs.val)
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
simp only [not_or, not_lt, ←hzs] at bad
Proof state after:
case neg
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.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬i.z.normSq = nan ∧ i.z.normSq.hi.val ≤ 16.val ∧ cs.val ≤ 16.val
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Theorem: Box.mem_approx_potential
Proof state before:
case neg
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.count
zs : Interval
hzs : i.z.normSq = zs
bad : ¬i.z.normSq = nan ∧ i.z.normSq.hi.val ≤ 16.val ∧ cs.val ≤ 16.val
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
rcases bad with ⟨zsn, z4, c4⟩
Proof state after:
case neg.intro.intro
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.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16.val
c4 : cs.val ≤ 16.val
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro
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.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ 16.val
c4 : cs.val ≤ 16.val
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
rw [Floating.val_ofNat] at c4 z4
Proof state after:
case neg.intro.intro
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.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ ↑16
c4 : cs.val ≤ ↑16
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro
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.count
zs : Interval
hzs : i.z.normSq = zs
zsn : ¬i.z.normSq = nan
z4 : i.z.normSq.hi.val ≤ ↑16
c4 : cs.val ≤ ↑16
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
simp only [← hcs, Nat.cast_ofNat, Interval.hi_eq_nan] at c4 z4 csn zsn
Proof state after:
case neg.intro.intro
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
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro
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
⊢ s.potential c' ↑z' ∈ approx (potential_small.iter_sqrt i.n)
Tactic:
apply Interval.mem_approx_iter_sqrt' s.potential_nonneg
Proof state after:
case neg.intro.intro
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
⊢ s.potential c' ↑z' ^ 2 ^ i.n ∈ approx potential_small
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro
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
⊢ s.potential c' ↑z' ^ 2 ^ i.n ∈ approx potential_small
Tactic:
simp only [←s.potential_eqn_iter, f_f'_iter]
Proof state after:
case neg.intro.intro
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
⊢ s.potential c' ↑((f' 2 c')^[i.n] z') ∈ approx potential_small
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro
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
⊢ s.potential c' ↑((f' 2 c')^[i.n] z') ∈ approx potential_small
Tactic:
generalize hw' : (f' 2 c')^[i.n] z' = w'
Proof state after:
case neg.intro.intro
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'
⊢ s.potential c' ↑w' ∈ approx potential_small
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro
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'
⊢ s.potential c' ↑w' ∈ approx potential_small
Tactic:
have le4 : Real.sqrt 16 ≤ 4 := by rw [Real.sqrt_le_iff]; norm_num
Proof state after:
case neg.intro.intro
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
⊢ s.potential c' ↑w' ∈ approx potential_small
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro
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
⊢ s.potential c' ↑w' ∈ approx potential_small
Tactic:
apply approx_potential_small
Proof state after:
case neg.intro.intro.c4
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
⊢ Complex.abs c' ≤ 4

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
⊢ Complex.abs w' ≤ 4
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
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'
⊢ √16 ≤ 4
Tactic:
rw [Real.sqrt_le_iff]
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
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'
⊢ 0 ≤ 4 ∧ 16 ≤ 4 ^ 2
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
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'
⊢ 0 ≤ 4 ∧ 16 ≤ 4 ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Box.mem_approx_potential
Proof state before:
case neg.intro.intro.c4
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
⊢ Complex.abs c' ≤ 4
Tactic:
exact le_trans (Box.abs_le_sqrt_normSq cm csn) (le_trans (Real.sqrt_le_sqrt c4) le4)
Proof state after:
no goals
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
⊢ Complex.abs w' ≤ 4
Tactic:
refine le_trans (Box.abs_le_sqrt_normSq ?_ zsn) (le_trans (Real.sqrt_le_sqrt z4) le4)
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
⊢ w' ∈ approx i.z