mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hbc
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ n ≤ n + 1

Tactic:
fun_prop

Goal state after:
case inl.refine_2.hbc
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ n ≤ n + 1
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable (IocProdIoc a n (n + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable id

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable (Prod.map (restrict₂ ⋯) id)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable (IocProdIoc a n (n + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable (_root_.IicProdIoc n (n + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_2.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a n).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)
x₀ : (i : ↥(Iic a)) → X ↑i
this : restrict₂ ⋯ ∘ _root_.IicProdIoc n (n + 1) = IocProdIoc a n (n + 1) ∘ Prod.map (restrict₂ ⋯) id
⊢ Measurable ⇑(piSingleton n)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
hf_eq_tsum : f = ∑' (n : ℕ), fs n
⊢ ∀ (n : ℕ), Measurable (Function.uncurry (fs n))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable (Function.uncurry fun a x ↦ ↑(f a x) * g a x)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable fun x ↦ ↑(f a x)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0
g : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
hg : Measurable (Function.uncurry g)
a : α
⊢ Measurable fun x ↦ g a x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯)
      (⇑(partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) 0 (I.sup id)) ∘ₘ Measure.pi fun i ↦ μ ↑i) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

pp: case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (frestrictLe (I.sup id))

pp: case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (restrict₂ ⋯)

pp: case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (Iic (I.sup id)).restrict

Tactic:
partialTraj_const,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯)
      (⇑((Kernel.id ×ₖ const ((i : ↥(Iic 0)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)).map (_root_.IicProdIoc 0 (I.sup id))) ∘ₘ
        Measure.pi fun i ↦ μ ↑i) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (frestrictLe (I.sup id))

case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (restrict₂ ⋯)

case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (Iic (I.sup id)).restrict
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable fun x ↦ κ.rnDerivAux η a x

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (_root_.IicProdIoc 0 (I.sup id))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (frestrictLe (I.sup id))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable (Iic (I.sup id)).restrict

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
h_le : κ ≤ κ + η
hα : ¬Countable α
this : MeasurableSpace.CountablyGenerated γ
⊢ Measurable fun a ↦ (a, ())

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ Measurable (Function.uncurry fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (Prod.map (restrict₂ ⋯) id)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (IocProdIoc a k (k + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft (fun i ↦ X ↑i) (e.restrictPreimageFinset I))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (_root_.IicProdIoc k (k + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hf
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable (I.preimage ⇑e ⋯).restrict

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ MeasurableSet (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S)

Tactic:
fun_prop

Goal state after:
case hs
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ MeasurableSet (⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I)) ⁻¹' S)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (restrict₂ ⋯)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(piCongrLeft X e)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (_root_.IicProdIoc a k)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case hg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
⊢ Measurable (Function.uncurry fun a x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
e : ℕ ≃ ι
I : Finset ι
S : Set ((i : ↥I) → X ↑i)
hS : MeasurableSet S
hs : cylinder I S ∈ measurableCylinders X
⊢ Measurable ⇑(Equiv.piCongrLeft (fun b ↦ X ↑b) (e.restrictPreimageFinset I))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (_root_.IicProdIoc a (k + 1))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable ⇑(MeasurableEquiv.IicProdIoc ⋯).symm

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable id

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (Prod.map id (IocProdIoc a k (k + 1)))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable ⇑(MeasurableEquiv.IicProdIoc ⋯)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable ⇑prodAssoc

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1)))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable fun x ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Measurable (Prod.map (_root_.IicProdIoc a k) id)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable fun b ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b)

Tactic:
fun_prop

Goal state after: