mathlib-initiative/mathlib-tactics huggingface dataset:
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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
n : ℕ
⊢ B n = cylinder (t n) (T n)

Tactic:
by

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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
n : ℕ
⊢ Measurable ⇑(g n)

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ ((partialTraj κ a (a + 1)).map fun x ↦ x ⟨a + 1, ⋯⟩) = κ a

Tactic:
by

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

Goal state before:
pp: 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
l : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
hl : ∀ (k : ℕ) (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = ε
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → ((i : ↥(Iic k)) → X ↑i) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X ↑i),
    (∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) y)) →
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (χ n) (update (updateFinset x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction x₀ ind
k : ℕ
x : (i : ℕ) → X i
n : ℕ
⊢ ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) (frestrictLe p z))

Tactic:
by

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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
⊢ ⋂ n, B n = ∅

Tactic:
by

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✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
by

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

Goal state before:
pp: 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 : ℕ
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b

Tactic:
by

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

Goal state before:
pp: 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 : ℕ
⊢ (partialTraj κ a (b + 1)).map (frestrictLe₂ ⋯) = partialTraj κ a b

Tactic:
by
  obtain hab | hba := le_or_gt a b
  · have := IsMarkovKernel.map (κ b) (piSingleton b).measurable
    rw [partialTraj_succ_eq_comp hab, map_comp, partialTraj_succ_self, ← map_comp_right,
      frestrictLe₂_comp_IicProdIoc, ← fst_eq, fst_prod, id_comp]
    all_goals fun_prop
  · rw [partialTraj_le (Nat.succ_le_of_lt hba), partialTraj_le hba.le, deterministic_map]
    · rfl
    · fun_prop

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

Goal state before:
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
⊢ ∫⁻ (x : γ) in s,
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x ∂(κ + η) a =
    ∫⁻ (x : γ) in s, 1 ∂(κ + η) a

Tactic:
by

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

Goal state before:
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
⊢ ∫⁻ (x : γ) in s, 1 ∂(κ + η) a = ((κ + η) a) s

Tactic:
by

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

Goal state before:
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
this : (η a) s = 0
⊢ ((κ + η) a) s = (κ a) s

Tactic:
by

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

Goal state before:
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
⊢ ((κ + η) a) s = (κ a) s

Tactic:
by

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

Goal state before:
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
⊢ ((κ.singularPart η) a) s = (κ a) s

Tactic:
by

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 : α
⊢ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
by

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

Goal state before:
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)ᶜ
⊢ η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)

Tactic:
by

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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
n : ℕ
⊢ Measurable ⇑(piCongrLeft (fun i ↦ X ↑i) (aux n))

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
x₀ : (i : ↥(Iic a)) → X ↑i
hbc : b ≤ c
⊢ Measurable (frestrictLe₂ hbc)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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
⊢ partialTraj κ b c ∘ₖ partialTraj κ a b = partialTraj κ a c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
⊢ ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hba : b ≤ a
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
⊢ lmarginalPartialTraj κ a b f = f

Tactic:
by

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

Goal state before:
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
x : γ
hx : x ∈ s
⊢ ¬1 = κ.rnDerivAux (κ + η) a x

Tactic:
exact (hs' x hx).ne'

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

Goal state before:
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)ᶜ
this :
  η.withDensity (κ.rnDeriv η) =
    ((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal).withDensity (κ.rnDeriv η)
hs' : ∀ x ∈ s, κ.rnDerivAux (κ + η) a x < 1
⊢ ∫⁻ (x : γ) in s,
      ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal *
        (ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) ∂(κ + η) a =
    ∫⁻ (x : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a x) ∂(κ + η) a

Tactic:
by

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

Goal state before:
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)ᶜ
⊢ ((η.withDensity (κ.rnDeriv η)) a) s = (κ a) s

Tactic:
by

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 : α
⊢ (κ.singularPart η) a ⟂ₘ η a

Tactic:
by

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
hm : MeasurableSet (κ.mutuallySingularSetSlice η a)
⊢ s ⊆ κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ

Tactic:
by

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

Goal state before:
pp: 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
l : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
hl : ∀ (k : ℕ) (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset x (Iic p) x₀) = ε
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → ((i : ↥(Iic k)) → X ↑i) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X ↑i),
    (∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) y)) →
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (χ n) (update (updateFinset x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction x₀ ind
k✝ k : ℕ
hn : p ≤ k
h : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (χ n) (updateFinset x (Iic k) (frestrictLe k z))
x : (i : ℕ) → X i
n : ℕ
h1 : k + 1 ≤ k + 1
⊢ ¬k + 1 ≤ p

Tactic:
by

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 η
⊢ η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ

Tactic:
by

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
⊢ lmarginalPartialTraj κ a b f x₀ =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X ↑i),
      f (updateFinset x₀ (Ioc a b) x) ∂((partialTraj κ a b).map (restrict₂ ⋯)) (frestrictLe a x₀)

Tactic:
by

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✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ

Tactic:
by

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✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (κ.singularPart η) a = 0 ↔ ((κ.singularPart η) a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
by

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 : α
⊢ univ = κ.mutuallySingularSetSlice η a ∪ (κ.mutuallySingularSetSlice η a)ᶜ

Tactic:
by

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 : α
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
by

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 : α
⊢ (κ.singularPart η) a = 0 ↔ κ a ≪ η a

Tactic:
by

Goal state after: