awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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
rw₂ rw₃ : partialTraj (X := X) κ a c = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c

Tactic:
rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_eq_map, ProbabilityTheory.Kernel.partialTraj_le, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
h : ∀ (x₀ : (n : ℕ) → X n), lmarginalPartialTraj (X := X) κ a b f x₀ = f x₀
⊢ lmarginalPartialTraj (X := X) κ a b 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))
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₀
h₁ : Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic b) z)
⊢ lmarginalPartialTraj (X := X) κ a b f x₀ = f x₀

Tactic:
rw [lmarginalPartialTraj, partialTraj_le hba, Kernel.lintegral_deterministic']

Premises used: ProbabilityTheory.Kernel.partialTraj_le, ProbabilityTheory.Kernel.lmarginalPartialTraj, ProbabilityTheory.Kernel.lintegral_deterministic'
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
h : ∀ (i : ℕ), updateFinset (π := X) x₀ (Iic b) (frestrictLe₂ (π := X) hba (frestrictLe (π := X) a x₀)) i = x₀ i
⊢ f (updateFinset (π := X) x₀ (Iic b) (frestrictLe₂ (π := X) hba (frestrictLe (π := X) a x₀))) = f x₀

Tactic:
congr with i
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
i : ℕ
⊢ updateFinset (π := X) x₀ (Iic b) (frestrictLe₂ (π := X) hba (frestrictLe (π := X) a x₀)) i = x₀ i

Tactic:
simp [updateFinset]

Premises used: Function.updateFinset
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic b) z)

Tactic:
mf.comp measurable_updateFinset

Premises used: Measurable.comp, measurable_updateFinset
-- 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))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic b) z)

Tactic:
exact mf.comp measurable_updateFinset

Premises used: Measurable.comp, measurable_updateFinset
-- 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 g : ((n : ℕ) → X n) → ℝ≥0∞
hfg : f ≤ g
x₀ : (n : ℕ) → X n
⊢ lmarginalPartialTraj (X := X) κ a b f x₀ ≤ lmarginalPartialTraj (X := X) κ a b g x₀

Tactic:
lintegral_mono fun _ ↦ hfg _

Premises used: Function.updateFinset, MeasureTheory.lintegral_mono, Finset.Iic, ProbabilityTheory.Kernel.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))
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)
hg : Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic b) z)
⊢ 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₀)

Tactic:
nth_rw 1 [lmarginalPartialTraj, partialTraj_eq_prod, lintegral_map, lintegral_id_prod]

Premises used: ProbabilityTheory.Kernel.lintegral_id_prod, ProbabilityTheory.Kernel.lintegral_map, ProbabilityTheory.Kernel.lmarginalPartialTraj, ProbabilityTheory.Kernel.partialTraj_eq_prod
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
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
⊢ ∫⁻ (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₀)

Tactic:
congrm ∫⁻ _, f (fun i ↦ ?_) ∂_
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
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 ⋯) else x₀ i)
    (if h : a < i ∧ i ≤ b then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) else x₀ 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:
simp only [updateFinset, mem_Iic, IicProdIoc_def,
      frestrictLe_apply, mem_Ioc]

Premises used: Function.updateFinset, Finset.mem_Iic, IicProdIoc_def, Preorder.frestrictLe_apply, 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 : ℕ), 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 ⋯)
neg₂ : ¬i ≤ b → ¬(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)

Tactic:
split_ifs
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
h : i ≤ b
h_1 : i ≤ a
h_2 : ¬(a < i ∧ i ≤ b)
⊢ x₀ i = x₀ i

Tactic:
rfl
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
h : i ≤ b
h_1 : i ≤ a
h_2 : ¬(a < i ∧ i ≤ b)
⊢ x₀ i = x₀ i

Tactic:
try rfl
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
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 ⋯))

Tactic:
rfl
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
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 ⋯))

Tactic:
try rfl
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
h : ¬i ≤ b
h_1 : ¬(a < i ∧ i ≤ b)
⊢ x₀ i = x₀ i

Tactic:
rfl
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
h : ¬i ≤ b
h_1 : ¬(a < i ∧ i ≤ b)
⊢ x₀ i = x₀ i

Tactic:
try rfl
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
h : i ≤ b
h_1 : i ≤ a
h_2 : a < i ∧ i ≤ b
⊢ x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯)

Tactic:
lia
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
h : i ≤ b
h_1 : ¬i ≤ a
h_2 : ¬(a < i ∧ i ≤ b)
⊢ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯) = x₀ i

Tactic:
lia
-- 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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : (i : ↥(Ioc a b)) → X (↑i : ℕ)
i : ℕ
h : ¬i ≤ b
h_1 : a < i ∧ i ≤ b
⊢ x₀ i = x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a b) i ⋯)

Tactic:
lia
-- 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 : ℕ), IsSFiniteKernel (κ n)
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 b)) → X (↑i : ℕ))) ↦
    f (updateFinset (π := X) x₀ (Iic b) (_root_.IicProdIoc (X := X) a b a_1))

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 : ℕ), IsSFiniteKernel (κ n)
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 b)) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a b)

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 : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic b) 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))
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))
hg₁ : Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic (a + 1)) z)
⊢ 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₀)

Tactic:
rw [lmarginalPartialTraj, partialTraj_succ_self, lintegral_map, lintegral_id_prod, lintegral_map]

Premises used: ProbabilityTheory.Kernel.lintegral_id_prod, ProbabilityTheory.Kernel.lintegral_map, ProbabilityTheory.Kernel.partialTraj_succ_self, ProbabilityTheory.Kernel.lmarginalPartialTraj
-- 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
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
⊢ ∫⁻ (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:
congrm ∫⁻ x, f (fun i ↦ ?_) ∂_
-- 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 : ℕ
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 ⋯ 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)
⊢ 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:
simp only [updateFinset, mem_Iic, IicProdIoc_def, frestrictLe_apply, piSingleton,
      MeasurableEquiv.coe_mk, Equiv.coe_fn_mk, update]

Premises used: Function.update, Function.updateFinset, Finset.mem_Iic, MeasurableEquiv.coe_mk, IicProdIoc_def, Preorder.frestrictLe_apply, Equiv.coe_fn_mk, MeasurableEquiv.piSingleton
-- 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 : ℕ
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
pos₂ : ∀ (h1 : ¬i ≤ a + 1) (h : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯
neg₂ : ∀ (h1 : ¬i ≤ a + 1), ¬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)

Tactic:
split_ifs with h1 h2 h3
-- 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
h3 : ¬i = a + 1
⊢ x₀ i = x₀ i

Tactic:
rfl
-- 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
h3 : ¬i = a + 1
⊢ x₀ i = x₀ i

Tactic:
try rfl
-- 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.{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)

Tactic:
rfl
-- 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.{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)

Tactic:
try rfl
-- 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 = x₀ i

Tactic:
rfl
-- 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 = x₀ i

Tactic:
try rfl
-- 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
h3 : i = a + 1
⊢ x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯

Tactic:
lia