awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
⊢ updateFinset (π := X) x₀ (Iic b) (_root_.IicProdIoc (X := X) a b (frestrictLe (π := X) a x₀, x)) i =
    updateFinset (π := X) x₀ (Ioc a b) x i
have simp : Eq.{u_1 + 1} (α := X i)
  (if h : i ≤ b then if h : i ≤ a then x₀ i else x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i sorry) else x₀ i)
  (if h : a < i ∧ i ≤ b then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i sorry) else x₀ i)
Tactic: simp only [updateFinset, mem_Iic, IicProdIoc_def,
      frestrictLe_apply, mem_Ioc]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ b then if h : i ≤ a then x₀ i else x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
    (if h : a < i ∧ i ≤ b then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
have pos : i ≤ b → i ≤ a → ∀ (h : a < i ∧ i ≤ b), x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i sorry)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
pos : i ≤ b → i ≤ a → ∀ (h : a < i ∧ i ≤ b), x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯)
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ b then if h : i ≤ a then x₀ i else x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
    (if h : a < i ∧ i ≤ b then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
have neg : i ≤ b → i ≤ a → ¬(a < i ∧ i ≤ b) → x₀ i = x₀ i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
pos : i ≤ b → i ≤ a → ∀ (h : a < i ∧ i ≤ b), x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯)
neg : i ≤ b → i ≤ a → ¬(a < i ∧ i ≤ b) → x₀ i = x₀ i
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ b then if h : i ≤ a then x₀ i else x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
    (if h : a < i ∧ i ≤ b then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
have pos₁ : ∀ (h : i ≤ b) (h_1 : ¬i ≤ a) (h_2 : a < i ∧ i ≤ b),
  Eq (α := X i)
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i sorry) : X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i sorry) : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i sorry))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
pos : i ≤ b → i ≤ a → ∀ (h : a < i ∧ i ≤ b), x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯)
neg : i ≤ b → i ≤ a → ¬(a < i ∧ i ≤ b) → x₀ i = x₀ i
pos₁ :
  ∀ (h : i ≤ b) (h_1 : ¬i ≤ a) (h_2 : a < i ∧ i ≤ b),
    Eq (α := X i)
      (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) : X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) : ℕ))
      (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯))
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ b then if h : i ≤ a then x₀ i else x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
    (if h : a < i ∧ i ≤ b then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
have neg₁ : ∀ (h : i ≤ b) (h_1 : ¬i ≤ a), ¬(a < i ∧ i ≤ b) → x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i sorry) = x₀ i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
pos : i ≤ b → i ≤ a → ∀ (h : a < i ∧ i ≤ b), x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯)
neg : i ≤ b → i ≤ a → ¬(a < i ∧ i ≤ b) → x₀ i = x₀ i
pos₁ :
  ∀ (h : i ≤ b) (h_1 : ¬i ≤ a) (h_2 : a < i ∧ i ≤ b),
    Eq (α := X i)
      (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) : X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) : ℕ))
      (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯))
neg₁ : ∀ (h : i ≤ b) (h_1 : ¬i ≤ a), ¬(a < i ∧ i ≤ b) → x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) = x₀ i
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ b then if h : i ≤ a then x₀ i else x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
    (if h : a < i ∧ i ≤ b then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
have pos₂ : ¬i ≤ b → ∀ (h : a < i ∧ i ≤ b), x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i sorry)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
pos : i ≤ b → i ≤ a → ∀ (h : a < i ∧ i ≤ b), x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯)
neg : i ≤ b → i ≤ a → ¬(a < i ∧ i ≤ b) → x₀ i = x₀ i
pos₁ :
  ∀ (h : i ≤ b) (h_1 : ¬i ≤ a) (h_2 : a < i ∧ i ≤ b),
    Eq (α := X i)
      (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) : X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) : ℕ))
      (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯))
neg₁ : ∀ (h : i ≤ b) (h_1 : ¬i ≤ a), ¬(a < i ∧ i ≤ b) → x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) = x₀ i
pos₂ : ¬i ≤ b → ∀ (h : a < i ∧ i ≤ b), x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯)
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ b then if h : i ≤ a then x₀ i else x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
    (if h : a < i ∧ i ≤ b then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ i)
have neg₂ : ¬i ≤ b → ¬(a < i ∧ i ≤ b) → x₀ i = x₀ i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
⊢ lmarginalPartialTraj (X := X) κ a (a + 1) f x₀ =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
have rw : ∫⁻ (a_1 : X (a + 1)),
    f
      (updateFinset (π := X) x₀ (Iic (a + 1))
        (_root_.IicProdIoc (X := X) a (a + 1)
          (frestrictLe (π := X) a x₀,
            (piSingleton (X := X) a : (a_2 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
              a_1))) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀) =
  ∫⁻ (x : X (a + 1)),
    f
      (update (β := X) x₀ (a + 1)
        x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
Tactic: rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
rw :
  ∫⁻ (a_1 : X (a + 1)),
      f
        (updateFinset (π := X) x₀ (Iic (a + 1))
          (_root_.IicProdIoc (X := X) a (a + 1)
            (frestrictLe (π := X) a x₀,
              (piSingleton (X := X) a : (a_2 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
                a_1))) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
⊢ lmarginalPartialTraj (X := X) κ a (a + 1) f x₀ =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
have hf : 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: rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
rw :
  ∫⁻ (a_1 : X (a + 1)),
      f
        (updateFinset (π := X) x₀ (Iic (a + 1))
          (_root_.IicProdIoc (X := X) a (a + 1)
            (frestrictLe (π := X) a x₀,
              (piSingleton (X := X) a : (a_2 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
                a_1))) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
hf :
  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 : ℕ))
⊢ lmarginalPartialTraj (X := X) κ a (a + 1) f x₀ =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
have hg : 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: rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
rw :
  ∫⁻ (a_1 : X (a + 1)),
      f
        (updateFinset (π := X) x₀ (Iic (a + 1))
          (_root_.IicProdIoc (X := X) a (a + 1)
            (frestrictLe (π := X) a x₀,
              (piSingleton (X := X) a : (a_2 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
                a_1))) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
hf :
  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 : ℕ))
hg :
  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)))
⊢ lmarginalPartialTraj (X := X) κ a (a + 1) f x₀ =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
have hf₁ : 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: rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
rw :
  ∫⁻ (a_1 : X (a + 1)),
      f
        (updateFinset (π := X) x₀ (Iic (a + 1))
          (_root_.IicProdIoc (X := X) a (a + 1)
            (frestrictLe (π := X) a x₀,
              (piSingleton (X := X) a : (a_2 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
                a_1))) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
hf :
  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 : ℕ))
hg :
  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)))
