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)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
this :
  IsMarkovKernel (β := (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) (mβ :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b (b + 1))) ↦ X (↑i : ℕ)))
    ((κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)))
inl :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) b (b + 1))
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have inl₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (b + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) sorry)
Tactic: rw [partialTraj_succ_eq_comp hab, map_comp, partialTraj_succ_self, ← map_comp_right,
      frestrictLe₂_comp_IicProdIoc, ← fst_eq, fst_prod, id_comp]
-- 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 : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have inr : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (deterministic (frestrictLe₂ (π := X) sorry ∘ frestrictLe₂ (π := X) sorry) sorry) (deterministic (frestrictLe₂ (π := X) sorry) sorry)
Tactic: rw [partialTraj_le (Nat.succ_le_of_lt hba), partialTraj_le hba.le, deterministic_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 : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
inr :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) ⋯ ∘ frestrictLe₂ (π := X) ⋯) ⋯) (deterministic (frestrictLe₂ (π := X) ⋯) ⋯)
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have inr₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (b + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) sorry)
Tactic: rw [partialTraj_le (Nat.succ_le_of_lt hba), partialTraj_le hba.le, deterministic_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a k : ℕ
h : b ≤ k
hk : (partialTraj (X := X) κ a k).map (frestrictLe₂ (π := X) h) = partialTraj (X := X) κ a b
⊢ map (partialTraj (X := X) κ a (k + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have succ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) sorry)
Tactic: rw [← hk, ← frestrictLe₂_comp_frestrictLe₂ h k.le_succ, map_comp_right,
      partialTraj_succ_map_frestrictLe₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a k : ℕ
h : b ≤ k
hk : (partialTraj (X := X) κ a k).map (frestrictLe₂ (π := X) h) = partialTraj (X := X) κ a b
succ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) ⋯)
⊢ map (partialTraj (X := X) κ a (k + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have succ₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic k)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) h)
Tactic: rw [← hk, ← frestrictLe₂_comp_frestrictLe₂ h k.le_succ, map_comp_right,
      partialTraj_succ_map_frestrictLe₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hbc : b ≤ c
⊢ (partialTraj (X := X) κ a c).map (frestrictLe₂ (π := X) hbc) = partialTraj (X := X) κ a b
have base : (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) sorry) = partialTraj (X := X) κ a b
Tactic: induction c, hbc using Nat.le_induction with
  | base => exact map_id ..
  | succ k h hk =>
    rw [← hk, ← frestrictLe₂_comp_frestrictLe₂ h k.le_succ, map_comp_right,
      partialTraj_succ_map_frestrictLe₂]
    all_goals fun_prop
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hbc : b ≤ c
base : (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
⊢ (partialTraj (X := X) κ a c).map (frestrictLe₂ (π := X) hbc) = partialTraj (X := X) κ a b
have succ : ∀ (k : ℕ) (h : b ≤ k) (hk : (partialTraj (X := X) κ a k).map (frestrictLe₂ (π := X) h) = partialTraj (X := X) κ a b),
  map (partialTraj (X := X) κ a (k + 1)) (frestrictLe₂ (π := X) sorry) = partialTraj (X := X) κ a b
Tactic: induction c, hbc using Nat.le_induction with
  | base => exact map_id ..
  | succ k h hk =>
    rw [← hk, ← frestrictLe₂_comp_frestrictLe₂ h k.le_succ, map_comp_right,
      partialTraj_succ_map_frestrictLe₂]
    all_goals fun_prop
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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)
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
hbc : b ≤ c
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe₂ (π := X) hbc)
      ((partialTraj (X := X) κ a c : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ))) x₀))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
