Finite maxima of centered subGaussian processes

This module specializes the fixed-parameter finite-maximum bound to a common Mathlib subGaussian MGF scale and evaluates it at the optimized parameter.

theorem HighDimProb.expect_processSup_le_of_centeredSubGaussianMGF {Omega : Type u_1} {T : Type u_2} [MeasurableSpace Omega] {P : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Omega T ℝ} {s : Finset T} (hs : s.Nonempty) (hs_card : 2 ≤ s.card) {K : ℝ} (hXMeas : ∀ t ∈ s, Measurable (X t)) (hXSG : ∀ t ∈ s, CenteredSubGaussianMGF P (X t) K) : expect P (processSup X s hs) ≤ K * √(2 * Real.log ↑s.card)

Expected finite-process maximum bound for a common centered subGaussian scale.

The MGF and exponential-integrability obligations are discharged directly from Mathlib's HasSubgaussianMGF fields.

theorem HighDimProb.expect_finset_sup'_abs_le_of_centeredSubGaussianMGF {Ω : Type u_1} {T : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω T ℝ} {s : Finset T} (hs : s.Nonempty) {K : ℝ} (hXMeas : ∀ t ∈ s, Measurable (X t)) (hXSG : ∀ t ∈ s, CenteredSubGaussianMGF P (X t) K) : (expect P fun (ω : Ω) => s.sup' hs fun (t : T) => |X t ω|) ≤ K * √(2 * Real.log (2 * ↑s.card))

Expected finite supremum of absolute values for a centered subGaussian process.

theorem HighDimProb.expect_abs_sub_chain_le_sum_of_level_sup_of_centeredSubGaussianMGF {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} (gamma : ℕ → α) (L : ℕ) (nextLevel : Fin L → Finset α) (parent : Fin L → α → α) (K : Fin L → ℝ) (hmem : ∀ (k : Fin L), gamma (↑k + 1) ∈ nextLevel k) (hparent : ∀ (k : Fin L), gamma ↑k = parent k (gamma (↑k + 1))) (hXMeas : ∀ (k : Fin L), ∀ x ∈ nextLevel k, Measurable fun (ω : Ω) => X x ω - X (parent k x) ω) (hXSG : ∀ (k : Fin L), ∀ x ∈ nextLevel k, CenteredSubGaussianMGF P (fun (ω : Ω) => X x ω - X (parent k x) ω) (K k)) : (expect P fun (ω : Ω) => |X (gamma L) ω - X (gamma 0) ω|) ≤ ∑ k : Fin L, K k * √(2 * Real.log (2 * ↑(nextLevel k).card))

Expected finite chaining bound for centered subGaussian increments.

theorem HighDimProb.expect_abs_sub_chain_le_sum_of_level_sup_of_subGaussianMGFIncrements {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} (gamma : ℕ → α) (L : ℕ) (nextLevel : Fin L → Finset α) (parent : Fin L → α → α) (σ : ℝ) (r : Fin L → ℝ) (hmem : ∀ (k : Fin L), gamma (↑k + 1) ∈ nextLevel k) (hparent : ∀ (k : Fin L), gamma ↑k = parent k (gamma (↑k + 1))) (hXMeas : ∀ (k : Fin L), ∀ x ∈ nextLevel k, Measurable fun (ω : Ω) => X x ω - X (parent k x) ω) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) (hr : ∀ (k : Fin L), 0 < r k) (hdist : ∀ (k : Fin L), ∀ x ∈ nextLevel k, dist x (parent k x) ≤ r k) : (expect P fun (ω : Ω) => |X (gamma L) ω - X (gamma 0) ω|) ≤ ∑ k : Fin L, σ * r k * √(2 * Real.log (2 * ↑(nextLevel k).card))

Expected finite chaining bound from metric subGaussian increments and level radii.

