Lean4
/-- 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
integrable on `s` and continuous at `x₀`.
Version assuming that `μ` gives positive mass to all neighborhoods of `x₀` within `s`.
For a less precise but more usable version, see
`tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn`.
-/
theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos [MetrizableSpace α]
[IsLocallyFiniteMeasure μ] (hs : IsCompact s) (hμ : ∀ u, IsOpen u → x₀ ∈ u → 0 < μ (u ∩ s)) {c : α → ℝ}
(hc : ContinuousOn c s) (h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀) (hnc : ∀ x ∈ s, 0 ≤ c x) (hnc₀ : 0 < c x₀)
(h₀ : x₀ ∈ s) (hmg : IntegrableOn g s μ) (hcg : ContinuousWithinAt g s x₀) :
Tendsto (fun n : ℕ => (∫ x in s, c x ^ n ∂μ)⁻¹ • ∫ x in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀)) := by
/- We apply the general result
`tendsto_setIntegral_peak_smul_of_integrableOn_of_continuousWithinAt` to the sequence of
peak functions `φₙ = (c x) ^ n / ∫ (c x) ^ n`. The only nontrivial bit is to check that this
sequence converges uniformly to zero on any set `s \ u` away from `x₀`. By compactness, the
function `c` is bounded by `t < c x₀` there. Consider `t' ∈ (t, c x₀)`, and a neighborhood `v`
of `x₀` where `c x ≥ t'`, by continuity. Then `∫ (c x) ^ n` is bounded below by `t' ^ n μ v`.
It follows that, on `s \ u`, then `φₙ x ≤ t ^ n / (t' ^ n μ v)`,
which tends (exponentially fast) to zero with `n`. -/
let φ : ℕ → α → ℝ := fun n x => (∫ x in s, c x ^ n ∂μ)⁻¹ * c x ^ n
have hnφ : ∀ n, ∀ x ∈ s, 0 ≤ φ n x := by
intro n x hx
apply mul_nonneg (inv_nonneg.2 _) (pow_nonneg (hnc x hx) _)
exact setIntegral_nonneg hs.measurableSet fun x hx => pow_nonneg (hnc x hx) _
have I : ∀ n, IntegrableOn (fun x => c x ^ n) s μ := fun n => ContinuousOn.integrableOn_compact hs (hc.pow n)
have J : ∀ n, 0 ≤ᵐ[μ.restrict s] fun x : α => c x ^ n :=
by
intro n
filter_upwards [ae_restrict_mem hs.measurableSet] with x hx
exact pow_nonneg (hnc x hx) n
have P : ∀ n, (0 : ℝ) < ∫ x in s, c x ^ n ∂μ := by
intro n
refine (setIntegral_pos_iff_support_of_nonneg_ae (J n) (I n)).2 ?_
obtain ⟨u, u_open, x₀_u, hu⟩ : ∃ u : Set α, IsOpen u ∧ x₀ ∈ u ∧ u ∩ s ⊆ c ⁻¹' Ioi 0 :=
_root_.continuousOn_iff.1 hc x₀ h₀ (Ioi (0 : ℝ)) isOpen_Ioi hnc₀
apply (hμ u u_open x₀_u).trans_le
exact measure_mono fun x hx => ⟨ne_of_gt (pow_pos (a := c x) (hu hx) _), hx.2⟩
have hiφ : ∀ n, ∫ x in s, φ n x ∂μ = 1 := fun n => by rw [integral_const_mul, inv_mul_cancel₀ (P n).ne']
have A : ∀ u : Set α, IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 atTop (s \ u) :=
by
intro u u_open x₀u
obtain ⟨t, t_pos, tx₀, ht⟩ : ∃ t, 0 ≤ t ∧ t < c x₀ ∧ ∀ x ∈ s \ u, c x ≤ t :=
by
rcases eq_empty_or_nonempty (s \ u) with (h | h)
· exact ⟨0, le_rfl, hnc₀, by simp only [h, mem_empty_iff_false, IsEmpty.forall_iff, imp_true_iff]⟩
obtain ⟨x, hx, h'x⟩ : ∃ x ∈ s \ u, ∀ y ∈ s \ u, c y ≤ c x :=
IsCompact.exists_isMaxOn (hs.diff u_open) h (hc.mono diff_subset)
refine ⟨c x, hnc x hx.1, h'c x hx.1 ?_, h'x⟩
rintro rfl
exact hx.2 x₀u
obtain ⟨t', tt', t'x₀⟩ : ∃ t', t < t' ∧ t' < c x₀ := exists_between tx₀
have t'_pos : 0 < t' := t_pos.trans_lt tt'
obtain ⟨v, v_open, x₀_v, hv⟩ : ∃ v : Set α, IsOpen v ∧ x₀ ∈ v ∧ v ∩ s ⊆ c ⁻¹' Ioi t' :=
_root_.continuousOn_iff.1 hc x₀ h₀ (Ioi t') isOpen_Ioi t'x₀
have M : ∀ n, ∀ x ∈ s \ u, φ n x ≤ (μ.real (v ∩ s))⁻¹ * (t / t') ^ n :=
by
intro n x hx
have B : t' ^ n * μ.real (v ∩ s) ≤ ∫ y in s, c y ^ n ∂μ :=
calc
t' ^ n * μ.real (v ∩ s) = ∫ _ in v ∩ s, t' ^ n ∂μ := by simp [mul_comm]
_ ≤ ∫ y in v ∩ s, c y ^ n ∂μ :=
by
apply setIntegral_mono_on _ _ (v_open.measurableSet.inter hs.measurableSet) _
· refine integrableOn_const (C := t' ^ n) ?_
exact (lt_of_le_of_lt (measure_mono inter_subset_right) hs.measure_lt_top).ne
· exact (I n).mono inter_subset_right le_rfl
· intro x hx
exact pow_le_pow_left₀ t'_pos.le (hv hx).le _
_ ≤ ∫ y in s, c y ^ n ∂μ := setIntegral_mono_set (I n) (J n) (Eventually.of_forall inter_subset_right)
simp_rw [φ, ← div_eq_inv_mul, div_pow, div_div]
have :=
ENNReal.toReal_pos (hμ v v_open x₀_v).ne' ((measure_mono inter_subset_right).trans_lt hs.measure_lt_top).ne
gcongr
· exact hnc _ hx.1
· exact ht x hx
have N : Tendsto (fun n => (μ.real (v ∩ s))⁻¹ * (t / t') ^ n) atTop (𝓝 ((μ.real (v ∩ s))⁻¹ * 0)) :=
by
apply Tendsto.mul tendsto_const_nhds _
apply tendsto_pow_atTop_nhds_zero_of_lt_one (div_nonneg t_pos t'_pos.le)
exact (div_lt_one t'_pos).2 tt'
rw [mul_zero] at N
refine tendstoUniformlyOn_iff.2 fun ε εpos => ?_
filter_upwards [(tendsto_order.1 N).2 ε εpos] with n hn x hx
simp only [Pi.zero_apply, dist_zero_left, Real.norm_of_nonneg (hnφ n x hx.1)]
exact (M n x hx).trans_lt hn
have : Tendsto (fun i : ℕ => ∫ x : α in s, φ i x • g x ∂μ) atTop (𝓝 (g x₀)) :=
by
have B : Tendsto (fun i ↦ ∫ (x : α) in s, φ i x ∂μ) atTop (𝓝 1) := tendsto_const_nhds.congr (fun n ↦ (hiφ n).symm)
have C : ∀ᶠ (i : ℕ) in atTop, AEStronglyMeasurable (fun x ↦ φ i x) (μ.restrict s) := by
apply Eventually.of_forall (fun n ↦ ((I n).const_mul _).aestronglyMeasurable)
exact
tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto hs.measurableSet hs.measurableSet (Subset.rfl)
(self_mem_nhdsWithin) hs.measure_lt_top.ne (Eventually.of_forall hnφ) A B C hmg hcg
convert this
simp_rw [φ, ← smul_smul, integral_smul]
