Theorem: Interval.mem_approx_iter_sqrt (Ray/Render/Potential.lean)

State before:
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.iter_sqrt n)
Tactic:
rw [iter_sqrt]
State after:
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp

State before:
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Tactic:
by_cases a0 : a ≤ 0
State after:
case pos
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : a ≤ 0
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp

case neg
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : ¬a ≤ 0
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp

State before:
case pos
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : a ≤ 0
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Tactic:
simp only [log_nonpos a0 ax, nan_scaleB', exp_nan, approx_nan, mem_univ]
State after:
no goals

State before:
case neg
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : ¬a ≤ 0
⊢ a ^ 2 ^ (-↑n) ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Tactic:
rw [Real.rpow_def_of_pos (not_le.mp a0)]
State after:
case neg
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : ¬a ≤ 0
⊢ (a.log * 2 ^ (-↑n)).exp ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp

State before:
case neg
a : ℝ
x : Interval
n : ℕ
ax : a ∈ approx x
a0 : ¬a ≤ 0
⊢ (a.log * 2 ^ (-↑n)).exp ∈ approx (x.log.scaleB' (-Fixed.ofNat0 n)).exp
Tactic:
mono
State after:
no goals