have rw : Eq (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (((partialTraj (X := X) κ a c).map (frestrictLe₂ (π := X) hbc) :
        (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
      x₀ :
    Measure ((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 : ℕ)))
Tactic: rw [← map_apply _ (by fun_prop), partialTraj_map_frestrictLe₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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)
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
hbc : b ≤ c
rw :
  Eq (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (((partialTraj (X := X) κ a c).map (frestrictLe₂ (π := X) hbc) :
          (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        x₀ :
      Measure ((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 : ℕ)))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe₂ (π := X) hbc)
      ((partialTraj (X := X) κ a c : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ))) x₀))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
have rw₁ : Eq (α := Measure ((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 : ℕ)))
  ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
    Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
Tactic: rw [← map_apply _ (by fun_prop), partialTraj_map_frestrictLe₂]
-- 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 : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have inl : ∀ (hbc : b ≤ c), partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
Tactic: obtain hbc | hcb := le_total b c
-- 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 : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
inl : ∀ (hbc : b ≤ c), partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have inr : ∀ (hcb : c ≤ b), partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
Tactic: obtain hbc | hcb := le_total b c
-- 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 : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hbc : b ≤ c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have inl : partialTraj (X := X) κ a c = partialTraj (X := X) κ a c
Tactic: rw [partialTraj_comp_partialTraj hab hbc]
-- 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 : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hcb : c ≤ b
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have inr : deterministic (frestrictLe₂ (π := X) hcb) sorry ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
Tactic: rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]
-- 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 : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hcb : c ≤ b
inr : deterministic (frestrictLe₂ (π := X) hcb) ⋯ ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have inr₁ : (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) hcb) = partialTraj (X := X) κ a c
Tactic: rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]
-- 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 : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hcb : c ≤ b
inr : deterministic (frestrictLe₂ (π := X) hcb) ⋯ ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
inr₁ : (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) hcb) = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have inr₂ : partialTraj (X := X) κ a c = partialTraj (X := X) κ a c
Tactic: rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
b c : ℕ
hcb : c ≤ b
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have rw : deterministic (frestrictLe₂ (π := X) hcb) sorry ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
Tactic: rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
b c : ℕ
hcb : c ≤ b
rw : deterministic (frestrictLe₂ (π := X) hcb) ⋯ ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have rw₁ : (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) hcb) = partialTraj (X := X) κ a c
Tactic: rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
b c : ℕ
hcb : c ≤ b
rw : deterministic (frestrictLe₂ (π := X) hcb) ⋯ ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
rw₁ : (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) hcb) = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have rw₂ : partialTraj (X := X) κ a c = partialTraj (X := X) κ a c
Tactic: rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
⊢ lmarginalPartialTraj (X := X) κ a b f = f
have h : ∀ (x₀ : (n : ℕ) → X n), lmarginalPartialTraj (X := X) κ a b f x₀ = f x₀
Tactic: ext x₀
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ lmarginalPartialTraj (X := X) κ a b f x₀ = f x₀
have h : f (updateFinset (π := X) x₀ (Iic b) (frestrictLe₂ (π := X) hba (frestrictLe (π := X) a x₀))) = f x₀
Tactic: rw [lmarginalPartialTraj, partialTraj_le hba, Kernel.lintegral_deterministic']
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
h : f (updateFinset (π := X) x₀ (Iic b) (frestrictLe₂ (π := X) hba (frestrictLe (π := X) a x₀))) = f x₀
⊢ lmarginalPartialTraj (X := X) κ a b f x₀ = f x₀
have h₁ : Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic b) z)
Tactic: rw [lmarginalPartialTraj, partialTraj_le hba, Kernel.lintegral_deterministic']
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ f (updateFinset (π := X) x₀ (Iic b) (frestrictLe₂ (π := X) hba (frestrictLe (π := X) a x₀))) = f x₀
have h : ∀ (i : ℕ), updateFinset (π := X) x₀ (Iic b) (frestrictLe₂ (π := X) hba (frestrictLe (π := X) a x₀)) i = x₀ i
Tactic: congr with i
-- 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
⊢ lmarginalPartialTraj (X := X) κ a b f x₀ =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
have nth_rw : ∫⁻ (b_1 : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
    f
      (updateFinset (π := X) x₀ (Iic b)
        (_root_.IicProdIoc (X := X) a b
          (frestrictLe (π := X) a x₀,
            b_1))) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) sorry) :
        (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
      (frestrictLe (π := X) a x₀) =
  ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
    f
      (updateFinset (π := X) x₀ (Ioc a b)
        x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) sorry) :
        (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
      (frestrictLe (π := X) a x₀)
Tactic: nth_rw 1 [lmarginalPartialTraj, partialTraj_eq_prod, lintegral_map, lintegral_id_prod]
-- 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
nth_rw :
  ∫⁻ (b_1 : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic b)
          (_root_.IicProdIoc (X := X) a b
            (frestrictLe (π := X) a x₀,
              b_1))) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
⊢ lmarginalPartialTraj (X := X) κ a b f x₀ =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
have hf : Measurable (β := ℝ≥0∞) fun (a_1 : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) ↦
  f (updateFinset (π := X) x₀ (Iic b) (_root_.IicProdIoc (X := X) a b a_1))
Tactic: nth_rw 1 [lmarginalPartialTraj, partialTraj_eq_prod, lintegral_map, lintegral_id_prod]
-- 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
nth_rw :
  ∫⁻ (b_1 : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic b)
          (_root_.IicProdIoc (X := X) a b
            (frestrictLe (π := X) a x₀,
              b_1))) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
hf :
  Measurable (β := ℝ≥0∞) fun (a_1 : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) ↦
    f (updateFinset (π := X) x₀ (Iic b) (_root_.IicProdIoc (X := X) a b a_1))
⊢ lmarginalPartialTraj (X := X) κ a b f x₀ =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
have hf₁ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
  (_root_.IicProdIoc (X := X) a b)
Tactic: nth_rw 1 [lmarginalPartialTraj, partialTraj_eq_prod, lintegral_map, lintegral_id_prod]
-- 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
nth_rw :
  ∫⁻ (b_1 : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic b)
          (_root_.IicProdIoc (X := X) a b
            (frestrictLe (π := X) a x₀,
              b_1))) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
hf :
  Measurable (β := ℝ≥0∞) fun (a_1 : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) ↦
    f (updateFinset (π := X) x₀ (Iic b) (_root_.IicProdIoc (X := X) a b a_1))
hf₁ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a b)
⊢ lmarginalPartialTraj (X := X) κ a b f x₀ =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
have hg : Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic b) z)
Tactic: nth_rw 1 [lmarginalPartialTraj, partialTraj_eq_prod, lintegral_map, lintegral_id_prod]
-- 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
⊢ ∫⁻ (b_1 : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic b)
          (_root_.IicProdIoc (X := X) a b
            (frestrictLe (π := X) a x₀,
              b_1))) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀) =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
have congrm : ∀ (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
Tactic: congrm ∫⁻ _, f (fun i ↦ ?_) ∂_