Stochastic processes satisfying the Kolmogorov condition #
theorem
Finset.iSup_sum_le
{α : Type u_1}
{ι : Type u_2}
{β : Sort u_3}
[CompleteLattice α]
[AddCommMonoid α]
[IsOrderedAddMonoid α]
{I : Finset ι}
(f : ι → β → α)
:
theorem
Finset.sup_le_sum
{α : Type u_1}
{β : Type u_2}
[AddCommMonoid β]
[LinearOrder β]
[OrderBot β]
[IsOrderedAddMonoid β]
(s : Finset α)
(f : α → β)
(hfs : ∀ i ∈ s, 0 ≤ f i)
:
structure
ProbabilityTheory.IsMeasurableKolmogorovProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
(X : T → Ω → E)
(P : MeasureTheory.Measure Ω)
(p q : ℝ)
(M : NNReal)
:
- measurablePair (s t : T) : Measurable fun (ω : Ω) => (X s ω, X t ω)
Instances For
def
ProbabilityTheory.IsKolmogorovProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
(X : T → Ω → E)
(P : MeasureTheory.Measure Ω)
(p q : ℝ)
(M : NNReal)
:
Equations
- ProbabilityTheory.IsKolmogorovProcess X P p q M = ∃ (Y : T → Ω → E), ProbabilityTheory.IsMeasurableKolmogorovProcess Y P p q M ∧ ∀ (t : T), X t =ᵐ[P] Y t
Instances For
noncomputable def
ProbabilityTheory.IsKolmogorovProcess.mk
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
(X : T → Ω → E)
(h : IsKolmogorovProcess X P p q M)
:
T → Ω → E
Equations
Instances For
theorem
ProbabilityTheory.IsKolmogorovProcess.isMeasurableKolmogorovProcess_mk
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(h : IsKolmogorovProcess X P p q M)
:
IsMeasurableKolmogorovProcess (mk X h) P p q M
theorem
ProbabilityTheory.IsKolmogorovProcess.ae_eq_mk
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(h : IsKolmogorovProcess X P p q M)
(t : T)
:
theorem
ProbabilityTheory.IsKolmogorovProcess.congr
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X Y : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
(h : ∀ (t : T), X t =ᵐ[P] Y t)
:
IsKolmogorovProcess Y P p q M
theorem
ProbabilityTheory.IsMeasurableKolmogorovProcess.isKolmogorovProcess
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsMeasurableKolmogorovProcess X P p q M)
:
IsKolmogorovProcess X P p q M
theorem
ProbabilityTheory.IsKolmogorovProcess.kolmogorovCondition
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
(s t : T)
:
theorem
ProbabilityTheory.IsMeasurableKolmogorovProcess.measurable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[BorelSpace E]
(hX : IsMeasurableKolmogorovProcess X P p q M)
(s : T)
:
Measurable (X s)
theorem
ProbabilityTheory.IsKolmogorovProcess.aemeasurable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[BorelSpace E]
(hX : IsKolmogorovProcess X P p q M)
(s : T)
:
AEMeasurable (X s) P
theorem
ProbabilityTheory.measurable_pair_of_measurable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{X : T → Ω → E}
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
(hX : ∀ (s : T), Measurable (X s))
(s t : T)
:
Measurable fun (ω : Ω) => (X s ω, X t ω)
theorem
ProbabilityTheory.aemeasurable_pair_of_aemeasurable
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
(hX : ∀ (s : T), AEMeasurable (X s) P)
(s t : T)
:
AEMeasurable (fun (ω : Ω) => (X s ω, X t ω)) P
theorem
ProbabilityTheory.IsMeasurableKolmogorovProcess.mk_of_secondCountableTopology
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
(h_meas : ∀ (s : T), Measurable (X s))
(h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q)
:
IsMeasurableKolmogorovProcess X P p q M
theorem
ProbabilityTheory.IsMeasurableKolmogorovProcess.stronglyMeasurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsMeasurableKolmogorovProcess X P p q M)
{s t : T}
:
MeasureTheory.StronglyMeasurable fun (ω : Ω) => edist (X s ω) (X t ω)
theorem
ProbabilityTheory.IsKolmogorovProcess.aestronglyMeasurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
{s t : T}
:
MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => edist (X s ω) (X t ω)) P
theorem
ProbabilityTheory.IsMeasurableKolmogorovProcess.measurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsMeasurableKolmogorovProcess X P p q M)
{s t : T}
:
Measurable fun (ω : Ω) => edist (X s ω) (X t ω)
theorem
ProbabilityTheory.IsKolmogorovProcess.aemeasurable_edist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
{s t : T}
:
AEMeasurable (fun (ω : Ω) => edist (X s ω) (X t ω)) P
theorem
ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
(hp : 0 < p)
(hq : 0 < q)
{s t : T}
(h : edist s t = 0)
:
theorem
ProbabilityTheory.IsKolmogorovProcess.edist_eq_zero_of_M_eq_zero
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q 0)
(hp : 0 < p)
{s t : T}
:
theorem
ProbabilityTheory.IsKolmogorovProcess.lintegral_sup_rpow_edist_eq_zero
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
(hp : 0 < p)
(hq : 0 < q)
{T' : Set T}
(hT' : T'.Countable)
(h : ∀ s ∈ T', ∀ t ∈ T', edist s t = 0)
:
theorem
ProbabilityTheory.IsKolmogorovProcess.lintegral_sup_rpow_edist_eq_zero'
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hX : IsKolmogorovProcess X P p q M)
(hp : 0 < p)
(hq : 0 < q)
{J : Set T}
(hJ : J.Countable)
{δ : ENNReal}
(h : ∀ (s : ↑J) (t : { t : ↑J // edist s t ≤ δ }), edist s ↑t = 0)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_card_mul_rpow
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hq : 0 ≤ q)
(hX : IsKolmogorovProcess X P p q M)
{ε : ENNReal}
(C : Finset (T × T))
(hC : ∀ u ∈ C, edist u.1 u.2 ≤ ε)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_card_mul_rpow_of_dist_le
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
(hp : 0 < p)
(hq : 0 ≤ q)
(hX : IsKolmogorovProcess X P p q M)
{J : Finset T}
{a c : ENNReal}
{n : ℕ}
(hJ_card : ↑J.card ≤ a ^ n)
(ha : 1 < a)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_cover_of_dist_le
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
(hp : 0 < p)
(hq : 0 ≤ q)
(hX : IsKolmogorovProcess X P p q M)
{C : Finset T}
{ε : ENNReal}
(hC_card : ↑C.card = internalCoveringNumber ε J)
{c : ENNReal}
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_cover_rescale
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
(hp : 0 < p)
(hq : 0 ≤ q)
(hX : IsKolmogorovProcess X P p q M)
(hJ : J.Finite)
{C : ℕ → Finset T}
{ε₀ : ENNReal}
(hε₀ : ε₀ ≠ ⊤)
(hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε₀ * 2⁻¹ ^ i) J)
(hC_subset : ∀ (i : ℕ), ↑(C i) ⊆ J)
(hC_card : ∀ (i : ℕ), ↑(C i).card = internalCoveringNumber (ε₀ * 2⁻¹ ^ i) J)
{δ : ENNReal}
(hδ_pos : 0 < δ)
(hδ_le : δ ≤ ε₀ * 4)
{k m : ℕ}
(hm₁ : ε₀ * 2⁻¹ ^ m ≤ δ)
(hm₂ : δ ≤ ε₀ * 4 * 2⁻¹ ^ m)
(hmk : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_succ
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{ε : ℕ → ENNReal}
{j k : ℕ}
(hq : 0 ≤ q)
(hX : IsKolmogorovProcess X P p q M)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J)
(hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J)
(hjk : j < k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_sum_rpow
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{ε : ℕ → ENNReal}
{k m : ℕ}
(hp : 1 ≤ p)
(hX : IsKolmogorovProcess X P p q M)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_sum
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{ε : ℕ → ENNReal}
{k m : ℕ}
(hp : 1 ≤ p)
(hX : IsKolmogorovProcess X P p q M)
(hq : 0 ≤ q)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J)
(hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_of_minimal_cover
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{ε : ℕ → ENNReal}
{k m : ℕ}
(hp : 1 ≤ p)
(hX : IsKolmogorovProcess X P p q M)
(hε : ∀ (n : ℕ), ε n ≤ EMetric.diam J)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J)
(hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J)
(hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε n) J)
{c₁ : ENNReal}
{d : ℝ}
(hd_pos : 0 < d)
(hdq : d ≤ q)
(h_cov : HasBoundedInternalCoveringNumber J c₁ d)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_of_minimal_cover_two
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{k m : ℕ}
(hp : 1 ≤ p)
(hX : IsKolmogorovProcess X P p q M)
{ε₀ : ENNReal}
(hε : ε₀ ≤ EMetric.diam J)
(hε' : ε₀ ≠ ⊤)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε₀ * 2⁻¹ ^ n) J)
(hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J)
(hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε₀ * 2⁻¹ ^ n) J)
{c₁ : ENNReal}
{d : ℝ}
(hd_pos : 0 < d)
(hdq : d < q)
(h_cov : HasBoundedInternalCoveringNumber J c₁ d)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_sum_rpow_of_le_one
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{ε : ℕ → ENNReal}
{k m : ℕ}
(hp_pos : 0 < p)
(hp : p ≤ 1)
(hX : IsKolmogorovProcess X P p q M)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_sum_of_le_one
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{ε : ℕ → ENNReal}
{k m : ℕ}
(hp_pos : 0 < p)
(hp : p ≤ 1)
(hq : 0 ≤ q)
(hX : IsKolmogorovProcess X P p q M)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J)
(hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_of_minimal_cover_of_le_one
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{ε : ℕ → ENNReal}
{k m : ℕ}
(hp_pos : 0 < p)
(hp : p ≤ 1)
(hX : IsKolmogorovProcess X P p q M)
(hε : ∀ (n : ℕ), ε n ≤ EMetric.diam J)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε n) J)
(hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J)
(hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε n) J)
{c₁ : ENNReal}
{d : ℝ}
(hd_pos : 0 < d)
(hdq : d ≤ q)
(h_cov : HasBoundedInternalCoveringNumber J c₁ d)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_rpow_edist_le_of_minimal_cover_two_of_le_one
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{k m : ℕ}
(hp_pos : 0 < p)
(hp : p ≤ 1)
(hX : IsKolmogorovProcess X P p q M)
{ε₀ : ENNReal}
(hε : ε₀ ≤ EMetric.diam J)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε₀ * 2⁻¹ ^ n) J)
(hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J)
(hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε₀ * 2⁻¹ ^ n) J)
{c₁ : ENNReal}
{d : ℝ}
(hd_pos : 0 < d)
(hdq : d < q)
(h_cov : HasBoundedInternalCoveringNumber J c₁ d)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.second_term_bound
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{p q : ℝ}
{M : NNReal}
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{J : Set T}
{C : ℕ → Finset T}
{k m : ℕ}
(hp_pos : 0 < p)
(hX : IsKolmogorovProcess X P p q M)
{ε₀ : ENNReal}
(hε : ε₀ ≤ EMetric.diam J)
(hC : ∀ (n : ℕ), IsCover (↑(C n)) (ε₀ * 2⁻¹ ^ n) J)
(hC_subset : ∀ (n : ℕ), ↑(C n) ⊆ J)
(hC_card : ∀ (n : ℕ), ↑(C n).card = internalCoveringNumber (ε₀ * 2⁻¹ ^ n) J)
{c₁ : ENNReal}
{d : ℝ}
(hd_pos : 0 < d)
(hdq : d < q)
(h_cov : HasBoundedInternalCoveringNumber J c₁ d)
(hm : m ≤ k)
:
theorem
ProbabilityTheory.lintegral_sup_cover_eq_of_lt_iInf_dist
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{M : NNReal}
{p q : ℝ}
{J : Set T}
{δ : ENNReal}
{C : Finset T}
{ε : ENNReal}
(hX : IsKolmogorovProcess X P p q M)
(hp : 0 < p)
(hq : 0 < q)
(hJ : J.Finite)
(hC : IsCover (↑C) ε J)
(hC_subset : ↑C ⊆ J)
(hε_lt : ε < ⨅ (s : ↑J), ⨅ (t : ↑J), ⨅ (_ : 0 < edist s t), edist s t)
:
theorem
ProbabilityTheory.exists_nat_pow_lt_iInf
{T : Type u_1}
[PseudoEMetricSpace T]
{J : Set T}
(hJ : EMetric.diam J < ⊤)
(hJ_finite : J.Finite)
(hJ_nonempty : J.Nonempty)
:
theorem
ProbabilityTheory.scale_change_lintegral_iSup
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{M : NNReal}
{p q : ℝ}
{J : Set T}
{C : ℕ → Finset T}
{ε : ℕ → ENNReal}
(hC : ∀ (i : ℕ), IsCover (↑(C i)) (ε i) J)
(hX : IsKolmogorovProcess X P p q M)
(hp : 0 ≤ p)
(δ : ENNReal)
(m k : ℕ)
:
∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C k }),
⨆ (t : { t : { x : T // x ∈ C k } // edist s t ≤ δ }), edist (X (↑s) ω) (X (↑↑t) ω) ^ p ∂P ≤ 2 ^ p * ∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C k }),
⨆ (t : { t : { x : T // x ∈ C k } // edist s t ≤ δ }),
edist (X (chainingSequence hC ⋯ m) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P + 4 ^ p * ∫⁻ (ω : Ω), ⨆ (s : { x : T // x ∈ C k }), edist (X (↑s) ω) (X (chainingSequence hC ⋯ m) ω) ^ p ∂P
theorem
ProbabilityTheory.finite_set_bound_of_edist_le_of_diam_le
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{M : NNReal}
{d p q : ℝ}
{J : Set T}
{c δ : ENNReal}
(hJ : HasBoundedInternalCoveringNumber J c d)
(hJ_finite : J.Finite)
(hX : IsKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(hp_pos : 0 < p)
(hdq_lt : d < q)
(hδ_le : EMetric.diam J ≤ δ / 4)
:
theorem
ProbabilityTheory.finite_set_bound_of_edist_le_of_le_diam
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{M : NNReal}
{d p q : ℝ}
{J : Set T}
{c δ : ENNReal}
(hJ : HasBoundedInternalCoveringNumber J c d)
(hJ_finite : J.Finite)
(hX : IsKolmogorovProcess X P p q M)
(hd_pos : 0 < d)
(hp_pos : 0 < p)
(hdq_lt : d < q)
(hδ : δ ≠ 0)
(hδ_le : δ / 4 ≤ EMetric.diam J)
:
theorem
ProbabilityTheory.finite_set_bound_of_edist_le_of_le_diam'
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{M : NNReal}
{d p q : ℝ}
{J : Set T}
{c δ : ENNReal}
(hJ : HasBoundedInternalCoveringNumber J c d)
(hJ_finite : J.Finite)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hp_pos : 0 < p)
(hdq_lt : d < q)
(hδ : δ ≠ 0)
(hδ_le : δ / 4 ≤ EMetric.diam J)
:
theorem
ProbabilityTheory.finite_set_bound_of_edist_le
{T : Type u_1}
{Ω : Type u_2}
{E : Type u_3}
[PseudoEMetricSpace T]
{mΩ : MeasurableSpace Ω}
[PseudoEMetricSpace E]
{P : MeasureTheory.Measure Ω}
{X : T → Ω → E}
{M : NNReal}
{d p q : ℝ}
{J : Set T}
{c δ : ENNReal}
(hJ : HasBoundedInternalCoveringNumber J c d)
(hJ_finite : J.Finite)
(hX : IsKolmogorovProcess X P p q M)
(hc : c ≠ ⊤)
(hd_pos : 0 < d)
(hp_pos : 0 < p)
(hdq_lt : d < q)
(hδ : δ ≠ 0)
: