awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : i ≤ a + 1
h2 : ¬i ≤ a
h : ¬i = a + 1
⊢ @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ = x₀ i

Tactic:
lia
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : ¬i ≤ a + 1
h : i = a + 1
⊢ x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯

Tactic:
lia
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable (β := ℝ≥0∞) fun (b : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ↦
    f (updateFinset (π := X) x₀ (Iic (a + 1)) (_root_.IicProdIoc (X := X) a (a + 1) (frestrictLe (π := X) a x₀, b)))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable (β := ℝ≥0∞) fun (a_1 : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) ↦
    f (updateFinset (π := X) x₀ (Iic (a + 1)) (_root_.IicProdIoc (X := X) a (a + 1) a_1))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (a + 1))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic (a + 1)) z)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
g : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n) → ℝ≥0∞ :=
  fun (c : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)) ↦ f (updateFinset (π := X) c.2 (Iic b) c.1)
η : Kernel ((n : ℕ) → X n) ((i : ↥(Iic b)) → X (↑i : ℕ)) :=
  (partialTraj (X := X) κ a b).comap (frestrictLe (π := X) a) ⋯
change :
  Measurable (β := ℝ≥0∞) fun (x₀ : (n : ℕ) → X n) ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      g (z, x₀) ∂(η : (a : (n : ℕ) → X n) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (n : ℕ) → X n) ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic b)
          z) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)

Tactic:
change Measurable fun x₀ ↦ ∫⁻ z : (i : Iic b) → X i, g (z, x₀) ∂η x₀

Premises used: Measurable, Prod.mk, DFunLike.coe, MeasureTheory.lintegral
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
g : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n) → ℝ≥0∞ :=
  fun (c : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)) ↦ f (updateFinset (π := X) c.2 (Iic b) c.1)
η : Kernel ((n : ℕ) → X n) ((i : ↥(Iic b)) → X (↑i : ℕ)) :=
  (partialTraj (X := X) κ a b).comap (frestrictLe (π := X) a) ⋯
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (n : ℕ) → X n) ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      g (z, x₀) ∂(η : (a : (n : ℕ) → X n) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
hbc : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
h :
  ∀ (x₀ : (n : ℕ) → X n),
    lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
      lmarginalPartialTraj (X := X) κ a c f x₀
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) = lmarginalPartialTraj (X := X) κ a c f

Tactic:
ext x₀
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
hbc : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
h :
  ∀ (hab : a ≤ a) (hbc : a ≤ c),
    lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
      lmarginalPartialTraj (X := X) κ a c f x₀
h₁ :
  ∀ (hab : a < b),
    lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
      lmarginalPartialTraj (X := X) κ a c f x₀
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀

Tactic:
obtain rfl | hab := eq_or_lt_of_le hab

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a ≤ a
hbc : a ≤ c
h :
  ∀ (hbc : a ≤ a),
    lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a a f) x₀ =
      lmarginalPartialTraj (X := X) κ a a f x₀
h₁ :
  ∀ (hbc : a < c),
    lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
      lmarginalPartialTraj (X := X) κ a c f x₀
⊢ lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀

Tactic:
obtain rfl | hbc := eq_or_lt_of_le hbc

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
hbc : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
h :
  ∀ (hbc : b ≤ b),
    lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b b f) x₀ =
      lmarginalPartialTraj (X := X) κ a b f x₀
h₁ :
  ∀ (hbc : b < c),
    lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
      lmarginalPartialTraj (X := X) κ a c f x₀
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀

Tactic:
obtain rfl | hbc := eq_or_lt_of_le hbc

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab hbc : a ≤ a
h h₁ : lmarginalPartialTraj (X := X) κ a a f x₀ = lmarginalPartialTraj (X := X) κ a a f x₀
⊢ lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a a f) x₀ =
    lmarginalPartialTraj (X := X) κ a a f x₀

Tactic:
rw [lmarginalPartialTraj_le κ le_rfl (measurable_lmarginalPartialTraj _ _ hf)]

