Exponent identities for the zoom-in map

These lemmas collect the algebraic identities satisfied by the rescaling exponents that appear in eq:aniso:zoom:fields and eq:aniso:zoom:finite:variables.

theorem CIV.zoom_lambda_sq {t : ℝ} (ht : t < 0) : ((-t) ^ (1 / 2)) ^ 2 = -t

theorem CIV.zoom_lambda_eq_delta_mul_mu {lam h : ℝ} (hlam : 0 < lam) : lam = lam ^ (2 * h) * lam ^ (1 - 2 * h)

theorem CIV.zoom_rescaled_exponent {lam h : ℝ} (hlam : 0 < lam) (a b : ℕ) (τ : ℝ) (hτ : τ < 0) : lam ^ (1 + a) * (lam ^ (1 - 2 * h)) ^ b * (lam ^ 2 * -τ) ^ (-(1 / 2) - ↑a / 2 - (1 / 2 - h) * ↑b) = (-τ) ^ (-(1 / 2) - ↑a / 2 - (1 / 2 - h) * ↑b)

theorem CIV.zoom_rescaled_exponent_swirl {lam h : ℝ} (hlam : 0 < lam) (a b : ℕ) (τ : ℝ) (hτ : τ < 0) : lam ^ (1 + a) * lam ^ (2 * h) * (lam ^ (1 - 2 * h)) ^ b * (lam ^ 2 * -τ) ^ (-(1 / 2) - h - ↑a / 2 - (1 / 2 - h) * ↑b) = (-τ) ^ (-(1 / 2) - h - ↑a / 2 - (1 / 2 - h) * ↑b)

theorem CIV.tendsto_zoom_lengths {h : ℝ} (hh : 0 < h ∧ h < 1 / 2) : Filter.Tendsto (fun (t : ℝ) => (-t) ^ (1 / 2)) (nhdsWithin 0 (Set.Iio 0)) (nhds 0) ∧ Filter.Tendsto (fun (t : ℝ) => ((-t) ^ (1 / 2)) ^ (2 * h)) (nhdsWithin 0 (Set.Iio 0)) (nhds 0) ∧ Filter.Tendsto (fun (t : ℝ) => ((-t) ^ (1 / 2)) ^ (1 - 2 * h)) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)