awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
have 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₀)
Tactic: rw [← traj_comp_partialTraj hab] at i_f
Cleared hypotheses: i_f
-- 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
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₀)
⊢ condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      f =ᶠ[ae (F := Measure ((n : ℕ) → X n))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))]
    fun (x : (n : ℕ) → X n) ↦
    @integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (y : (n : ℕ) → X n) ↦ f y
have i_f' : @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
-- 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₀)
i_f' :
  @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₀))
⊢ condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      f =ᶠ[ae (F := Measure ((n : ℕ) → X n))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))]
    fun (x : (n : ℕ) → X n) ↦
    @integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (y : (n : ℕ) → X n) ↦ f y
have refine_1 : ∀ (s : Set ((i : ℕ) → X i)),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞)
        ((((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
                Measure ((n : ℕ) → X n)) :
              (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
            s :
          ℝ≥0∞)
        (∞ : ℝ≥0∞) →
      Eq.{u_2 + 1} (α := E)
        (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
          (Measure.restrict ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) s)
          fun (x : (i : ℕ) → 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) ∘
              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)) x₀) s)
          fun (x : (i : ℕ) → X i) ↦ f x)
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq (piLE.le _) i_f
    (fun s _ _ ↦ i_f'.comp_aemeasurable (measurable_frestrictLe b).aemeasurable |>.integrableOn)
    ?_ ?_ |>.symm
-- 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₀)
i_f' :
  @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₀))
⊢ AEStronglyMeasurable.{u_1, u_2} (α := (i : ℕ) → X i) (β := E) (m₀ := MeasurableSpace.pi (X := 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) ∘
      frestrictLe (π := X) b)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
have refine_2 : AEStronglyMeasurable.{u_1, u_2} (α := (i : ℕ) → X i) (β := E) (m₀ := MeasurableSpace.pi (X := 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) ∘
    frestrictLe (π := X) b)
  ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: rw [piLE_eq_comap_frestrictLe]
-- 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₀)
i_f' :
  @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₀))
t : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mt : MeasurableSet t
⊢ Eq.{u_2 + 1} (α := E)
    (@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 ⁻¹' t))
      fun (x : (i : ℕ) → X i) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b 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 ⁻¹' t))
      fun (y : (n : ℕ) → X n) ↦ f y)
have refine_1 : Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
Tactic: rw [← setIntegral_map mt i_f'.1, ← map_apply, traj_map_frestrictLe,
      setIntegral_traj_partialTraj hab i_f mt]
-- 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₀)
i_f' :
  @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₀))
t : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mt : MeasurableSet t
refine_1 : Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
⊢ Eq.{u_2 + 1} (α := E)
    (@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 ⁻¹' t))
      fun (x : (i : ℕ) → X i) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b 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 ⁻¹' t))
      fun (y : (n : ℕ) → X n) ↦ f y)
have refine_1₁ : AEMeasurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (_m := MeasurableSpace.pi (X := X))
  (frestrictLe (π := X) b) ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: rw [← setIntegral_map mt i_f'.1, ← map_apply, traj_map_frestrictLe,
      setIntegral_traj_partialTraj hab i_f mt]
-- 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
inst_4 : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
⊢ condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      f =ᶠ[ae (F := Measure ((n : ℕ) → X n))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))]
    fun (x : (n : ℕ) → X n) ↦
    @integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic c)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x))
      fun (y : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f
        (updateFinset (π := X) x (Iic c) y)
have i_cf : @Integrable _ _ _ _ (MeasurableSpace.pi (X := X))
  (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
  ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: have i_cf : Integrable ((traj κ a x₀)[f | piLE c]) (traj κ a x₀) :=
    integrable_condExp
-- 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
inst_4 : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_cf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X))
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      f =ᶠ[ae (F := Measure ((n : ℕ) → X n))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))]
    fun (x : (n : ℕ) → X n) ↦
    @integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic c)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x))
      fun (y : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f
        (updateFinset (π := X) x (Iic c) y)
have mcf : StronglyMeasurable
  (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
Tactic: have mcf : StronglyMeasurable ((traj κ a x₀)[f | piLE c]) :=
    stronglyMeasurable_condExp.mono (piLE.le c)
-- 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 c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_cf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X))
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
mcf :
  StronglyMeasurable
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
x : (n : ℕ) → X n
h1 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f x
h2 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    @integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (y : (n : ℕ) → X n) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f y
y : (n : ℕ) → X n
⊢ condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f y =
    condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f
      (updateFinset (π := X) x (Iic c) (frestrictLe (π := X) c y))
have h : ∀ i ∈ Set.Iic c, y i = updateFinset (π := X) x (Iic c) (frestrictLe (π := X) c y) i
Tactic: apply stronglyMeasurable_condExp.dependsOn_of_piLE
-- 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 c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_cf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X))
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
mcf :
  StronglyMeasurable
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
x : (n : ℕ) → X n
h1 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f x
h2 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    @integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (y : (n : ℕ) → X n) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f y
y : (n : ℕ) → X n
⊢ ∀ i ∈ Set.Iic c, y i = updateFinset (π := X) x (Iic c) (frestrictLe (π := X) c y) i
have h : ∀ i ≤ c, y i = if i ≤ c then y i else x i
Tactic: simp only [Set.mem_Iic, updateFinset, mem_Iic, frestrictLe_apply, dite_eq_ite]
-- 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)
μ₀ : Measure (X 0)
inst_2 : IsProbabilityMeasure μ₀
⊢ IsProbabilityMeasure (α := (n : ℕ) → X n) (m0 := MeasurableSpace.pi (X := X))
    (Measure.bind (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (mα := MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
      (Measure.map
        (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
              X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
          (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
        μ₀)
      (⇑(traj (X := X) κ 0) : (a : (i : ↥(Iic 0)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)))
have this : IsProbabilityMeasure (α := (i : ↥(Iic 0)) → X (↑i : ℕ)) (m0 :=
  MeasurableSpace.pi (X := fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)))
  (Measure.map
    (⇑(MeasurableEquiv.symm (piUnique fun (i : ↥(Iic 0)) ↦ X (↑i : ℕ)) :
          X (↑default : ℕ) ≃ᵐ ((i : ↥(Iic 0)) → X (↑i : ℕ))) :
      (a : X (↑default : ℕ)) → (i : ↥(Iic 0)) → X (↑i : ℕ))
    μ₀)
Tactic: have : IsProbabilityMeasure (μ₀.map (MeasurableEquiv.piUnique ((fun i : Iic 0 ↦ X i))).symm) :=
    Measure.isProbabilityMeasure_map <| by fun_prop