theorem HighDimProb.expect_abs_sub_chain_le_sum_of_level_sup_of_centeredSubGaussianMGF_of_card_le {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} (gamma : ℕ → α) (L : ℕ) (nextLevel : Fin L → Finset α) (parent : Fin L → α → α) (K : Fin L → ℝ) (N : Fin L → ℕ) (hmem : ∀ (k : Fin L), gamma (↑k + 1) ∈ nextLevel k) (hparent : ∀ (k : Fin L), gamma ↑k = parent k (gamma (↑k + 1))) (hXMeas : ∀ (k : Fin L), ∀ x ∈ nextLevel k, Measurable fun (ω : Ω) => X x ω - X (parent k x) ω) (hXSG : ∀ (k : Fin L), ∀ x ∈ nextLevel k, CenteredSubGaussianMGF P (fun (ω : Ω) => X x ω - X (parent k x) ω) (K k)) (hcard : ∀ (k : Fin L), (nextLevel k).card ≤ N k) : (expect P fun (ω : Ω) => |X (gamma L) ω - X (gamma 0) ω|) ≤ ∑ k : Fin L, K k * √(2 * Real.log (2 * ↑(N k)))

Expected finite chaining bound with cardinality upper bounds.

theorem HighDimProb.expect_abs_sub_chain_le_finiteEntropySum {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} (gamma : ℕ → α) (L : ℕ) (nextLevel : Fin L → Finset α) (parent : Fin L → α → α) (σ : ℝ) (rho : Fin (L + 1) → ℝ) (N : Fin L → ℕ) (hmem : ∀ (k : Fin L), gamma (↑k + 1) ∈ nextLevel k) (hparent : ∀ (k : Fin L), gamma ↑k = parent k (gamma (↑k + 1))) (hXMeas : ∀ (k : Fin L), ∀ x ∈ nextLevel k, Measurable fun (ω : Ω) => X x ω - X (parent k x) ω) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) (hρ : ∀ (j : Fin (L + 1)), 0 < rho j) (hdist : ∀ (k : Fin L), ∀ x ∈ nextLevel k, dist x (parent k x) ≤ rho k.castSucc) (hcard : ∀ (k : Fin L), (nextLevel k).card = N k) : (expect P fun (ω : Ω) => |X (gamma L) ω - X (gamma 0) ω|) ≤ finiteEntropySum rho N σ

Finite chaining bound written with an explicit natural cardinality family.

theorem HighDimProb.expect_abs_sub_chain_le_finiteEntropySum_of_path {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} {L : ℕ} (path : Fin (L + 1) → α) (nextLevel : Fin L → Finset α) (parent : Fin L → α → α) (σ : ℝ) (rho : Fin (L + 1) → ℝ) (N : Fin L → ℕ) (hmem : ∀ (k : Fin L), path k.succ ∈ nextLevel k) (hparent : ∀ (k : Fin L), path k.castSucc = parent k (path k.succ)) (hXMeas : ∀ (k : Fin L), ∀ x ∈ nextLevel k, Measurable fun (ω : Ω) => X x ω - X (parent k x) ω) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) (hρ : ∀ (j : Fin (L + 1)), 0 < rho j) (hdist : ∀ (k : Fin L), ∀ x ∈ nextLevel k, dist x (parent k x) ≤ rho k.castSucc) (hcard : ∀ (k : Fin L), (nextLevel k).card = N k) : (expect P fun (ω : Ω) => |X (path (Fin.last L)) ω - X (path 0) ω|) ≤ finiteEntropySum rho N σ

Finite chaining bound for a path indexed by Fin (L + 1).

