Radius Reg Pow tendsto radius Pow

lemma radiusRegPow_tendsto_radiusPow' {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (h : 0 ≤ s ∨ ψ 0 = 0) :    Tendsto (fun ε ↦ ⇑(𝐫₀ ε s ψ)) nhdsZeroUnits (nhds (𝐫 s ψ)) := by  refine tendsto_pi_nhds.mpr fun x ↦ ?_  rcases eq_zero_or_neZero x with (rfl | hx)  · rcases h with (hs | hψ)    · simp only [radiusRegPowCLM_apply, radiusPowLM_apply, Complex.real_smul, norm_zero,        ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_add]      have : (0 : ℝ) ^ s = (0 ^ 2) ^ (s / 2) := by        rw [← Real.rpow_natCast_mul (le_refl 0), Nat.cast_ofNat, mul_div_cancel₀ s (by norm_num)]      rw [this]      refine Tendsto.mul_const (ψ 0) <| Tendsto.ofReal ?_      exact Tendsto.rpow_const (Tendsto.pow tendsto_comap 2) (Or.inr <| by linarith)    · simp [hψ]  · exact radiusRegPow_tendsto_radiusPow s ψ hx.ne