awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
simp_rw :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u) fun (x : (n : ℕ) → X n) ↦
      (frestrictLe (π := X) b ⁻¹' A).indicator
        ((fun (x_1 : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x_1 x) ∘ frestrictLe (π := X) b) x)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u) fun (x : (i : ℕ) → X i) ↦
      (frestrictLe (π := X) b ⁻¹' A).indicator (fun (y : (n : ℕ) → X n) ↦ f (frestrictLe (π := X) b y) y) x)
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u) fun (x : (n : ℕ) → X n) ↦
      A.indicator (fun (x_1 : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x_1 x) (frestrictLe (π := X) b x))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      (Measure.restrict ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u)
        (frestrictLe (π := X) b ⁻¹' A))
      fun (y : (n : ℕ) → X n) ↦ f (frestrictLe (π := X) b y) y)

Tactic:
simp_rw [← Set.indicator_comp_right, ← integral_indicator (measurable_frestrictLe b hA)]

Premises used: MeasureTheory.integral_indicator, Set.indicator_comp_right, Preorder.measurable_frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u) fun (x : (n : ℕ) → X n) ↦
      (frestrictLe (π := X) b ⁻¹' A).indicator
        ((fun (x_1 : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x_1 x) ∘ frestrictLe (π := X) b) x)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u) fun (x : (i : ℕ) → X i) ↦
      (frestrictLe (π := X) b ⁻¹' A).indicator (fun (y : (n : ℕ) → X n) ↦ f (frestrictLe (π := X) b y) y) x)

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
⊢ Integrable ((SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)

Tactic:
hf.indicator (hA.prod .univ)

Premises used: MeasurableSet.prod, MeasurableSet.univ, MeasureTheory.Integrable.indicator
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
h :
  (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
      A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x) =
    (SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f)
⊢ Integrable.{u_2, u_1} (ε := E)
    (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
      A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)

Tactic:
convert! hf.indicator (hA.prod .univ)

Premises used: MeasurableSet.prod, MeasurableSet.univ, MeasureTheory.Integrable.indicator
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
h :
  ∀ (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n),
    uncurry
        (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
          A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x)
        (x, y) =
      (SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f) (x, y)
⊢ (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
      A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x) =
    (SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f)

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
x : (i : ↥(Iic b)) → X (↑i : ℕ)
y : (n : ℕ) → X n
pos :
  ∀ (hx : x ∈ A),
    uncurry
        (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
          A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x)
        (x, y) =
      (SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f) (x, y)
neg :
  ∀ (hx : x ∉ A),
    uncurry
        (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
          A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x)
        (x, y) =
      (SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f) (x, y)
⊢ uncurry
      (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
        A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x)
      (x, y) =
    (SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f) (x, y)

Tactic:
by_cases hx : x ∈ A
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
x : (i : ↥(Iic b)) → X (↑i : ℕ)
y : (n : ℕ) → X n
hx : x ∈ A
⊢ uncurry
      (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
        A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x)
      (x, y) =
    (SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f) (x, y)

Tactic:
simp [uncurry_def, hx]

Premises used: Function.uncurry_def
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
x : (i : ↥(Iic b)) → X (↑i : ℕ)
y : (n : ℕ) → X n
hx : x ∉ A
⊢ uncurry
      (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
        A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x)
      (x, y) =
    (SProd.sprod (β := Set ((n : ℕ) → X n)) A Set.univ).indicator (uncurry f) (x, y)

Tactic:
simp [uncurry_def, hx]

Premises used: Function.uncurry_def
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (Measure.restrict
        ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀) A)
      fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        f y)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      (Measure.restrict ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
        (frestrictLe (π := X) b ⁻¹' A))
      fun (y : (n : ℕ) → X n) ↦ f y)

Tactic:
setIntegral_traj_partialTraj' hab ?_ hA

Premises used: ProbabilityTheory.Kernel.setIntegral_traj_partialTraj'
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
refine :
  Integrable.{u_2, u_1} (ε := E) (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (Measure.restrict
        ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀) A)
      fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        f y)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      (Measure.restrict ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
        (frestrictLe (π := X) b ⁻¹' A))
      fun (y : (n : ℕ) → X n) ↦ f y)

Tactic:
refine setIntegral_traj_partialTraj' hab ?_ hA

Premises used: ProbabilityTheory.Kernel.setIntegral_traj_partialTraj'
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
rw :
  ∀
    (hf :
      Integrable f
        ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
            traj (X := X) κ b).snd)
    {A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))} (hA : MeasurableSet A),
    Integrable.{u_2, u_1} (ε := E) (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
        traj (X := X) κ b)
⊢ Integrable.{u_2, u_1} (ε := E) (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)

Tactic:
rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf

Premises used: MeasureTheory.Measure.snd_compProd, ProbabilityTheory.Kernel.traj_comp_partialTraj, ProbabilityTheory.Kernel.comp_apply
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  Integrable f
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
        traj (X := X) κ b).snd
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
⊢ Integrable.{u_2, u_1} (ε := E) (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)

Tactic:
hf.comp_measurable measurable_snd

Premises used: MeasureTheory.Integrable.comp_measurable, measurable_snd
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  Integrable f
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
        traj (X := X) κ b).snd
A : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
hA : MeasurableSet A
⊢ Integrable.{u_2, u_1} (ε := E) (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)

Tactic:
exact hf.comp_measurable measurable_snd

Premises used: MeasureTheory.Integrable.comp_measurable, measurable_snd
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
rw :
  @Integrable.{u_2, u_1} E _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
    (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        f y)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
⊢ @Integrable.{u_2, u_1} E _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
    (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        f y)
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))

Tactic:
rw [← map_apply _ (measurable_frestrictLe _), traj_map_frestrictLe _ _]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.traj_map_frestrictLe, Preorder.measurable_frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)

Tactic:
rw [← traj_comp_partialTraj hab] at i_f

Premises used: ProbabilityTheory.Kernel.traj_comp_partialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ @Integrable.{u_2, u_1} E _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
    (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        f y)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)

Tactic:
i_f.integral_comp

Premises used: MeasureTheory.Integrable.integral_comp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ @Integrable.{u_2, u_1} E _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
    (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        f y)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)

Tactic:
exact i_f.integral_comp

Premises used: MeasureTheory.Integrable.integral_comp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
inst_4 : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ @Integrable.{u_2, u_1} E _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
    (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        f y)
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))

Tactic:
have i_f' : Integrable (fun x ↦ ∫ y, f y ∂(traj κ b) x)
      (((traj κ a) x₀).map (frestrictLe b)) := by
    rw [← map_apply _ (measurable_frestrictLe _), traj_map_frestrictLe _ _]
    rw [← traj_comp_partialTraj hab] at i_f
    exact i_f.integral_comp