∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {F : Type u_4}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [FiniteDimensional ℝ F] [inst_6 : MeasurableSpace F]
  [BorelSpace F] {μ : MeasureTheory.Measure F} [μ.IsAddHaarMeasure] {φ : F → ℝ},
  (∀ (x : F), 0 ≤ φ x) →
    ∫ (x : F), φ x ∂μ = 1 →
      Filter.Tendsto (fun x => ‖x‖ ^ Module.finrank ℝ F * φ x) (Bornology.cobounded F) (nhds 0) →
        ∀ {g : F → E} {x₀ : F},
          MeasureTheory.Integrable g μ →
            ContinuousAt g x₀ →
              Filter.Tendsto (fun c => ∫ (x : F), (c ^ Module.finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) Filter.atTop
                (nhds (g x₀))