Truncated Dudley inequality for a finite terminal net with a fixed root

This module contains the finite, fixed-root, terminal-net-supremum form of the truncated Dudley chaining inequality and the dense-sequence full-supremum endpoint. The separate DudleyFull module builds a full consumer from every-sample uniform continuity instead. This file proves no Gaussian functional inequality.

The chain of arguments is:

• pointwise terminal-net chaining with a common root (HighDimProb.sup'_abs_sub_root_le_sum_level_sup), so the supremum bound is proved pointwise before any integration;
• integration by monotonicity, giving the expectation of the terminal-net supremum by the sum of the expected per-level suprema;
• the finite-maximum subGaussian bound on each level;
• a rooted dyadic net chain constructed internally from total boundedness, with base level the singleton {t₀} (an internal R-net of K by the radius hypothesis), minimal internal nets at the finer dyadic scales, and parent maps into the previous level;
• the existing dyadic finite-entropy-sum to truncated covering-number integral comparison.

The high-level consumer Dudley.truncatedBound only asks for the metric hypotheses on K, t₀, R, the subGaussian increment scale, and measurability; the nets, parent maps, covering-number equalities, and finiteness facts are constructed internally.

The module also retains the dense-sequence endpoint dudleyEntropyIntegral, whose continuous-path contract is independent of the uniformly-continuous finite-net endpoint exposed through DudleyFull.

theorem HighDimProb.dudleyEntropyIntegral {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} {K : Set α} {R σ : ℝ} (u : ℕ → ↑K) (hu : DenseRange u) (anchor : ↑K) (hAnchorNet : IsInternalEpsilonNet K {↑anchor} R) (hK : TotallyBounded K) (hXMeas : ∀ (x : α), Measurable (X x)) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) (hR : 0 < R) (hPathCont : ∀ (ω : Ω), Continuous fun (x : ↑K) => X (↑x) ω) (hPathBdd : ∀ (ω : Ω), BddAbove (Set.range fun (x : ↑K) => |X (↑x) ω - X (↑anchor) ω|)) (hFullIntegrable : IntegrableRealRandomVariable P fun (ω : Ω) => ⨆ (x : ↑K), |X (↑x) ω - X (↑anchor) ω|) (hEntropyIntegrable : IntervalIntegrable (fun (t : ℝ) => √(2 * Real.log (2 * ↑(coveringNumber K t).toNat))) MeasureTheory.volume 0 R) : (expect P fun (ω : Ω) => ⨆ (x : ↑K), |X (↑x) ω - X (↑anchor) ω|) ≤ 4 * σ * ∫ (t : ℝ) in 0..R, √(2 * Real.log (2 * ↑(coveringNumber K t).toNat))

Dudley's entropy-integral bound for the anchored supremum of a subGaussian process over a totally bounded index set.

The theorem uses internal covering numbers. Its explicit boundary assumptions are a dense sequence in K, an anchor whose singleton is an R-net for K, sample-path continuity and boundedness on K, integrability of the full anchored supremum, and interval integrability of the entropy integrand at zero.

theorem HighDimProb.Dudley.Internal.expect_sup'_abs_sub_root_le_sum_level_sup {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : RandomProcess Ω α ℝ} {L : ℕ} {levels : Fin (L + 1) → Finset α} {parent : Fin L → α → α} {t₀ : α} (hroot : ∀ y ∈ levels 0, y = t₀) (hparent_mem : ∀ (k : Fin L), ∀ x ∈ levels k.succ, parent k x ∈ levels k.castSucc) (hne : ∀ (k : Fin L), (levels k.succ).Nonempty) (hT : (levels (Fin.last L)).Nonempty) (hLevelInt : ∀ (k : Fin L), IntegrableRealRandomVariable P fun (ω : Ω) => (levels k.succ).sup' ⋯ fun (y : α) => |X y ω - X (parent k y) ω|) : (expect P fun (ω : Ω) => (levels (Fin.last L)).sup' hT fun (x : α) => |X x ω - X t₀ ω|) ≤ ∑ k : Fin L, expect P fun (ω : Ω) => (levels k.succ).sup' ⋯ fun (y : α) => |X y ω - X (parent k y) ω|

Expectation of the terminal-net supremum is bounded by the sum of the expected per-level parent-increment suprema, with the fixed common root t₀.

The pointwise bound is established first (sup'_abs_sub_root_le_sum_level_sup), then integrated by monotonicity.

theorem HighDimProb.Dudley.Internal.expect_sup'_abs_sub_root_le_finiteEntropySum {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} {L : ℕ} {levels : Fin (L + 1) → Finset α} {parent : Fin L → α → α} {t₀ : α} {σ : ℝ} {rho : Fin (L + 1) → ℝ} (hroot : ∀ y ∈ levels 0, y = t₀) (hparent_mem : ∀ (k : Fin L), ∀ x ∈ levels k.succ, parent k x ∈ levels k.castSucc) (hparent_dist : ∀ (k : Fin L), ∀ x ∈ levels k.succ, dist x (parent k x) ≤ rho k.castSucc) (hne : ∀ (k : Fin L), (levels k.succ).Nonempty) (hT : (levels (Fin.last L)).Nonempty) (hXMeas : ∀ (t : α), Measurable (X t)) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) (hρ : ∀ (j : Fin (L + 1)), 0 < rho j) : (expect P fun (ω : Ω) => (levels (Fin.last L)).sup' hT fun (x : α) => |X x ω - X t₀ ω|) ≤ finiteEntropySum rho (fun (k : Fin L) => (levels k.succ).card) σ

Terminal-net supremum expectation bound for subGaussian-increment processes, summed into the finite entropy sum of the level cardinalities.

theorem HighDimProb.Dudley.truncatedBound {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} {K : Set α} {t₀ : α} {R σ : ℝ} (L : ℕ) (hK : TotallyBounded K) (ht₀ : t₀ ∈ K) (hR : 0 < R) (hdist : ∀ t ∈ K, dist t t₀ ≤ R) (hXMeas : ∀ (t : α), Measurable (X t)) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) : ∃ (T : Finset α) (hT : T.Nonempty), ↑T ⊆ K ∧ IsInternalEpsilonNet K (↑T) (dyadicRadius R L) ∧ (expect P fun (ω : Ω) => T.sup' hT fun (t : α) => |X t ω - X t₀ ω|) ≤ 4 * σ * ∫ (t : ℝ) in dyadicRadius R (L + 1)..R, √(2 * Real.log (2 * ↑(coveringNumber K t).toNat))

Truncated Dudley inequality for a finite terminal net with a fixed root.

From totally bounded K, a root t₀ ∈ K within radius R of every point of K, subGaussian increments of scale σ > 0, and measurability of the process, there exists a finite internal terminal net T of K at scale dyadicRadius R L such that the expected supremum of |X t - X t₀| over T is bounded by the truncated covering-number entropy integral.

The chain is built internally: the base level is the singleton {t₀} (an internal R-net of K by the radius hypothesis), the finer levels are minimal internal dyadic nets (so their cardinalities equal the covering numbers), and the parent maps point into the previous level. The caller supplies no paths, parents, level cardinalities, or finiteness facts.