awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 : ((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 : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)
hf' :
  @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f)
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      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 x y)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      f (frestrictLe (π := X) b x) x)
have simp_rw : Eq.{u_2 + 1} (α := E)
  (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
    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) ↦
      uncurry f (x, y))
  (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
    uncurry f (frestrictLe (π := X) b x, x))
Tactic: simp_rw [← uncurry_apply_pair f, ← Measure.integral_compProd hf,
    partialTraj_compProd_traj hab, integral_map (by fun_prop) hf'.1]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 : ((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 : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)
hf' :
  @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f)
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
simp_rw :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      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) ↦
        uncurry f (x, y))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      uncurry f (frestrictLe (π := X) b x, x))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      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 x y)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      f (frestrictLe (π := X) b x) x)
have simp_rw₁ : Eq.{u_2 + 1} (α := E)
  (∫ (x : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)),
    uncurry f
      x ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)
  (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
    uncurry f (frestrictLe (π := X) b x, x))
Tactic: simp_rw [← uncurry_apply_pair f, ← Measure.integral_compProd hf,
    partialTraj_compProd_traj hab, integral_map (by fun_prop) hf'.1]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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₀)
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      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))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      f x)
have apply : 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: apply integral_traj_partialTraj' hab
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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₀)
⊢ 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)
have 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
Tactic: rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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 := 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 : ℕ))) u) 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 x y)
    (@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)
have 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) ↦
    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: rw [← integral_integral_indicator _ _ _ hA, integral_traj_partialTraj' hab]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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
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) ↦
      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)
⊢ 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 : ℕ))) u) 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 x y)
    (@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)
have rw₁ : 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: rw [← integral_integral_indicator _ _ _ hA, integral_traj_partialTraj' hab]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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) ↦
      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)
have 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)
Tactic: simp_rw [← Set.indicator_comp_right, ← integral_indicator (measurable_frestrictLe b hA)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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.{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)
have 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)
Tactic: convert! hf.indicator (hA.prod .univ)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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
⊢ (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)
have 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)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hx : x ∈ A
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hx : x ∈ A
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
have 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)
Tactic: refine setIntegral_traj_partialTraj' hab ?_ hA
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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
⊢ 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)
have 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)
Tactic: rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf
Cleared hypotheses: hf, A, hA
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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₀))
have 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₀)
Tactic: rw [← map_apply _ (measurable_frestrictLe _), traj_map_frestrictLe _ _]