hf₁ :
  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))
⊢ lmarginalPartialTraj (X := X) κ a (a + 1) f x₀ =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
have hf₂ : 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: rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
rw :
  ∫⁻ (a_1 : X (a + 1)),
      f
        (updateFinset (π := X) x₀ (Iic (a + 1))
          (_root_.IicProdIoc (X := X) a (a + 1)
            (frestrictLe (π := X) a x₀,
              (piSingleton (X := X) a : (a_2 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
                a_1))) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
hf :
  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 : ℕ))
hg :
  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)))
hf₁ :
  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))
hf₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (a + 1))
⊢ lmarginalPartialTraj (X := X) κ a (a + 1) f x₀ =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
have hg₁ : Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic (a + 1)) z)
Tactic: rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
⊢ ∫⁻ (a_1 : X (a + 1)),
      f
        (updateFinset (π := X) x₀ (Iic (a + 1))
          (_root_.IicProdIoc (X := X) a (a + 1)
            (frestrictLe (π := X) a x₀,
              (piSingleton (X := X) a : (a_2 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
                a_1))) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : X (a + 1)),
      f
        (update (β := X) x₀ (a + 1)
          x) ∂(κ a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure (X (a + 1))) (frestrictLe (π := X) a x₀)
have congrm : ∀ (x : X (a + 1)) (i : ℕ),
  updateFinset (π := X) x₀ (Iic (a + 1))
      (_root_.IicProdIoc (X := X) a (a + 1)
        (frestrictLe (π := X) a x₀,
          (piSingleton (X := X) a : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) x))
      i =
    update (β := X) x₀ (a + 1) x i
Tactic: congrm ∫⁻ x, f (fun i ↦ ?_) ∂_
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
⊢ updateFinset (π := X) x₀ (Iic (a + 1))
      (_root_.IicProdIoc (X := X) a (a + 1)
        (frestrictLe (π := X) a x₀,
          (piSingleton (X := X) a : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) x))
      i =
    update (β := X) x₀ (a + 1) x i
have simp : Eq.{u_1 + 1} (α := X i)
  (if h : i ≤ a + 1 then if h : i ≤ a then x₀ i else @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i sorry else x₀ i)
  (if h : i = a + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x sorry else x₀ i)
Tactic: simp only [updateFinset, mem_Iic, IicProdIoc_def, frestrictLe_apply, piSingleton,
      MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, update]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ a + 1 then if h : i ≤ a then x₀ i else @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ else x₀ i)
    (if h : i = a + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ else x₀ i)
have pos : ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x sorry
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
pos :
  ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ a + 1 then if h : i ≤ a then x₀ i else @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ else x₀ i)
    (if h : i = a + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ else x₀ i)
have neg : ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : ¬i = a + 1), x₀ i = x₀ i
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
pos :
  ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯
neg : ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : ¬i = a + 1), x₀ i = x₀ i
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ a + 1 then if h : i ≤ a then x₀ i else @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ else x₀ i)
    (if h : i = a + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ else x₀ i)
have pos₁ : ∀ (h1 : i ≤ a + 1) (h2 : ¬i ≤ a) (h : i = a + 1),
  Eq.{u_1 + 1} (α := X i) (@Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i sorry : X i)
    (Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x sorry : X i)
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
pos :
  ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯
neg : ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : ¬i = a + 1), x₀ i = x₀ i
pos₁ :
  ∀ (h1 : i ≤ a + 1) (h2 : ¬i ≤ a) (h : i = a + 1),
    Eq.{u_1 + 1} (α := X i) (@Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ : X i)
      (Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ : X i)
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ a + 1 then if h : i ≤ a then x₀ i else @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ else x₀ i)
    (if h : i = a + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ else x₀ i)
have neg₁ : ∀ (h1 : i ≤ a + 1) (h2 : ¬i ≤ a), ¬i = a + 1 → @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i sorry = x₀ i
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
pos :
  ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯
neg : ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : ¬i = a + 1), x₀ i = x₀ i
pos₁ :
  ∀ (h1 : i ≤ a + 1) (h2 : ¬i ≤ a) (h : i = a + 1),
    Eq.{u_1 + 1} (α := X i) (@Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ : X i)
      (Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ : X i)
neg₁ : ∀ (h1 : i ≤ a + 1) (h2 : ¬i ≤ a), ¬i = a + 1 → @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ = x₀ i
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ a + 1 then if h : i ≤ a then x₀ i else @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ else x₀ i)
    (if h : i = a + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ else x₀ i)
have pos₂ : ∀ (h1 : ¬i ≤ a + 1) (h : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x sorry
Tactic: split_ifs with h1 h2 h3