isTightMeasureSet_iff_tendsto_measure_norm_gt

English

If S is tight and f is continuous, then the image of S under the pushforward map is also tight.

Русский

Если S плотное и f непрерывна, то образ S под перенесением по f также плотный.

LaTeX

$$IsTightMeasureSet S → (∀ {f}, Continuous f → IsTightMeasureSet (Set.image (Measure.map f) S))$$

Lean4

/-- In a proper normed group, a set of measures `S` is tight if and only if
the function `r ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}` tends to `0` at infinity. -/
theorem isTightMeasureSet_iff_tendsto_measure_norm_gt [ProperSpace E] :
    IsTightMeasureSet S ↔ Tendsto (fun r : ℝ ↦ ⨆ μ ∈ S, μ {x | r < ‖x‖}) atTop (𝓝 0) :=
  ⟨tendsto_measure_norm_gt_of_isTightMeasureSet, isTightMeasureSet_of_tendsto_measure_norm_gt⟩

Похожие утверждения