@[irreducible]

def iterate_induction {X : ℕ → Type u_1} {p : ℕ} (x₀ : (i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) (ind : (k : ℕ) → ((n : { x : ℕ // x ∈ Finset.Iic k }) → X ↑n) → X (k + 1)) (k : ℕ) : X k

This function takes a trajectory up to time p and a way of building the next step of the trajectory and returns a whole trajectory whose first steps correspond to the initial ones provided.

Equations

• One or more equations did not get rendered due to their size.

theorem iterate_induction_le {X : ℕ → Type u_1} {p : ℕ} (x₀ : (i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) (ind : (k : ℕ) → ((n : { x : ℕ // x ∈ Finset.Iic k }) → X ↑n) → X (k + 1)) (k : { x : ℕ // x ∈ Finset.Iic p }) : iterate_induction x₀ ind ↑k = x₀ k

theorem proj_updateFinset {X : ℕ → Type u_1} {n : ℕ} (x : (n : ℕ) → X n) (y : (i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) : Preorder.frestrictLe n (Function.updateFinset x (Finset.Iic n) y) = y

theorem aux {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {n : ℕ} (x₀ : (i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) : ⇑(el' n) ∘ Prod.mk x₀ ∘ (Set.Ioi n).restrict = fun (y : (i : ℕ) → X i) => Function.updateFinset y (Finset.Iic n) x₀

theorem isProjectiveLimit_nat_iff' {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (I : Finset ℕ) → MeasureTheory.Measure ((i : { x : ℕ // x ∈ I }) → X ↑i)) (hμ : MeasureTheory.IsProjectiveMeasureFamily μ) (ν : MeasureTheory.Measure ((n : ℕ) → X n)) (a : ℕ) : MeasureTheory.IsProjectiveLimit ν μ ↔ ∀ n ≥ a, MeasureTheory.Measure.map (Preorder.frestrictLe n) ν = μ (Finset.Iic n)

To check that a measure ν is the projective limit of a projective family of measures indexed by Finset ℕ, it is enough to check on intervals of the form Iic n, where n is larger than a given integer.

theorem isProjectiveLimit_nat_iff {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (I : Finset ℕ) → MeasureTheory.Measure ((i : { x : ℕ // x ∈ I }) → X ↑i)) (hμ : MeasureTheory.IsProjectiveMeasureFamily μ) (ν : MeasureTheory.Measure ((n : ℕ) → X n)) : MeasureTheory.IsProjectiveLimit ν μ ↔ ∀ (n : ℕ), MeasureTheory.Measure.map (Preorder.frestrictLe n) ν = μ (Finset.Iic n)

To check that a measure ν is the projective limit of a projective family of measures indexed by Finset ℕ, it is enough to check on intervals of the form Iic n.

noncomputable def inducedFamily {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i)) (S : Finset ℕ) : MeasureTheory.Measure ((k : { x : ℕ // x ∈ S }) → X ↑k)

Given a family of measures μ : (n : ℕ) → Measure ((i : Iic n) → X i), we can define a family of measures indexed by Finset ℕ by projecting the measures.

Equations

• inducedFamily μ S = MeasureTheory.Measure.map (Finset.restrict₂ ⋯) (μ (S.sup id))

instance instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i)) [∀ (n : ℕ), MeasureTheory.IsFiniteMeasure (μ n)] (I : Finset ℕ) : MeasureTheory.IsFiniteMeasure (inducedFamily μ I)

Equations

• ⋯ = ⋯

theorem inducedFamily_Iic {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i)) (n : ℕ) : inducedFamily μ (Finset.Iic n) = μ n

Given a family of measures μ : (n : ℕ) → Measure ((i : Iic n) → X i), the induced family equals μ over the intervals Iic n.

theorem isProjectiveMeasureFamily_inducedFamily {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ : (n : ℕ) → MeasureTheory.Measure ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i)) (h : ∀ (a b : ℕ) (hab : a ≤ b), MeasureTheory.Measure.map (Preorder.frestrictLe₂ hab) (μ b) = μ a) : MeasureTheory.IsProjectiveMeasureFamily (inducedFamily μ)

Given a family of measures μ : (n : ℕ) → Measure ((i : Iic n) → X i), the induced family will be projective only if μ is projective, in the sense that if a ≤ b, then projecting μ b gives μ a.

noncomputable def ionescuTulceaContent {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] {n : ℕ} (x : (i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) : MeasureTheory.AddContent (MeasureTheory.measurableCylinders X)

Given a family of kernels κ : (n : ℕ) → Kernel ((i : Iic n) → X i) (X (n + 1)), and the trajectory up to time n we can construct an additive content over cylinders. It corresponds to composing the kernels by starting at time n + 1.

Equations

• ionescuTulceaContent κ x = MeasureTheory.kolContent ⋯

theorem ionescuTulceaContent_cylinder {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] {a : ℕ} {b : ℕ} (x : (i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) {S : Set ((i : { x : ℕ // x ∈ Finset.Iic b }) → X ↑i)} (mS : MeasurableSet S) : (ionescuTulceaContent κ x) (MeasureTheory.cylinder (Finset.Iic b) S) = ((ProbabilityTheory.Kernel.partialKernel κ a b) x) S

The ionescuTulceaContent κ x of a cylinder indexed by first coordinates is given by partialKernel.

theorem ionescuTulceaContent_eq_lmarginalPartialKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] {N : ℕ} {S : Set ((i : { x : ℕ // x ∈ Finset.Iic N }) → X ↑i)} (mS : MeasurableSet S) (x : (n : ℕ) → X n) (n : ℕ) : (ionescuTulceaContent κ (Preorder.frestrictLe n x)) (MeasureTheory.cylinder (Finset.Iic N) S) = ProbabilityTheory.Kernel.lmarginalPartialKernel κ n N ((MeasureTheory.cylinder (Finset.Iic N) S).indicator 1) x

The ionescuTulceaContent of a cylinder is equal to the integral of its indicator function.

theorem cylinders_nat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] : MeasureTheory.measurableCylinders X = ⋃ (N : ℕ), ⋃ (S : Set ((i : { x : ℕ // x ∈ Finset.Iic N }) → X ↑i)), ⋃ (_ : MeasurableSet S), {MeasureTheory.cylinder (Finset.Iic N) S}

The cylinders of a product space indexed by ℕ can be seen as depending on the first corrdinates.

theorem le_lmarginalPartialKernel_succ {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] {f : ℕ → ((n : ℕ) → X n) → ENNReal} {N : ℕ → ℕ} (hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Finset.Iic (N n))) (mf : ∀ (n : ℕ), Measurable (f n)) {bound : ENNReal} (fin_bound : bound ≠ ⊤) (le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound) {k : ℕ} (anti : ∀ (x : (n : ℕ) → X n), Antitone fun (n : ℕ) => ProbabilityTheory.Kernel.lmarginalPartialKernel κ (k + 1) (N n) (f n) x) {l : ((n : ℕ) → X n) → ENNReal} (htendsto : ∀ (x : (n : ℕ) → X n), Filter.Tendsto (fun (n : ℕ) => ProbabilityTheory.Kernel.lmarginalPartialKernel κ (k + 1) (N n) (f n) x) Filter.atTop (nhds (l x))) (ε : ENNReal) (y : (n : { x : ℕ // x ∈ Finset.Iic k }) → X ↑n) (hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ ProbabilityTheory.Kernel.lmarginalPartialKernel κ k (N n) (f n) (Function.updateFinset x (Finset.Iic k) y)) : ∃ (z : X (k + 1)), ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ ProbabilityTheory.Kernel.lmarginalPartialKernel κ (k + 1) (N n) (f n) (Function.update (Function.updateFinset x (Finset.Iic k) y) (k + 1) z)

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

theorem dependsOn_cylinder_indicator {ι : Type u_2} {α : ι → Type u_3} {I : Finset ι} (S : Set ((i : { x : ι // x ∈ I }) → α ↑i)) : DependsOn ((MeasureTheory.cylinder I S).indicator 1) ↑I

The indicator of a cylinder only depends on the variables whose the cylinder depends on.

theorem ionescuTulceaContent_tendsto_zero {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (A : ℕ → Set ((n : ℕ) → X n)) (A_mem : ∀ (n : ℕ), A n ∈ MeasureTheory.measurableCylinders X) (A_anti : Antitone A) (A_inter : ⋂ (n : ℕ), A n = ∅) {p : ℕ} (x₀ : (i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) : Filter.Tendsto (fun (n : ℕ) => (ionescuTulceaContent κ x₀) (A n)) Filter.atTop (nhds 0)

This is the key theorem to prove the existence of the ionescuTulceaKernel: the ionescuTulceaContent of a decresaing sequence of cylinders with empty intersection converges to 0. This implies the σ-additivity of ionescuTulceaContent (see sigma_additive_addContent_of_tendsto_zero), which allows to extend it to the σ-algebra by Carathéodory's theorem.

theorem ionescuTulceaContent_sigma_subadditive {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] {p : ℕ} (x₀ : (i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) ⦃f : ℕ → Set ((n : ℕ) → X n)⦄ (hf : ∀ (n : ℕ), f n ∈ MeasureTheory.measurableCylinders X) (hf_Union : ⋃ (n : ℕ), f n ∈ MeasureTheory.measurableCylinders X) : (ionescuTulceaContent κ x₀) (⋃ (n : ℕ), f n) ≤ ∑' (n : ℕ), (ionescuTulceaContent κ x₀) (f n)

The ionescuTulceaContent is sigma-subadditive.

noncomputable def ionescuTulceaFun {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (p : ℕ) (x₀ : (i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) : MeasureTheory.Measure ((n : ℕ) → X n)

This function is the kernel given by the Ionescu-Tulcea theorem.

Equations

• ionescuTulceaFun κ p x₀ = MeasureTheory.Measure.ofAddContent ⋯ ⋯ (ionescuTulceaContent κ x₀) ⋯

theorem isProbabilityMeasure_ionescuTulceaFun {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (p : ℕ) (x₀ : (i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) : MeasureTheory.IsProbabilityMeasure (ionescuTulceaFun κ p x₀)

theorem isProjectiveLimit_ionescuTulceaFun {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (p : ℕ) (x₀ : (i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) : MeasureTheory.IsProjectiveLimit (ionescuTulceaFun κ p x₀) (inducedFamily fun (n : ℕ) => (ProbabilityTheory.Kernel.partialKernel κ p n) x₀)

theorem measurable_ionescuTulceaFun {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (p : ℕ) : Measurable (ionescuTulceaFun κ p)

noncomputable def ionescuTulceaKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (p : ℕ) : ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) ((n : ℕ) → X n)

Ionescu-Tulcea Theorem : Given a family of kernels κ k taking variables in Iic k with value in X (k+1), the kernel ionescuTulceaKernel κ p takes a variable x depending on the variables i ≤ p and associates to it a kernel on trajectories depending on all variables, where the entries with index ≤ p are those of x, and then one follows iteratively the kernels κ p, then κ (p+1), and so on.

The fact that such a kernel exists on infinite trajectories is not obvious, and is the content of the Ionescu-Tulcea theorem.

Equations

• ionescuTulceaKernel κ p = { toFun := ionescuTulceaFun κ p, measurable' := ⋯ }

theorem ionescuTulceaKernel_apply {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (p : ℕ) (x₀ : (i : { x : ℕ // x ∈ Finset.Iic p }) → X ↑i) : (ionescuTulceaKernel κ p) x₀ = ionescuTulceaFun κ p x₀

instance instIsMarkovKernelForallValNatMemFinsetIicForallIonescuTulceaKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (p : ℕ) : ProbabilityTheory.IsMarkovKernel (ionescuTulceaKernel κ p)

Equations

• ⋯ = ⋯

theorem ionescuTulceaKernel_proj {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (a : ℕ) (b : ℕ) : (ionescuTulceaKernel κ a).map (Preorder.frestrictLe b) = ProbabilityTheory.Kernel.partialKernel κ a b

theorem eq_ionescuTulceaKernel' {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] {a : ℕ} (n : ℕ) (η : ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) ((n : ℕ) → X n)) (hη : ∀ b ≥ n, η.map (Preorder.frestrictLe b) = ProbabilityTheory.Kernel.partialKernel κ a b) : η = ionescuTulceaKernel κ a

theorem eq_ionescuTulceaKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] {a : ℕ} (η : ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) ((n : ℕ) → X n)) (hη : ∀ (b : ℕ), η.map (Preorder.frestrictLe b) = ProbabilityTheory.Kernel.partialKernel κ a b) : η = ionescuTulceaKernel κ a

theorem partialKernel_comp_ionescuTulceaKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] {a : ℕ} {b : ℕ} (hab : a ≤ b) : (ionescuTulceaKernel κ b).comp (ProbabilityTheory.Kernel.partialKernel κ a b) = ionescuTulceaKernel κ a

theorem ionescuTulceaKernel_proj_le {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] {a : ℕ} {b : ℕ} (hab : a ≤ b) : (ionescuTulceaKernel κ b).map (Preorder.frestrictLe a) = ProbabilityTheory.Kernel.deterministic (Preorder.frestrictLe₂ hab) ⋯

def ℱ {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] : MeasureTheory.Filtration ℕ inferInstance

The canonical filtration on dependent functions indexed by ℕ, where 𝓕 n consists of measurable sets depending only on coordinates ≤ n.

Equations

• ℱ = { seq := fun (n : ℕ) => MeasurableSpace.comap (Preorder.frestrictLe n) inferInstance, mono' := ⋯, le' := ⋯ }

theorem stronglyMeasurable_dependsOn {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {E : Type u_2} [NormedAddCommGroup E] {n : ℕ} {f : ((n : ℕ) → X n) → E} (mf : MeasureTheory.StronglyMeasurable f) : DependsOn f (Set.Iic n)

If a function is strongly measurable with respect to the σ-algebra generated by the first coordinates, then it only depends on those first coordinates.

theorem ionescuTulceaKernel_eq {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] (n : ℕ) : ionescuTulceaKernel κ n = ((ProbabilityTheory.Kernel.deterministic id ⋯).prod ((ionescuTulceaKernel κ n).map (Set.Ioi n).restrict)).map ⇑(el' n)

This theorem shows that ionescuTulceaKernel κ n is, up to an equivalence, the product of a determinstic kernel with another kernel. This is an intermediate result to compute integrals with respect to this kernel.

theorem measurable_updateFinset' {ι : Type u_3} [DecidableEq ι] {I : Finset ι} {X : ι → Type u_4} [(i : ι) → MeasurableSpace (X i)] {y : (i : { x : ι // x ∈ I }) → X ↑i} : Measurable fun (x : (i : ι) → X i) => Function.updateFinset x I y

theorem ionescuTulceaKernel_eq_map_updateFinset {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] [Nonempty (X 0)] {n : ℕ} (x₀ : (i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) : (ionescuTulceaKernel κ n) x₀ = MeasureTheory.Measure.map (fun (y : (i : ℕ) → X i) => Function.updateFinset y (Finset.Iic n) x₀) ((ionescuTulceaKernel κ n) x₀)

theorem integrable_ionescuTulceaKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] {E : Type u_2} [NormedAddCommGroup E] [Nonempty (X 0)] {a : ℕ} {b : ℕ} (hab : a ≤ b) {f : ((n : ℕ) → X n) → E} (x₀ : (i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) (i_f : MeasureTheory.Integrable f ((ionescuTulceaKernel κ a) x₀)) : ∀ᵐ (x : (i : ℕ) → X i) ∂(ionescuTulceaKernel κ a) x₀, MeasureTheory.Integrable f ((ionescuTulceaKernel κ b) (Preorder.frestrictLe b x))

theorem integral_ionescuTulceaKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] {E : Type u_2} [NormedAddCommGroup E] [Nonempty (X 0)] [NormedSpace ℝ E] {n : ℕ} (x₀ : (i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) {f : ((n : ℕ) → X n) → E} (mf : MeasureTheory.AEStronglyMeasurable f ((ionescuTulceaKernel κ n) x₀)) : ∫ (x : (n : ℕ) → X n), f x ∂(ionescuTulceaKernel κ n) x₀ = ∫ (x : (n : ℕ) → X n), f (Function.updateFinset x (Finset.Iic n) x₀) ∂(ionescuTulceaKernel κ n) x₀

theorem partialKernel_comp_ionescuTulceaKernel_apply {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] {E : Type u_2} [NormedAddCommGroup E] [Nonempty (X 0)] [NormedSpace ℝ E] {a : ℕ} {b : ℕ} (hab : a ≤ b) (f : ((i : { x : ℕ // x ∈ Finset.Iic b }) → X ↑i) → ((n : ℕ) → X n) → E) (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) (x₀ : (i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) (i_f : MeasureTheory.Integrable (fun (x : (i : ℕ) → X i) => f (Preorder.frestrictLe b x) x) ((ionescuTulceaKernel κ a) x₀)) : ∫ (x : (i : { x : ℕ // x ∈ Finset.Iic b }) → X ↑i), ∫ (y : (n : ℕ) → X n), f x y ∂(ionescuTulceaKernel κ b) x ∂(ProbabilityTheory.Kernel.partialKernel κ a b) x₀ = ∫ (x : (n : ℕ) → X n), f (Preorder.frestrictLe b x) x ∂(ionescuTulceaKernel κ a) x₀

theorem condexp_ionescuTulceaKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] {E : Type u_2} [NormedAddCommGroup E] [Nonempty (X 0)] [NormedSpace ℝ E] [CompleteSpace E] {a : ℕ} {b : ℕ} (hab : a ≤ b) (x₀ : (i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) {f : ((n : ℕ) → X n) → E} (i_f : MeasureTheory.Integrable f ((ionescuTulceaKernel κ a) x₀)) (mf : MeasureTheory.StronglyMeasurable f) : MeasureTheory.condexp (↑ℱ b) ((ionescuTulceaKernel κ a) x₀) f =ᵐ[(ionescuTulceaKernel κ a) x₀] fun (x : (n : ℕ) → X n) => ∫ (y : (n : ℕ) → X n), f y ∂(ionescuTulceaKernel κ b) (Preorder.frestrictLe b x)

theorem condexp_ionescuTulceaKernel' {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic k }) → X ↑i) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] {E : Type u_2} [NormedAddCommGroup E] [Nonempty (X 0)] [NormedSpace ℝ E] [CompleteSpace E] {a : ℕ} {b : ℕ} {c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) (x₀ : (i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) {f : ((n : ℕ) → X n) → E} : MeasureTheory.condexp (↑ℱ b) ((ionescuTulceaKernel κ a) x₀) f =ᵐ[(ionescuTulceaKernel κ a) x₀] fun (x : (n : ℕ) → X n) => ∫ (y : (i : { x : ℕ // x ∈ Finset.Iic c }) → X ↑i), MeasureTheory.condexp (↑ℱ c) ((ionescuTulceaKernel κ a) x₀) f (Function.updateFinset x (Finset.Iic c) y) ∂(ProbabilityTheory.Kernel.partialKernel κ b c) (Preorder.frestrictLe b x)