mathlib-initiative/mathlib-tactics huggingface dataset:
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))

pp: case hfg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
⊢ ∀ (a : α), (fun x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᵐ[(κ + η) a] fun x ↦ 1

Tactic:
·

Goal state after:
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))
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case hfg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
⊢ ∀ (a : α), (fun x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᵐ[(κ + η) a] fun x ↦ 1

Tactic:
·

Goal state after:
case hfg
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
h_le : κ ≤ κ + η
⊢ ∀ (a : α), (fun x ↦ ENNReal.ofReal (κ.rnDerivAux (κ + η) a x)) ≤ᵐ[(κ + η) a] fun x ↦ 1
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case inr
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
k : ℕ
x : (n : ℕ) → X n
h : ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)

Tactic:
·

Goal state after:
case inr
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
x✝ : ∀ (n : ℕ), Nonempty (X n)
a : ℕ → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (Iic (a n)) (S n)
χ : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (χ n) ↑(Iic (a n))
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀) =
      lmarginalPartialTraj κ p (a n) (χ n) (updateFinset y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv : ∀ (k M n : ℕ), a n ≤ M → lmarginalPartialTraj κ k M (χ n) = lmarginalPartialTraj κ k (a n) (χ n)
anti_lma : ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x
k : ℕ
x : (n : ℕ) → X n
h : ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)
⊢ ∃ l, Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 l)
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 : α
⊢ MeasurableSet {x | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}

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)

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

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a, x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x} → ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

Tactic:
·

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ MeasurableSet {x | ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x}
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)

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

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a, x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x} → ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

Tactic:
·

Goal state after:
α : 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)
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 : α
⊢ Measurable (Function.uncurry fun a x ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x))

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a, x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x} → ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) = 0 x

Tactic:
·

Goal state after:
case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry fun a x ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x))
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ MeasurableSet
    {x |
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x}

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

pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable
    (Function.uncurry fun a x ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x)

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a,
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x

Tactic:
·

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ MeasurableSet
    {x |
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x}
Module: Mathlib.Probability.Kernel.RadonNikodym

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

pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable
    (Function.uncurry fun a x ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x)

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a,
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x

Tactic:
·

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun b ↦
    ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a b) * κ.rnDeriv η a b
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✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable
    (Function.uncurry fun a x ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x)

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ∀ᵐ (x : γ) ∂(κ + η) a,
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x = 0 x

Tactic:
·

Goal state after:
case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable
    (Function.uncurry fun a x ↦
      ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) - ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x) * κ.rnDeriv η a x)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b

pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b

Tactic:
·

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 1 - κ.rnDerivAux (κ + η) a x ≠ 0

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
·

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 1 - κ.rnDerivAux (κ + η) a x ≠ 0
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
·

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 ≤ 1 - κ.rnDerivAux (κ + η) a x
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x

Tactic:
·

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
x : γ
hx : κ.rnDerivAux (κ + η) a x < 1
⊢ 0 < 1 - κ.rnDerivAux (κ + η) a x
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b

Tactic:
·

Goal state after:
case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ Measurable
    (Function.uncurry fun a x ↦
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)

pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ ∫⁻ (b : γ) in s,
      ↑(κ.rnDerivAux (κ + η) a b).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b ∂(κ + η) a =
    (κ a) s

Tactic:
·

Goal state after:
case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hsm : MeasurableSet s
hs : s ⊆ κ.mutuallySingularSetSlice η a
hs' : ∀ x ∈ s, 1 ≤ κ.rnDerivAux (κ + η) a x
⊢ Measurable
    (Function.uncurry fun a x ↦
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ deterministic (frestrictLe₂ ⋯ ∘ frestrictLe₂ ⋯) ⋯ = deterministic (frestrictLe₂ ⋯) ⋯

pp: case inr.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ Measurable (frestrictLe₂ ⋯)

Tactic:
·

Goal state after:
case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ deterministic (frestrictLe₂ ⋯ ∘ frestrictLe₂ ⋯) ⋯ = deterministic (frestrictLe₂ ⋯) ⋯
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ Measurable (frestrictLe₂ ⋯)

Tactic:
·

Goal state after:
case inr.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ Measurable (frestrictLe₂ ⋯)
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 : α
⊢ ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂η a = 0

pp: case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
·

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂η a = 0
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 : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
·

Goal state after:
case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hbc : b ≤ c
⊢ partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c

pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hcb : c ≤ b
⊢ partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c

Tactic:
·

Goal state after:
case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hbc : b ≤ c
⊢ partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c