Theorems · Theorem · probability

ProbabilityTheory.Kernel.le_lmarginalPartialTraj_succ

∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {f : ℕ → ((n : ℕ) → X n) → ENNReal} {a : ℕ → ℕ},
  (∀ (n : ℕ), DependsOn (f n) ↑(Finset.Iic (a n))) →
    (∀ (n : ℕ), Measurable (f n)) →
      ∀ {bound : ENNReal},
        bound ≠ ⊤ →
          (∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound) →
            ∀ {k : ℕ},
              (∀ (x : (n : ℕ) → X n),
                  Antitone fun n => ProbabilityTheory.Kernel.lmarginalPartialTraj κ (k + 1) (a n) (f n) x) →
                ∀ {l : ((n : ℕ) → X n) → ENNReal},
                  (∀ (x : (n : ℕ) → X n),
                      Filter.Tendsto (fun n => ProbabilityTheory.Kernel.lmarginalPartialTraj κ (k + 1) (a n) (f n) x)
                        Filter.atTop (nhds (l x))) →
                    ∀ (ε : ENNReal) (y : (i : ↥(Finset.Iic k)) → X ↑i),
                      (∀ (x : (i : ℕ) → X i) (n : ℕ),
                          ε ≤
                            ProbabilityTheory.Kernel.lmarginalPartialTraj κ k (a n) (f n)
                              (Function.updateFinset x (Finset.Iic k) y)) →
                        ∃ z,
                          ∀ (x : (i : ℕ) → X i) (n : ℕ),
                            ε ≤
                              ProbabilityTheory.Kernel.lmarginalPartialTraj κ (k + 1) (a n) (f n)
                                (Function.update (Function.updateFinset x (Finset.Iic k) y) (k + 1) z)

This is an auxiliary result for trajContent_tendsto_zero. Consider f a sequence of bounded measurable functions such that f n depends only on the first coordinates up to a n. Assume that when integrating f n against partialTraj (k + 1) (a n), one gets a non-increasing sequence of functions which converges to l. Assume then that there exists ε and y : Π i : Iic k, X i such that when integrating f n against partialTraj k (a n) y, you get something at least ε for all n. Then there exists z such that this remains true when integrating f against partialTraj (k + 1) (a n) (update y (k + 1) z).

Defined in

Mathlib.Probability.Kernel.IonescuTulcea.Traj

Cited by

1 results in Mathlib

Foundations

Depth 263 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MeasurableSpaceProbabilityTheory.IsMarkovKernel