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)
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₀)
h :
  Eq.{u_1 + 1} (α := Measure ((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₀))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
⊢ ∀ᵐ (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)

Tactic:
convert! i_f.1

Premises used: And.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)
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₀)
h :
  Eq.{u_1 + 1} (α := Measure ((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₀))
    (((traj (X := X) κ a).map (frestrictLe (π := X) b) :
        (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
      x₀)
h₁ h₂ :
  Eq.{u_1 + 1} (α := Measure ((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₀))
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ℕ) → X i)) x₀))
⊢ Eq.{u_1 + 1} (α := Measure ((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₀))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)

Tactic:
rw [← traj_map_frestrictLe, Kernel.map_apply _ (measurable_frestrictLe _)]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.traj_map_frestrictLe, Preorder.measurable_frestrictLe
-- 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) κ 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₀)

Tactic:
i_f.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable
-- 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) κ 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₀)

Tactic:
exact i_f.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable
-- 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 : ℕ)
hf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (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₀)

Tactic:
rw [← traj_comp_partialTraj hab] at hf

Premises used: ProbabilityTheory.Kernel.traj_comp_partialTraj
-- 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 : ℕ)
hf :
  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 : ↥(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 : ℕ))),
    AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)

Tactic:
hf.comp

Premises used: MeasureTheory.AEStronglyMeasurable.comp
-- 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 : ℕ)
hf :
  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 : ↥(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 : ℕ))),
    AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)

Tactic:
exact hf.comp

Premises used: MeasureTheory.AEStronglyMeasurable.comp
-- 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
inst_3 : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
hφ :
  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₀)
hfm :
  AEStronglyMeasurable (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₀))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      f x)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      f (updateFinset (π := X) x (Iic a) x₀))

Tactic:
nth_rw 1 [← traj_map_updateFinset, integral_map]

Premises used: ProbabilityTheory.Kernel.traj_map_updateFinset, MeasureTheory.integral_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
inst_3 : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (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)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (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)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ AEStronglyMeasurable (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)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (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)) AEStronglyMeasurable._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₀)
⊢ AEStronglyMeasurable (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)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
h h₁ :
  Eq (α := autoParam (Measure ((n : ℕ) → X n)) AEStronglyMeasurable._auto_1)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))
⊢ Eq.{u_1 + 1} (α := autoParam (Measure ((n : ℕ) → X n)) AEStronglyMeasurable._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:
rw [traj_map_updateFinset]

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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
h :
  ∀ (s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) (ms : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
              traj (X := X) κ b :
            (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      (((Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
                ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u) :
              Measure (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))) :
            (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u)

Tactic:
ext s ms
-- 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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
h :
  ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) a : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        (Prod.mk a ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        u =
    ∫⁻ (b_1 : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) b_1 :
            Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u
h₁ : MeasurableSet (α := (n : ℕ) → X n) ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)
h₂ : MeasurableSet s
h₃ :
  Measurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) fun (x : (i : ℕ) → X i) ↦
    (frestrictLe (π := X) b x, x)
h₄ : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
            traj (X := X) κ b :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
              ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u) :
            Measure (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))) :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Measure.map_apply, Measure.compProd_apply, ← traj_comp_partialTraj hab, comp_apply']

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.compProd_apply, ProbabilityTheory.Kernel.traj_comp_partialTraj, ProbabilityTheory.Kernel.comp_apply'
-- 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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
h :
  ∀ (x : (i : ↥(Iic b)) → X (↑i : ℕ)),
    Eq (α := ℝ≥0∞)
      ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x :
              Measure ((n : ℕ) → X n)) :
            (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
          (Prod.mk x ⁻¹' s) :
        ℝ≥0∞)
      ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x :
              Measure ((n : ℕ) → X n)) :
            (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
          ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s) :
        ℝ≥0∞)
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) a : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        (Prod.mk a ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        u =
    ∫⁻ (b_1 : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) b_1 :
            Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u

Tactic:
congr 1 with x
-- 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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X (↑i : ℕ)
h :
  Eq (α := ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
        ((fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) :
      ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x)
          ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)) :
      ℝ≥0∞)
h₁ : Measurable (β := (i : ℕ) → X i) fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x
h₂ : MeasurableSet (α := (i : ℕ) → X i) ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)
h₃ : Measurable (β := (i : ℕ) → X i) fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x
h₄ : MeasurableSet (Prod.mk x ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) :
      ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s) :
      ℝ≥0∞)

Tactic:
rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_apply]

Premises used: ProbabilityTheory.Kernel.traj_map_updateFinset, MeasureTheory.Measure.map_apply
-- 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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X (↑i : ℕ)
h :
  ∀ (y : (i : ℕ) → X i),
    Membership.mem (γ := Set ((i : ℕ) → X i))
        ((fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) y ↔
      Membership.mem (γ := Set ((i : ℕ) → X i))
        (Set.preimage (β := (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x)
          ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s))
        y
⊢ Eq (α := ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
        ((fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) :
      ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x)
          ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)) :
      ℝ≥0∞)

Tactic:
congr 1 with y