awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
h :
  ∀ (x_1 : (i : ℕ) → X i) (x_2 : ℕ),
    updateFinset (π := X) x_1 (Iic n) x x_2 =
      ((⇑(IicProdIoi (X := X) n) :
            (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
          Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
        x_1 x_2
⊢ Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))

Tactic:
ext
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
x_1 : (i : ℕ) → X i
x_2 : ℕ
⊢ updateFinset (π := X) x_1 (Iic n) x x_2 =
    ((⇑(IicProdIoi (X := X) n) :
          (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
        Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
      x_1 x_2

Tactic:
simp [IicProdIoi, updateFinset]

Premises used: Function.updateFinset, MeasurableEquiv.IicProdIoi
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
⊢ Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))

Tactic:
have : (updateFinset · _ x) = IicProdIoi n ∘ (Prod.mk x) ∘ (Set.Ioi n).restrict := by
    ext; simp [IicProdIoi, updateFinset]
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi n).restrict (π := X))
hf₁ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((a : (↑(Set.Ioi n) : Type)) → X (↑a : ℕ))) (β :=
    (n : ℕ) → X n)
    (⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
hg :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) (β :=
    (i : ℕ) → X i)
    (⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
hf₂ : Measurable (α := (i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ)) (Prod.mk x)
hg₁ :
  Measurable (α := (i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ)) (β := (i : ℕ) → X i)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x)
hf₃ : Measurable.{u_1, u_1} (α := (i : ℕ) → X i) ((Set.Ioi n).restrict (π := X))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ n).map ((Set.Ioi n).restrict (π := X)))
          (⇑(IicProdIoi (X := X) n) :
            (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) :
        (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
      x)

Tactic:
rw [this, ← Function.comp_assoc, ← Measure.map_map, ← Measure.map_map, map_apply, prod_apply,
    map_apply, id_apply, Measure.dirac_prod]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.prod_apply, MeasureTheory.Measure.dirac_prod, ProbabilityTheory.Kernel.id_apply, MeasureTheory.Measure.map_map, Function.comp_assoc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
⊢ Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi n).restrict (π := X))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((a : (↑(Set.Ioi n) : Type)) → X (↑a : ℕ))) (β :=
    (n : ℕ) → X n)
    (⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) (β :=
    (i : ℕ) → X i)
    (⇑(IicProdIoi (X := X) n) :
      (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
⊢ Measurable (α := (i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ)) (Prod.mk x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
⊢ Measurable (α := (i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ)) (β := (i : ℕ) → X i)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
this :
  Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
⊢ Measurable.{u_1, u_1} (α := (i : ℕ) → X i) ((Set.Ioi n).restrict (π := X))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
hf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
hg :
  AEMeasurable (β := (n : ℕ) → X n) (_m := MeasurableSpace.pi (X := X))
    (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ ∫⁻ (x : (n : ℕ) → X n), f x ∂(traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ =
    ∫⁻ (x : (n : ℕ) → X n),
      f
        (updateFinset (π := X) x (Iic a)
          x₀) ∂(traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀

Tactic:
nth_rw 1 [← traj_map_updateFinset, MeasureTheory.lintegral_map']

Premises used: ProbabilityTheory.Kernel.traj_map_updateFinset, MeasureTheory.lintegral_map'
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)

Tactic:
mf
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
h :
  Eq.{u_1 + 1} (α := autoParam (Measure ((n : ℕ) → X n)) AEMeasurable._auto_1)
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))

Tactic:
convert! mf
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ Eq.{u_1 + 1} (α := autoParam (Measure ((n : ℕ) → X n)) AEMeasurable._auto_1)
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)

Tactic:
traj_map_updateFinset x₀

Premises used: ProbabilityTheory.Kernel.traj_map_updateFinset
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ Eq.{u_1 + 1} (α := autoParam (Measure ((n : ℕ) → X n)) AEMeasurable._auto_1)
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)

Tactic:
exact traj_map_updateFinset x₀

Premises used: ProbabilityTheory.Kernel.traj_map_updateFinset
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ AEMeasurable (β := (n : ℕ) → X n) (_m := MeasurableSpace.pi (X := X))
    (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)

Tactic:
measurable_updateFinset_left.aemeasurable

Premises used: Measurable.aemeasurable, measurable_updateFinset_left
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf :
  AEMeasurable (_m := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ AEMeasurable (β := (n : ℕ) → X n) (_m := MeasurableSpace.pi (X := X))
    (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)

Tactic:
exact measurable_updateFinset_left.aemeasurable

Premises used: Measurable.aemeasurable, measurable_updateFinset_left
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
⊢ ∫⁻ (x : (n : ℕ) → X n), f x ∂(traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ =
    ∫⁻ (x : (n : ℕ) → X n),
      f
        (updateFinset (π := X) x (Iic a)
          x₀) ∂(traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀

Tactic:
lintegral_traj₀ x₀ mf.aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.Kernel.lintegral_traj₀
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
rw :
  ∀
    (i_f :
      (∀ᵐ (y :
          (i : ↥(Iic b)) →
            X
              (↑i :
                ℕ)) ∂((partialTraj (X := X) κ a b :
                (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
              x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
          @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
            ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
        @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
          (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
            @integral _ _ _ _ (MeasurableSpace.pi (X := X))
              ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
              fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
          ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
            x₀)),
    ∀ᵐ (x :
      (i : ℕ) →
        X
          i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
        Measure ((n : ℕ) → X n)),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
hf :
  ∀
    (i_f :
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
          x₀)),
    AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
        x₀)
⊢ ∀ᵐ (x :
    (i : ℕ) →
      X
        i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
      Measure ((n : ℕ) → X n)),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))

Tactic:
rw [← traj_comp_partialTraj hab, integrable_comp_iff] at i_f

Premises used: ProbabilityTheory.Kernel.traj_comp_partialTraj, ProbabilityTheory.integrable_comp_iff
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (i : ↥(Iic b)) →
        X
          (↑i :
            ℕ)) ∂((partialTraj (X := X) κ a b :
            (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
          x₀ :
        Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
hf :
  AEMeasurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (_m := MeasurableSpace.pi (X := X))
    (frestrictLe (π := X) b) ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
h :
  ∀ᵐ (y :
    (i : ↥(Iic b)) →
      X
        (↑i :
          ℕ)) ∂Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
apply : MeasurableSpace ((i : ↥(Iic b)) → X (↑i : ℕ))
⊢ ∀ᵐ (x :
    (i : ℕ) →
      X
        i) ∂((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
      Measure ((n : ℕ) → X n)),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))

Tactic:
apply ae_of_ae_map (p := fun x ↦ Integrable f (traj κ b x))

Premises used: MeasureTheory.ae_of_ae_map
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (i : ↥(Iic b)) →
        X
          (↑i :
            ℕ)) ∂((partialTraj (X := X) κ a b :
            (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
          x₀ :
        Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
⊢ AEMeasurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (_m := MeasurableSpace.pi (X := X))
    (frestrictLe (π := X) b) ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (i : ↥(Iic b)) →
        X
          (↑i :
            ℕ)) ∂((partialTraj (X := X) κ a b :
            (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
          x₀ :
        Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
⊢ ∀ᵐ (y :
    (i : ↥(Iic b)) →
      X
        (↑i :
          ℕ)) ∂((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)

Tactic:
i_f.1

Premises used: And.left