Radius Pow LM apply mem HS

lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a : ℕ)    (hψ : ψ ∈ PolyBddSchwartzMap d a) (h : 0 < d + 2 * (a + s)) :    MemHS (𝐫 s ψ) := by  rcases Nat.eq_zero_or_pos d with (rfl | hd)  · simp only [MemHS, MemLp.of_discrete]  · have : NeZero d := ⟨hd.ne'⟩    refine (memLp_two_iff_integrable_sq_norm (by fun_prop)).mpr ⟨by fun_prop, ?_⟩    suffices ∫⁻ (x : Space d), ‖‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s)‖ₑ < ⊤ by      have hInt (x : Space d) : ‖𝐫 s ψ x‖ ^ 2 = ‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s) := by        simp [radiusPowLM, mul_pow, mul_comm, Real.rpow_mul]      simpa only [HasFiniteIntegral, hInt]    have lintegral_lt_top_aux : ∀ {S : Set (Space d)} {C p : ℝ},        IntegrableOn (fun x ↦ ‖x‖ ^ p) S → ∀ {G : Space d → ENNReal},        ∫⁻ x in S, G x ≤ ∫⁻ x in S, ‖C ^ 2‖ₑ * ‖‖x‖ ^ p‖ₑ →        ∫⁻ x in S, G x < ⊤ := by      intro S C p hp G hG      refine hG.trans_lt ?_      rw [lintegral_const_mul _ (by fun_prop)]      exact ENNReal.mul_lt_top enorm_lt_top hp.hasFiniteIntegral    rw [← lintegral_add_compl _ (measurableSet_ball (x := 0) (ε := 1)), ENNReal.add_lt_top]    constructor    · -- `‖x‖ < 1`: bound `‖ψ x‖` by `‖x‖ᵃ`      obtain ⟨C, hC_pos, hC⟩ := hψ a (le_refl _)      suffices hBound : ∀ᵐ x, ‖‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s)‖ₑ ≤ ‖C ^ 2‖ₑ * ‖‖x‖ ^ (2 * (a + s))‖ₑ by        exact lintegral_lt_top_aux ((integrableOn_norm_rpow_ball_iff Real.zero_lt_one _).mpr h)          (setLIntegral_mono_ae' measurableSet_ball (Eventually.mono hBound fun _ h' _ ↦ h'))      apply ae_iff.mpr      refine measure_mono_null ?_ (measure_singleton 0)      intro x hx      by_contra hx'      apply hx      apply norm_pos_iff.mpr at hx'      simp_rw [← enorm_mul, enorm_le_iff_norm_le, mul_add, Real.rpow_add hx', norm_mul, ← mul_assoc]      refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)      simp_rw [← Nat.cast_two (R := ℝ), mul_comm, Real.rpow_mul_natCast hx'.le, norm_pow, ← mul_pow,        norm_norm, Real.norm_eq_abs, abs_of_pos hC_pos, abs_of_nonneg (Real.rpow_nonneg hx'.le _)]      apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mpr      apply (inv_mul_le_iff₀' (by positivity)).mp      rw [← Real.rpow_neg_one, ← Real.rpow_mul hx'.le, mul_comm _ (-1), neg_mul, one_mul,        Real.rpow_neg_natCast]      exact hC x    · -- `1 ≤ ‖x‖`: bound `‖ψ x‖` by a suitable power of `‖x‖`      obtain ⟨C, hC_pos, hC⟩ := ψ.decay (⌈s⌉.toNat + d) 0      simp only [norm_iteratedFDeriv_zero, ← Real.rpow_natCast, Nat.cast_add] at hC      suffices hBound : ∀ x ∈ (Metric.ball 0 1)ᶜ,          ‖‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s)‖ₑ ≤ ‖C ^ 2‖ₑ * ‖‖x‖ ^ (-2 * d : ℝ)‖ₑ by        have hd' : (d + -2 * d : ℝ) < 0 := by simp [hd]        exact lintegral_lt_top_aux ((integrableOn_norm_rpow_ball_compl_iff zero_lt_one _).mpr hd')          (setLIntegral_mono' (by measurability) hBound)      intro x hx      simp only [Set.mem_compl_iff, Metric.mem_ball, dist_zero_right, not_lt] at hx      simp_rw [← enorm_mul, enorm_le_iff_norm_le, norm_mul, norm_pow, Real.norm_eq_abs, sq_abs,        Real.abs_rpow_of_nonneg (norm_nonneg _), abs_norm]      have hx' : 0 < ‖x‖ := by linarith      have hψ : ‖ψ x‖ ≤ C * ‖x‖ ^ (-(⌈s⌉.toNat + d) : ℝ) := by        rw [Real.rpow_neg hx'.le]        exact (le_mul_inv_iff₀' <| Real.rpow_pos_of_pos hx' _).mpr (hC x)      calc        _ ≤ (C * ‖x‖ ^ (-(⌈s⌉.toNat + d) : ℝ)) ^ 2 * ‖x‖ ^ (2 * s) := by          refine mul_le_mul_of_nonneg_right ?_ (Real.rpow_nonneg hx'.le _)          exact pow_le_pow_left₀ (norm_nonneg _) hψ 2        _ = C ^ 2 * ‖x‖ ^ (-2 * d : ℝ) * ‖x‖ ^ (2 * (s - ⌈s⌉.toNat) : ℝ) := by          simp_rw [mul_pow, ← Real.rpow_mul_natCast hx'.le, mul_assoc, ← Real.rpow_add hx']          ring_nf      suffices s ≤ ⌈s⌉.toNat by        have h' : 0 < C ^ 2 * ‖x‖ ^ (-2 * d : ℝ) :=          mul_pos (sq_pos_of_pos hC_pos) (Real.rpow_pos_of_pos hx' _)        apply (mul_le_iff_le_one_right h').mpr        exact Real.rpow_le_one_of_one_le_of_nonpos hx (by linarith)      exact (Int.le_ceil s).trans (by exact_mod_cast Int.self_le_toNat ⌈s⌉)