Theorems · Theorem · measure theory

tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn

∀ {α : Type u_1} {E : Type u_2} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E} {x₀ : α} {s : Set α}
  [CompleteSpace E] [TopologicalSpace.MetrizableSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure],
  IsCompact s →
    ∀ {c : α → ℝ},
      ContinuousOn c s →
        (∀ y ∈ s, y ≠ x₀ → c y < c x₀) →
          (∀ x ∈ s, 0 ≤ c x) →
            0 < c x₀ →
              x₀ ∈ closure (interior s) →
                ContinuousOn g s →
                  Filter.Tendsto (fun n => (∫ (x : α) in s, c x ^ n ∂μ)⁻¹ • ∫ (x : α) in s, c x ^ n • g x ∂μ)
                    Filter.atTop (nhds (g x₀))

If a continuous function c realizes its maximum at a unique point x₀ in a compact set s, then the sequence of functions (c x) ^ n / ∫ (c x) ^ n is a sequence of peak functions concentrating around x₀. Therefore, ∫ (c x) ^ n * g / ∫ (c x) ^ n converges to g x₀ if g is continuous on s.

Defined in

Mathlib.MeasureTheory.Integral.PeakFunction

Cited by

1 results in Mathlib

Foundations

Depth 264 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceBorelSpaceNormedAddCommGroupNormedSpaceCompleteSpaceTopologicalSpace.MetrizableSpaceMeasureTheory.IsLocallyFiniteMeasureMeasureTheory.Measure.IsOpenPosMeasure