English
For measurable s, the function r ↦ ρ.IicSnd r s tends to 0 as r ↓ -∞.
Русский
Для измеримого множества s функция r ↦ ρ.IicSnd r s стремится к 0 при r → -∞.
LaTeX
$$$\mathrm{Tendsto}\left(\lambda r. ρ.IicSnd r s\right)\;\mathrm{atBot}\; (\mathcal{N}(0))$$$
Lean4
theorem tendsto_IicSnd_atBot [IsFiniteMeasure ρ] {s : Set α} (hs : MeasurableSet s) :
Tendsto (fun r : ℚ ↦ ρ.IicSnd r s) atBot (𝓝 0) :=
by
simp_rw [ρ.IicSnd_apply _ hs]
have h_empty : ρ (s ×ˢ ∅) = 0 := by simp only [prod_empty, measure_empty]
rw [← h_empty, ← Real.iInter_Iic_rat, prod_iInter]
suffices h_neg : Tendsto (fun r : ℚ ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r : ℚ, s ×ˢ Iic ↑(-r))))
by
have h_inter_eq : ⋂ r : ℚ, s ×ˢ Iic ↑(-r) = ⋂ r : ℚ, s ×ˢ Iic (r : ℝ) :=
by
ext1 x
simp only [mem_iInter, mem_prod, mem_Iic]
refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩ <;> have h' := h (-i)
· rw [neg_neg] at h'; exact h'.2
· exact h'.2
rw [h_inter_eq] at h_neg
have h_fun_eq : (fun r : ℚ ↦ ρ (s ×ˢ Iic (r : ℝ))) = fun r : ℚ ↦ ρ (s ×ˢ Iic ↑(- -r)) := by simp_rw [neg_neg]
rw [h_fun_eq]
exact h_neg.comp tendsto_neg_atBot_atTop
refine tendsto_measure_iInter_atTop (fun q ↦ (hs.prod measurableSet_Iic).nullMeasurableSet) ?_ ⟨0, measure_ne_top ρ _⟩
refine fun q r hqr ↦ Set.prod_mono subset_rfl fun x hx ↦ ?_
simp only [Rat.cast_neg, mem_Iic] at hx ⊢
refine hx.trans (neg_le_neg ?_)
exact mod_cast hqr