theorem HighDimProb.expect_finset_sup'_abs_sub_anchor_le_finiteEntropySum {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} {L : ℕ} (s : Finset α) (hs : s.Nonempty) (path : α → Fin (L + 1) → α) (nextLevel : Fin L → Finset α) (parent : Fin L → α → α) (anchor : α) (residual : RealRandomVariable Ω) (σ : ℝ) (rho : Fin (L + 1) → ℝ) (hmem : ∀ x ∈ s, ∀ (k : Fin L), path x k.succ ∈ nextLevel k) (hparent : ∀ x ∈ s, ∀ (k : Fin L), path x k.castSucc = parent k (path x k.succ)) (hresidual : ∀ x ∈ s, ∀ (ω : Ω), |X x ω - X (path x (Fin.last L)) ω| ≤ residual ω) (hanchor : ∀ x ∈ s, path x 0 = anchor) (hXMeas : ∀ (k : Fin L), ∀ x ∈ nextLevel k, Measurable fun (ω : Ω) => X x ω - X (parent k x) ω) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) (hρ : ∀ (j : Fin (L + 1)), 0 < rho j) (hdist : ∀ (k : Fin L), ∀ x ∈ nextLevel k, dist x (parent k x) ≤ rho k.castSucc) (hresidualIntegrable : IntegrableRealRandomVariable P residual) : (expect P fun (ω : Ω) => s.sup' hs fun (x : α) => |X x ω - X anchor ω|) ≤ expect P residual + finiteEntropySum rho (fun (k : Fin L) => (nextLevel k).card) σ

Expected finite anchored supremum bound with an explicit terminal residual.

theorem HighDimProb.expect_finset_sup'_abs_sub_anchor_le_truncatedEntropyIntegral {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} {K : Set α} {L : ℕ} {R σ : ℝ} (s : Finset α) (hs : s.Nonempty) (path : α → Fin (L + 1) → α) (nextLevel : Fin L → Finset α) (parent : Fin L → α → α) (anchor : α) (residual : RealRandomVariable Ω) (hmem : ∀ x ∈ s, ∀ (k : Fin L), path x k.succ ∈ nextLevel k) (hparent : ∀ x ∈ s, ∀ (k : Fin L), path x k.castSucc = parent k (path x k.succ)) (hresidual : ∀ x ∈ s, ∀ (ω : Ω), |X x ω - X (path x (Fin.last L)) ω| ≤ residual ω) (hanchor : ∀ x ∈ s, path x 0 = anchor) (hXMeas : ∀ (k : Fin L), ∀ x ∈ nextLevel k, Measurable fun (ω : Ω) => X x ω - X (parent k x) ω) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) (hR : 0 < R) (hdist : ∀ (k : Fin L), ∀ x ∈ nextLevel k, dist x (parent k x) ≤ dyadicRadius R ↑k.castSucc) (hN : ∀ (k : Fin L), coveringNumber K (dyadicRadius R (↑k + 1)) = ↑(nextLevel k).card) (hfinite : coveringNumber K (dyadicRadius R (L + 1)) ≠ ⊤) (hresidualIntegrable : IntegrableRealRandomVariable P residual) : (expect P fun (ω : Ω) => s.sup' hs fun (x : α) => |X x ω - X anchor ω|) ≤ expect P residual + 4 * σ * ∫ (t : ℝ) in dyadicRadius R (L + 1)..R, √(2 * Real.log (2 * ↑(coveringNumber K t).toNat))

Expected finite anchored supremum bound by a truncated entropy integral and an explicit terminal residual.