Premises used: le_rfl, ProbabilityTheory.Kernel.lmarginalPartialTraj_le, ProbabilityTheory.Kernel.measurable_lmarginalPartialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a ≤ a
hbc_1 : a ≤ c
hbc : a < c
h h₁ : lmarginalPartialTraj (X := X) κ a c f x₀ = lmarginalPartialTraj (X := X) κ a c f x₀
⊢ lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀

Tactic:
rw [lmarginalPartialTraj_le κ le_rfl (measurable_lmarginalPartialTraj _ _ hf)]

Premises used: le_rfl, ProbabilityTheory.Kernel.lmarginalPartialTraj_le, ProbabilityTheory.Kernel.measurable_lmarginalPartialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b ≤ b
h h₁ : lmarginalPartialTraj (X := X) κ a b f x₀ = lmarginalPartialTraj (X := X) κ a b f x₀
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b b f) x₀ =
    lmarginalPartialTraj (X := X) κ a b f x₀

Tactic:
rw [lmarginalPartialTraj_le κ le_rfl hf]

Premises used: le_rfl, ProbabilityTheory.Kernel.lmarginalPartialTraj_le
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
hbc_1 : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
h :
  ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      ∫⁻ (z : (i : ↥(Iic c)) → X (↑i : ℕ)),
        f
          (updateFinset (π := X) x₀ (Iic c)
            z) ∂(partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
          z ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        ((Iic a).restrict (π := X) x₀) =
    ∫⁻ (z : (i : ↥(Iic c)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic c)
          z) ∂(partialTraj (X := X) κ a c : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
        ((Iic a).restrict (π := X) x₀)
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀

Tactic:
simp_rw [lmarginalPartialTraj, frestrictLe, restrict_updateFinset,
    updateFinset_updateFinset_of_subset (Iic_subset_Iic.2 hbc.le)]

Premises used: Iff.mpr, Function.restrict_updateFinset, LT.lt.le, Finset.Iic_subset_Iic, ProbabilityTheory.Kernel.lmarginalPartialTraj, Preorder.frestrictLe, Function.updateFinset_updateFinset_of_subset
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
hbc_1 : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
h : Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic c) z)
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      ∫⁻ (z : (i : ↥(Iic c)) → X (↑i : ℕ)),
        f
          (updateFinset (π := X) x₀ (Iic c)
            z) ∂(partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
          z ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        ((Iic a).restrict (π := X) x₀) =
    ∫⁻ (z : (i : ↥(Iic c)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic c)
          z) ∂(partialTraj (X := X) κ a c : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
        ((Iic a).restrict (π := X) x₀)

Tactic:
rw [← lintegral_comp, partialTraj_comp_partialTraj hab.le hbc.le]

Premises used: LT.lt.le, ProbabilityTheory.Kernel.partialTraj_comp_partialTraj, ProbabilityTheory.Kernel.lintegral_comp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
hbc_1 : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
⊢ Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic c) z)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
h : ∀ (x : (n : ℕ) → X n), lmarginalPartialTraj (X := X) κ b c f x = f x
⊢ lmarginalPartialTraj (X := X) κ b c f = f

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
h :
  ∫⁻ (x_1 : (i : ↥(Ioc b c)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) x (Ioc b c)
          x_1) ∂((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
          (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x) =
    f x
⊢ lmarginalPartialTraj (X := X) κ b c f x = f x

Tactic:
rw [lmarginalPartialTraj_eq_lintegral_map mf]

Premises used: ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ ∫⁻ (x_1 : (i : ↥(Ioc b c)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) x (Ioc b c)
          x_1) ∂((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
          (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x) =
    f x

Tactic:
@lintegral_eq_const _ _ _ ?_ _ _ (ae_of_all _ fun y ↦ hf fun i hi ↦ ?_)

Premises used: MeasureTheory.lintegral_eq_const, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
h :
  IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
    (((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
        (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
      (frestrictLe (π := X) b x))
h₁ :
  ∀ (y : (i : ↥(Ioc b c)) → X (↑i : ℕ)) (i : ℕ) (hi : i ∈ (↑(Iic a) : Set ℕ)),
    Function.updateFinset (π := X) x (Ioc b c) y i = x i
⊢ ∫⁻ (x_1 : (i : ↥(Ioc b c)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) x (Ioc b c)
          x_1) ∂((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
          (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x) =
    f x

Tactic:
refine @lintegral_eq_const _ _ _ ?_ _ _ (ae_of_all _ fun y ↦ hf fun i hi ↦ ?_)

Premises used: MeasureTheory.lintegral_eq_const, MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
    (((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
        (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
      (frestrictLe (π := X) b x))

Tactic:
@IsMarkovKernel.isProbabilityMeasure _ _ _ _ _ ?_ _

Premises used: ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
h :
  IsMarkovKernel (β := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (mβ :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
    ((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯))
⊢ IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
    (((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
        (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
      (frestrictLe (π := X) b x))

Tactic:
refine @IsMarkovKernel.isProbabilityMeasure _ _ _ _ _ ?_ _

Premises used: ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic c)) → X (↑i : ℕ)) (β := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ IsMarkovKernel (β := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (mβ :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
    ((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯))

Tactic:
exact IsMarkovKernel.map _ (by fun_prop)

Premises used: ProbabilityTheory.Kernel.IsMarkovKernel.map
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
y : (i : ↥(Ioc b c)) → X (↑i : ℕ)
i : ℕ
hi : i ∈ (↑(Iic a) : Set ℕ)
h :
  ∀ (hf : DependsOn (α := X) f (Set.Iic a)) (hab : a ≤ b) (hi : i ≤ a) (h : b < i ∧ i ≤ c),
    y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) i ⋯) = x i
⊢ Function.updateFinset (π := X) x (Ioc b c) y i = x i

Tactic:
simp_all only [coe_Iic, Set.mem_Iic, Function.updateFinset, mem_Ioc, dite_eq_right_iff]

Premises used: Finset.coe_Iic, Function.updateFinset, dite_eq_right_iff, Set.mem_Iic, Finset.mem_Ioc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x : (n : ℕ) → X n
y : (i : ↥(Ioc b c)) → X (↑i : ℕ)
i : ℕ
hf : DependsOn (α := X) f (Set.Iic a)
hab : a ≤ b
hi : i ≤ a
⊢ ∀ (h : b < i ∧ i ≤ c), y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) i ⋯) = x i

Tactic:
lia
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
d : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hac : a ≤ c
had : a ≤ d
inr :
  ∀
    (this :
      ∀ {c d : ℕ} (hac : a ≤ c) (had : a ≤ d) (hcd : c ≤ d),
        lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f)
    (hcd : ¬c ≤ d), lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
wlog :
  ∀ {c d : ℕ} (hac : a ≤ c) (had : a ≤ d) (hcd : c ≤ d),
    lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f

Tactic:
wlog hcd : c ≤ d generalizing c d
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
d : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hac : a ≤ c
had : a ≤ d
this :
  ∀ {c d : ℕ} (hac : a ≤ c) (had : a ≤ d) (hcd : c ≤ d),
    lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
hcd : ¬c ≤ d
inr inr₁ : lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b c f
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f

Tactic:
rw [this had hac (le_of_not_ge hcd)]

Premises used: le_of_not_ge
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
inl : ∀ (hbc : b ≤ c), lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
inr : ∀ (hcb : c ≤ b), lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f

Tactic:
obtain hbc | hcb := le_total b c

Premises used: le_total
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hbc : b ≤ c
inl :
  lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b c (lmarginalPartialTraj (X := X) κ c d f)
inl₁ inl₂ : lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b c f
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f

Tactic:
rw [← lmarginalPartialTraj_self hbc hcd mf, hf.lmarginalPartialTraj_of_le d mf hac]

Premises used: DependsOn.lmarginalPartialTraj_of_le, ProbabilityTheory.Kernel.lmarginalPartialTraj_self