English
If every basis vector direction yields a tail tending to zero, then the set of measures is tight.
Русский
Если по каждому направлению базиса хвост стремится к нулю, тогда множество мер плотное.
LaTeX
$$isTightMeasureSet_of_forall_basis_tendsto$$
Lean4
theorem isTightMeasureSet_of_forall_basis_tendsto (b : OrthonormalBasis ι 𝕜 E)
(h : ∀ i, Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ {x | r < ‖⟪b i, x⟫_𝕜‖}) atTop (𝓝 0)) : IsTightMeasureSet S :=
by
rcases subsingleton_or_nontrivial E with hE | hE
· simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot]
convert tendsto_pure_nhds (a := ∅) _
simp
have h_rank : (0 : ℝ) < Fintype.card ι := by simpa [← Module.finrank_eq_card_basis b.toBasis, Module.finrank_pos_iff]
have : Nonempty ι := by simpa [Fintype.card_pos_iff] using h_rank
have : ProperSpace E := FiniteDimensional.proper 𝕜 E
refine isTightMeasureSet_of_tendsto_measure_norm_gt ?_
have h_le : (fun r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) ≤ fun r ↦ ∑ i, ⨆ μ ∈ S, μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} :=
by
intro r
calc
⨆ μ ∈ S, μ {x | r < ‖x‖}
_ ≤ ⨆ μ ∈ S, μ (⋃ i, {x : E | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) :=
by
gcongr with μ hμS
intro x hx
simp only [Set.mem_setOf_eq, Set.mem_iUnion] at hx ⊢
have hx' : r < √(Fintype.card ι) * ⨆ i, ‖⟪b i, x⟫_𝕜‖ := hx.trans_le (b.norm_le_card_mul_iSup_norm_inner x)
rw [← div_lt_iff₀' (by positivity)] at hx'
by_contra! h_le
exact lt_irrefl (r / √(Fintype.card ι)) (hx'.trans_le (ciSup_le h_le))
_ ≤ ⨆ μ ∈ S, ∑ i, μ {x : E | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} :=
by
gcongr with μ hμS
exact measure_iUnion_fintype_le μ _
_ ≤ ∑ i, ⨆ μ ∈ S, μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖} :=
by
refine iSup_le fun μ ↦ (iSup_le fun hμS ↦ ?_)
gcongr with i
exact le_biSup (fun μ ↦ μ {x | r / √(Fintype.card ι) < ‖⟪b i, x⟫_𝕜‖}) hμS
refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds ?_ (fun _ ↦ zero_le') h_le
rw [← Finset.sum_const_zero]
refine tendsto_finset_sum Finset.univ fun i _ ↦ (h i).comp ?_
exact tendsto_id.atTop_div_const (by positivity)
