English
A strengthened basis-tends-to condition implies tightness for S.
Русский
Усиленное условие по базису влечет плотность для S.
LaTeX
$$isTightMeasureSet_of_forall_basis_tendsto$$
Lean4
/-- In a finite-dimensional inner product space,
a set of measures `S` is tight if and only if the function `r ↦ ⨆ μ ∈ S, μ {x | r < |⟪y, x⟫|}`
tends to `0` at infinity for all `y`. -/
theorem isTightMeasureSet_iff_inner_tendsto :
IsTightMeasureSet S ↔ ∀ y, Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪y, x⟫_𝕜‖}) atTop (𝓝 0) :=
by
refine ⟨fun h y ↦ ?_, isTightMeasureSet_of_inner_tendsto⟩
have : ProperSpace E := FiniteDimensional.proper 𝕜 E
rw [isTightMeasureSet_iff_tendsto_measure_norm_gt] at h
by_cases hy : y = 0
· simp only [hy, inner_zero_left]
refine (tendsto_congr' ?_).mpr tendsto_const_nhds
filter_upwards [eventually_ge_atTop 0] with r hr
simp [not_lt.mpr hr]
have h' : Tendsto (fun r ↦ ⨆ μ ∈ S, μ {x | r * ‖y‖⁻¹ < ‖x‖}) atTop (𝓝 0) :=
h.comp <| (tendsto_mul_const_atTop_of_pos (by positivity)).mpr tendsto_id
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds h' (fun _ ↦ zero_le') ?_
intro r
have h_le (μ : Measure E) : μ {x | r < ‖⟪y, x⟫_𝕜‖} ≤ μ {x | r * ‖y‖⁻¹ < ‖x‖} :=
by
refine measure_mono fun x hx ↦ ?_
simp only [Set.mem_setOf_eq] at hx ⊢
rw [mul_inv_lt_iff₀]
· rw [mul_comm]
exact hx.trans_le (norm_inner_le_norm y x)
· positivity
refine iSup₂_le_iff.mpr fun μ hμS ↦ ?_
exact le_iSup_of_le (i := μ) <| by simp [hμS, h_le]
