theorem
HighDimProb.bddAbove_image_of_uniformContinuousOn_of_isInternalEpsilonNet
{alpha : Type u_1}
[PseudoMetricSpace alpha]
{K : Set alpha}
{T : ℕ → Finset alpha}
{eps : ℕ → ℝ}
{f : alpha → ℝ}
(hT : ∀ (n : ℕ), (T n).Nonempty)
(hnet : ∀ (n : ℕ), IsInternalEpsilonNet K (↑(T n)) (eps n))
(heps_pos : ∀ (n : ℕ), 0 < eps n)
(heps : Filter.Tendsto eps Filter.atTop (nhds 0))
(hf : UniformContinuousOn f K)
:
A shrinking positive internal-net family makes the image of a uniformly
continuous real function bounded above. The bound is supplied by one finite
net at a scale below the continuity modulus for tolerance 1.
theorem
HighDimProb.tendsto_finset_sup'_of_isInternalEpsilonNet
{alpha : Type u_1}
[PseudoMetricSpace alpha]
{K : Set alpha}
{T : ℕ → Finset alpha}
{eps : ℕ → ℝ}
{f : alpha → ℝ}
(hK : K.Nonempty)
(hT : ∀ (n : ℕ), (T n).Nonempty)
(hnet : ∀ (n : ℕ), IsInternalEpsilonNet K (↑(T n)) (eps n))
(heps_pos : ∀ (n : ℕ), 0 < eps n)
(heps : Filter.Tendsto eps Filter.atTop (nhds 0))
(hf : UniformContinuousOn f K)
(hfbdd : BddAbove (f '' K))
:
Filter.Tendsto (fun (n : ℕ) => (T n).sup' ⋯ f) Filter.atTop (nhds (sSup (f '' K)))
Finite internal-net suprema converge to the supremum on K. The
BddAbove premise is explicit because uniform continuity alone does not
bound a function on an arbitrary set.
theorem
HighDimProb.tendsto_finset_sup'_of_uniformContinuousOn_of_isInternalEpsilonNet
{alpha : Type u_1}
[PseudoMetricSpace alpha]
{K : Set alpha}
{T : ℕ → Finset alpha}
{eps : ℕ → ℝ}
{f : alpha → ℝ}
(hK : K.Nonempty)
(hT : ∀ (n : ℕ), (T n).Nonempty)
(hnet : ∀ (n : ℕ), IsInternalEpsilonNet K (↑(T n)) (eps n))
(heps_pos : ∀ (n : ℕ), 0 < eps n)
(heps : Filter.Tendsto eps Filter.atTop (nhds 0))
(hf : UniformContinuousOn f K)
:
Filter.Tendsto (fun (n : ℕ) => (T n).sup' ⋯ f) Filter.atTop (nhds (sSup (f '' K)))
The bounded-above premise in the core theorem follows from uniform continuity and the same shrinking positive internal-net family.
theorem
HighDimProb.tendsto_finset_sup'_abs_sub_of_uniformContinuousOn_of_isInternalEpsilonNet
{alpha : Type u_1}
[PseudoMetricSpace alpha]
{K : Set alpha}
{T : ℕ → Finset alpha}
{eps : ℕ → ℝ}
{f : alpha → ℝ}
{t0 : alpha}
(ht0 : t0 ∈ K)
(hT : ∀ (n : ℕ), (T n).Nonempty)
(hnet : ∀ (n : ℕ), IsInternalEpsilonNet K (↑(T n)) (eps n))
(heps_pos : ∀ (n : ℕ), 0 < eps n)
(heps : Filter.Tendsto eps Filter.atTop (nhds 0))
(hf : UniformContinuousOn f K)
:
Apply the supremum convergence theorem to the increment modulus rooted at
t0 ∈ K.