English
A tendsto result for a composite smul of a measure-integrable function by a smoothed scalar field.
Русский
Сходимость интеграла от смуля, полученного по композитной функции и сглаженным весам.
LaTeX
$$$\\text{tendsto_integral_comp_smul_smul_of_integrable}$: convergence of ∫ φ_i x · g x as i→∞$$
Lean4
/-- Consider a nonnegative function `φ` with integral one, decaying quickly enough at infinity.
Then suitable renormalizations of `φ` form a sequence of peak functions around the origin:
`∫ (c ^ d * φ (c • x)) • g x` converges to `g 0` as `c → ∞` if `g` is continuous at `0`
and integrable. -/
theorem tendsto_integral_comp_smul_smul_of_integrable {φ : F → ℝ} (hφ : ∀ x, 0 ≤ φ x) (h'φ : ∫ x, φ x ∂μ = 1)
(h : Tendsto (fun x ↦ ‖x‖ ^ finrank ℝ F * φ x) (cobounded F) (𝓝 0)) {g : F → E} (hg : Integrable g μ)
(h'g : ContinuousAt g 0) : Tendsto (fun (c : ℝ) ↦ ∫ x, (c ^ (finrank ℝ F) * φ (c • x)) • g x ∂μ) atTop (𝓝 (g 0)) :=
by
have I : Integrable φ μ := integrable_of_integral_eq_one h'φ
apply tendsto_integral_peak_smul_of_integrable_of_tendsto (t := closedBall 0 1) (x₀ := 0)
· exact isClosed_closedBall.measurableSet
· exact closedBall_mem_nhds _ zero_lt_one
· exact (isCompact_closedBall 0 1).measure_ne_top
· filter_upwards [Ici_mem_atTop 0] with c (hc : 0 ≤ c) x using mul_nonneg (by positivity) (hφ _)
· intro u u_open hu
apply tendstoUniformlyOn_iff.2 (fun ε εpos ↦ ?_)
obtain ⟨δ, δpos, h'u⟩ : ∃ δ > 0, ball 0 δ ⊆ u := Metric.isOpen_iff.1 u_open _ hu
obtain ⟨M, Mpos, hM⟩ : ∃ M > 0, ∀ ⦃x : F⦄, x ∈ (closedBall 0 M)ᶜ → ‖x‖ ^ finrank ℝ F * φ x < δ ^ finrank ℝ F * ε :=
by
rcases
(hasBasis_cobounded_compl_closedBall (0 : F)).eventually_iff.1
((tendsto_order.1 h).2 (δ ^ finrank ℝ F * ε) (by positivity)) with
⟨M, -, hM⟩
refine ⟨max M 1, zero_lt_one.trans_le (le_max_right _ _), fun x hx ↦ hM ?_⟩
simp only [mem_compl_iff, mem_closedBall, dist_zero_right, le_max_iff, not_or, not_le] at hx
simpa using hx.1
filter_upwards [Ioi_mem_atTop (M / δ)] with c (hc : M / δ < c) x hx
have cpos : 0 < c := lt_trans (by positivity) hc
suffices c ^ finrank ℝ F * φ (c • x) < ε by simpa [abs_of_nonneg (hφ _), abs_of_nonneg cpos.le]
have hδx : δ ≤ ‖x‖ := by
have : x ∈ (ball 0 δ)ᶜ := fun h ↦ hx (h'u h)
simpa only [mem_compl_iff, mem_ball, dist_zero_right, not_lt]
suffices δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) < δ ^ finrank ℝ F * ε by
rwa [mul_lt_mul_iff_of_pos_left (by positivity)] at this
calc
δ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x))
_ ≤ ‖x‖ ^ finrank ℝ F * (c ^ finrank ℝ F * φ (c • x)) := by gcongr; exact mul_nonneg (by positivity) (hφ _)
_ = ‖c • x‖ ^ finrank ℝ F * φ (c • x) := by simp [norm_smul, abs_of_pos cpos, mul_pow]; ring
_ < δ ^ finrank ℝ F * ε := by
apply hM
rw [div_lt_iff₀ δpos] at hc
simp only [mem_compl_iff, mem_closedBall, dist_zero_right, norm_smul, Real.norm_eq_abs, abs_of_nonneg cpos.le,
not_le]
exact hc.trans_le (by gcongr)
· have : Tendsto (fun c ↦ ∫ (x : F) in closedBall 0 c, φ x ∂μ) atTop (𝓝 1) :=
by
rw [← h'φ]
exact (aecover_closedBall tendsto_id).integral_tendsto_of_countably_generated I
apply this.congr'
filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
rw [integral_const_mul, setIntegral_comp_smul_of_pos _ _ _ hc, smul_eq_mul, ← mul_assoc,
mul_inv_cancel₀ (by positivity), _root_.smul_closedBall _ _ zero_le_one]
simp [abs_of_nonneg hc.le]
· filter_upwards [Ioi_mem_atTop 0] with c (hc : 0 < c)
exact (I.comp_smul hc.ne').aestronglyMeasurable.const_mul _
· exact hg
· exact h'g
