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
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_cf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X))
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
mcf :
  StronglyMeasurable
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
x : (n : ℕ) → X n
h1 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f x
h2 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    @integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (y : (n : ℕ) → X n) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f y
⊢ AEMeasurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic c)) → X (↑i : ℕ)) (_m := MeasurableSpace.pi (X := X))
    (frestrictLe (π := X) c)
    ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b 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
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_cf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X))
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
mcf :
  StronglyMeasurable
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
x : (n : ℕ) → X n
h1 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f x
h2 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    @integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (y : (n : ℕ) → X n) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f y
⊢ Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic c)) → X (↑i : ℕ)) (frestrictLe (π := X) c)

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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
⊢ AEMeasurable (β := (i : ↥(Iic 0)) → X (↑i : ℕ))
    (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
          X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
      (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
    μ₀

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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
⊢ IsProbabilityMeasure (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
    (Measure.map
      (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
            X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
        (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
      μ₀)

Tactic:
have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piUnique ((fun i : Iic 0 ↦ X i))).symm) :=
    Measure.isProbabilityMeasure_map <| by 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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
this :
  IsProbabilityMeasure (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
    (Measure.map
      (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
            X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
        (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
      μ₀)
⊢ IsProbabilityMeasure (α := (n : ℕ) → X n) (m0 := MeasurableSpace.pi (X := X))
    (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.map
        (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
              X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
          (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
        μ₀)
      (⇑(traj (X := X) κ 0) : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)))

Tactic:
infer_instance
-- 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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
⊢ Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic a)) → X (↑i : ℕ)) (frestrictLe (π := X) a)

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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
⊢ Measurable (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)) fun (x : (i : ℕ) → X i) ↦
    (frestrictLe (π := X) a x, x (a + 1))

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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
rw :
  Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.map
        (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
              X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
          (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
        μ₀)
      (⇑(Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
    (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.map
        (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
              X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
          (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
        μ₀)
      (⇑(map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
⊢ Measure.map (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ) ⊗ₘ κ a =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) (trajMeasure (X := X) μ₀ κ)

Tactic:
rw [Measure.compProd_eq_comp_prod, trajMeasure, Measure.map_comp _ _ (by fun_prop),
    traj_map_frestrictLe, Measure.comp_assoc, Measure.map_comp _ _ (by fun_prop)]

Premises used: MeasureTheory.Measure.map_comp, ProbabilityTheory.Kernel.trajMeasure, MeasureTheory.Measure.compProd_eq_comp_prod, MeasureTheory.Measure.comp_assoc, ProbabilityTheory.Kernel.traj_map_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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
e_f :
  ∀ (x₀ : (i : ↥(Iic 0)) → X (↑i : ℕ)),
    Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      ((Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a :
            (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
          x₀ :
        Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
            (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
          x₀ :
        Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
⊢ Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.map
        (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
              X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
          (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
        μ₀)
      (⇑(Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
    (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.map
        (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
              X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
          (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
        μ₀)
      (⇑(map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))

Tactic:
congr with x₀ : 1
-- 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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
x₀ : (i : ↥(Iic 0)) → X (↑i : ℕ)
⊢ Measurable (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)) fun (x : (i : ℕ) → X i) ↦
    (frestrictLe (π := X) a x, x (a + 1))

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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
x₀ : (i : ↥(Iic 0)) → X (↑i : ℕ)
e_f :
  Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    (Measure.bind (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀)
      (⇑(Kernel.id ×ₖ κ a) : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1))))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      x₀)
e_f₁ :
  (partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀ ⊗ₘ κ a =
    (map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
        (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
      x₀
e_f₂ :
  (partialTraj (X := X) κ 0 a : (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x₀ ⊗ₘ κ a =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)))
      ((traj (X := X) κ 0 : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ℕ) → X i)) x₀)
e_f₃ e_f₄ :
  Eq.{u_1 + 1} (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)))
      ((traj (X := X) κ 0 : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)))
      ((traj (X := X) κ 0 : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((i : ℕ) → X i)) x₀))
⊢ Eq (α := Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((Kernel.id ×ₖ κ a ∘ₖ partialTraj (X := X) κ 0 a :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
    ((map (traj (X := X) κ 0) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1)) :
          (a_1 : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))
        x₀ :
      Measure (((i : ↥(Iic a)) → X (↑i : ℕ)) × X (a + 1)))

Tactic:
rw [comp_apply, ← Measure.compProd_eq_comp_prod, map_apply _ (by fun_prop),
    partialTraj_compProd_eq_map_traj zero_le']

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.comp_apply, MeasureTheory.Measure.compProd_eq_comp_prod, zero_le', ProbabilityTheory.Kernel.partialTraj_compProd_eq_map_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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
inst_3 : StandardBorelSpace.{u_1} (X (a + 1))
inst_4 : Nonempty.{u_1 + 1} (X (a + 1))
⊢ Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic a)) → X (↑i : ℕ)) (frestrictLe (π := X) a)

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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
inst_3 : StandardBorelSpace.{u_1} (X (a + 1))
inst_4 : Nonempty.{u_1 + 1} (X (a + 1))
⊢ Measurable (β := X (a + 1)) fun (x : (i : ℕ) → X i) ↦ x (a + 1)

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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
inst_3 : StandardBorelSpace.{u_1} (X (a + 1))
inst_4 : Nonempty.{u_1 + 1} (X (a + 1))
apply :
  Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) (trajMeasure (X := X) μ₀ κ) =
    Measure.map (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ) ⊗ₘ κ a
⊢ (ae (F := Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
        (Measure.map (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ))).EventuallyEq
    (β := Measure (X (a + 1)))
    (⇑(condDistrib (fun (x : (i : ℕ) → X i) ↦ x (a + 1)) (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ)) :
      (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1)))
    (⇑(κ a) : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1)))

Tactic:
apply condDistrib_ae_eq_of_measure_eq_compProd_of_measurable (by fun_prop) (by fun_prop)

Premises used: ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable
-- 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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
inst_3 : StandardBorelSpace.{u_1} (X (a + 1))
inst_4 : Nonempty.{u_1 + 1} (X (a + 1))
⊢ Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) (trajMeasure (X := X) μ₀ κ) =
    Measure.map (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ) ⊗ₘ κ a

Tactic:
map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure.symm

Premises used: ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, Eq.symm
-- 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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
a : ℕ
inst_3 : StandardBorelSpace.{u_1} (X (a + 1))
inst_4 : Nonempty.{u_1 + 1} (X (a + 1))
⊢ Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) a x, x (a + 1))) (trajMeasure (X := X) μ₀ κ) =
    Measure.map (frestrictLe (π := X) a) (trajMeasure (X := X) μ₀ κ) ⊗ₘ κ a

Tactic:
exact map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure.symm

Premises used: ProbabilityTheory.Kernel.map_frestrictLe_trajMeasure_compProd_eq_map_trajMeasure, Eq.symm
-- Module: Mathlib.Probability.Kernel.Irreducible
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
φ : Measure α
inst : Subsingleton α
s : Set α
hs : MeasurableSet s
hsp : GT.gt (α := ℝ≥0∞) ((φ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
a : α
h :
  GT.gt (α := ℝ≥0∞)
    ((((HPow.hPow (α := Kernel α α) (β := ℕ) Kernel.id 1 : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ ∃ (n : ℕ),
    GT.gt (α := ℝ≥0∞)
      ((((HPow.hPow (α := Kernel α α) Kernel.id n : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
use 1
-- Module: Mathlib.Probability.Kernel.Irreducible
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
φ : Measure α
inst : Subsingleton α
s : Set α
hs : MeasurableSet s
hsp : GT.gt (α := ℝ≥0∞) ((φ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
a : α
⊢ a ∈ s

Tactic:
have ha : a ∈ s :=
      Subsingleton.mem_iff_nonempty.mpr
        <| MeasureTheory.nonempty_of_measure_ne_zero (μ := φ) (ne_of_lt hsp).symm
-- Module: Mathlib.Probability.Kernel.Irreducible
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
φ : Measure α
inst : Subsingleton α
s : Set α
hs : MeasurableSet s
hsp : GT.gt (α := ℝ≥0∞) ((φ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
a : α
ha : a ∈ s
⊢ GT.gt (α := ℝ≥0∞)
    ((((HPow.hPow (α := Kernel α α) (β := ℕ) Kernel.id 1 : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp [id_apply, ha]

Premises used: ProbabilityTheory.Kernel.id_apply
-- Module: Mathlib.Probability.Kernel.Irreducible
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
c : ℝ≥0∞
φ : Measure α
κ : Kernel α α
hκ : IsIrreducible φ κ
s : Set α
hs : MeasurableSet s
hsp : GT.gt (α := ℝ≥0∞) ((c • φ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ GT.gt (α := ℝ≥0∞) ((φ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_all
-- Module: Mathlib.Probability.Kernel.Irreducible
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
c : ℝ≥0∞
φ : Measure α
κ : Kernel α α
hκ : IsIrreducible φ κ
s : Set α
hs : MeasurableSet s
hsp : GT.gt (α := ℝ≥0∞) ((c • φ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (a : α),
    ∃ (n : ℕ),
      GT.gt (α := ℝ≥0∞) ((((κ ^ n : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa using hκ.irreducible hs <| by simp_all

Premises used: ProbabilityTheory.Kernel.IsIrreducible.irreducible
-- Module: Mathlib.Probability.Kernel.Irreducible
Goal:
α : Type u_1
mα : MeasurableSpace α
φ₁ φ₂ : Measure α
hφ : φ₁ ≤ φ₂
κ : Kernel α α
hκ : IsIrreducible φ₂ κ
s : Set α
hs : MeasurableSet s
hsp : GT.gt (α := ℝ≥0∞) ((φ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (a : α),
    ∃ (n : ℕ),
      GT.gt (α := ℝ≥0∞) ((((κ ^ n : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa using hκ.irreducible hs <| Std.lt_of_lt_of_le hsp (hφ s)

Premises used: ProbabilityTheory.Kernel.IsIrreducible.irreducible, Std.lt_of_lt_of_le
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
f : β → E
hf : StronglyMeasurable f
simp_rw : MeasurableSet.{u_1} (α := α) {a : α | @HasFiniteIntegral _ _ _ mβ f ((κ : (a : α) → Measure β) a)}
⊢ MeasurableSet.{u_1} (α := α) {a : α | @Integrable _ _ _ _ mβ f ((κ : (a : α) → Measure β) a)}

Tactic:
simp_rw [Integrable, hf.aestronglyMeasurable, true_and]

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.Integrable, true_and
-- Module: Mathlib.Probability.Kernel.MeasurableIntegral
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst : NormedAddCommGroup E
f : β → E
hf : StronglyMeasurable f
⊢ MeasurableSet.{u_1} (α := α) {a : α | @HasFiniteIntegral _ _ _ mβ f ((κ : (a : α) → Measure β) a)}

Tactic:
measurableSet_lt hf.enorm.lintegral_kernel measurable_const

Premises used: MeasureTheory.StronglyMeasurable.enorm, setOf, Measurable.lintegral_kernel, measurableSet_lt, measurable_const, MeasureTheory.HasFiniteIntegral