theorem HighDimProb.expect_abs_sub_dyadic_path_le_truncatedEntropyIntegral {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [PseudoMetricSpace α] {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {X : RandomProcess Ω α ℝ} {K : Set α} {L : ℕ} {R σ : ℝ} (path : Fin (L + 1) → α) (nextLevel : Fin L → Finset α) (parent : Fin L → α → α) (hmem : ∀ (k : Fin L), path k.succ ∈ nextLevel k) (hparent : ∀ (k : Fin L), path k.castSucc = parent k (path k.succ)) (hXMeas : ∀ (k : Fin L), ∀ x ∈ nextLevel k, Measurable fun (ω : Ω) => X x ω - X (parent k x) ω) (hX : HasSubGaussianMGFIncrements P X σ) (hσ : 0 < σ) (hR : 0 < R) (hdist : ∀ (k : Fin L), ∀ x ∈ nextLevel k, dist x (parent k x) ≤ dyadicRadius R ↑k.castSucc) (hN : ∀ (k : Fin L), coveringNumber K (dyadicRadius R (↑k + 1)) = ↑(nextLevel k).card) (hfinite : coveringNumber K (dyadicRadius R (L + 1)) ≠ ⊤) : (expect P fun (ω : Ω) => |X (path (Fin.last L)) ω - X (path 0) ω|) ≤ 4 * σ * ∫ (t : ℝ) in dyadicRadius R (L + 1)..R, √(2 * Real.log (2 * ↑(coveringNumber K t).toNat))

Finite dyadic chaining bound by the truncated covering-number entropy integral.

theorem HighDimProb.expect_iSup_abs_sub_anchor_le_of_denseRange_of_prefix_bound {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [TopologicalSpace α] {P : MeasureTheory.Measure Ω} {X : RandomProcess Ω α ℝ} (u : ℕ → α) (hu : DenseRange u) (anchor : α) (C : ℝ) (hAnchorMeas : Measurable (X anchor)) (hUmeas : ∀ (n : ℕ), Measurable (X (u n))) (hPathCont : ∀ (ω : Ω), Continuous fun (x : α) => |X x ω - X anchor ω|) (hPathBdd : ∀ (ω : Ω), BddAbove (Set.range fun (x : α) => |X x ω - X anchor ω|)) (hFullIntegrable : IntegrableRealRandomVariable P fun (ω : Ω) => ⨆ (x : α), |X x ω - X anchor ω|) (hPrefixBound : ∀ (n : ℕ), (expect P fun (ω : Ω) => (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => |X (u k) ω - X anchor ω|) ≤ C) : (expect P fun (ω : Ω) => ⨆ (x : α), |X x ω - X anchor ω|) ≤ C

Expected full anchored supremum from uniformly bounded finite prefixes. Continuity and boundedness identify the dense-sequence supremum, while monotone convergence passes the uniform prefix bound to the full expectation.

theorem HighDimProb.expect_iSup_abs_sub_anchor_le_mul_intervalIntegral_of_denseRange_of_prefix_bound {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [TopologicalSpace α] {P : MeasureTheory.Measure Ω} {X : RandomProcess Ω α ℝ} (u : ℕ → α) (hu : DenseRange u) (anchor : α) (c R : ℝ) (f : ℝ → ℝ) (residual : ℕ → ℕ → ℝ) (hAnchorMeas : Measurable (X anchor)) (hUmeas : ∀ (n : ℕ), Measurable (X (u n))) (hPathCont : ∀ (ω : Ω), Continuous fun (x : α) => |X x ω - X anchor ω|) (hPathBdd : ∀ (ω : Ω), BddAbove (Set.range fun (x : α) => |X x ω - X anchor ω|)) (hFullIntegrable : IntegrableRealRandomVariable P fun (ω : Ω) => ⨆ (x : α), |X x ω - X anchor ω|) (hR : 0 ≤ R) (hf : IntervalIntegrable f MeasureTheory.volume 0 R) (hResidualTendsto : ∀ (n : ℕ), Filter.Tendsto (residual n) Filter.atTop (nhds 0)) (hPrefixBound : ∀ (n m : ℕ), (expect P fun (ω : Ω) => (Finset.range (n + 1)).sup' ⋯ fun (k : ℕ) => |X (u k) ω - X anchor ω|) ≤ residual n m + c * ∫ (t : ℝ) in dyadicRadius R (m + 1)..R, f t) : (expect P fun (ω : Ω) => ⨆ (x : α), |X x ω - X anchor ω|) ≤ c * ∫ (t : ℝ) in 0..R, f t

The full anchored supremum is bounded by the limiting integral when finite prefixes have a vanishing residual and a dyadic truncated-integral bound.