∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] (p : ENNReal) {μ : MeasureTheory.Measure E},
  μ.HasTemperateGrowth → ∃ k, MeasureTheory.eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) p μ < ⊤