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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ AEStronglyMeasurable (fun x' ↦ ∫ (y : Ω), f (x', y) ∂(condDistrib Y X μ) x') (Measure.map X (μ.restrict (X ⁻¹' t)))

Tactic:
rw [← Measure.restrict_map hX ht]
      exact (hf_int.1.integral_condDistrib_map hY).restrict

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

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsFiniteKernel (partialTraj κ a b)

Tactic:
· rw [partialTraj_le hba]; infer_instance

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

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsZeroOrMarkovKernel (partialTraj κ a b)

Tactic:
· rw [partialTraj_le hba]; infer_instance

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

Goal state before:
pp: case inr
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)
a b : ℕ
hba : b ≤ a
⊢ IsMarkovKernel (partialTraj κ a b)

Tactic:
· rw [partialTraj_le hba]; infer_instance

Goal state after:
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: V : Type u_1
p : ↑I
inst✝ : Finite V
G : SimpleGraph V
⊢ G(V, p) {G} = ↑(toNNReal p) ^ G.edgeSet.ncard * ↑(toNNReal (σ p)) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)

Tactic:
cases nonempty_fintype V

Goal state after:
case intro
V : Type u_1
p : ↑I
inst✝ : Finite V
G : SimpleGraph V
val✝ : Fintype V
⊢ G(V, p) {G} = ↑(toNNReal p) ^ G.edgeSet.ncard * ↑(toNNReal (σ p)) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2

Tactic:
have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
⊢ μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (μ[X | m] ^ 2) μ
ω : Ω
hω₀ : μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 - 2 * X * μ[X | m] | m] + μ[μ[X | m] ^ 2 | m]) ω
hω₁ : μ[X ^ 2 - 2 * X * μ[X | m] | m] ω = (μ[X ^ 2 | m] - μ[2 * X * μ[X | m] | m]) ω
⊢ μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω →
    μ[OfNat.ofNat 2 * X | m] ω = (OfNat.ofNat 2 * μ[X | m]) ω →
      μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2) ω

Tactic:
hω₂

Goal state after:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (X ^ 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (μ[X | m] ^ 2) μ
ω : Ω
hω₀ : μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 - 2 * X * μ[X | m] | m] + μ[μ[X | m] ^ 2 | m]) ω
hω₁ : μ[X ^ 2 - 2 * X * μ[X | m] | m] ω = (μ[X ^ 2 | m] - μ[2 * X * μ[X | m] | m]) ω
hω₂ : μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω
⊢ μ[OfNat.ofNat 2 * X | m] ω = (OfNat.ofNat 2 * μ[X | m]) ω →
    μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] ω = (μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2) ω
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : β), g b ∂(κ.withDensity f) a = ∫⁻ (b : β), f a b * g b ∂κ a

Tactic:
rw [Kernel.withDensity_apply _ hf,
    lintegral_withDensity_eq_lintegral_mul _ (Measurable.of_uncurry_left hf) hg]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a_1 : β), (f a * g) a_1 ∂κ a = ∫⁻ (b : β), f a b * g b ∂κ a
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
⊢ ∫⁻ (b : γ) in s, ↑(κ.rnDerivAux (κ + η) a b).toNNReal ∂(κ + η) a = (κ a) s

Tactic:
simp_rw [ofNNReal_toNNReal]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (b : γ) in s, ENNReal.ofReal (κ.rnDerivAux (κ + η) a b) ∂(κ + η) a = (κ a) s
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 fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) {x | 1 ≤ κ.rnDerivAux (κ + η) a x} = 0

Tactic:
simp_rw [ofNNReal_toNNReal]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (((κ + η).withDensity fun a x ↦ ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) a x)) a) {x | 1 ≤ κ.rnDerivAux (κ + η) a x} =
    0
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))
x y : (i : ℕ) → X i
⊢ l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) x₀)

Tactic:
have := hl p (updateFinset x _ x₀)

Goal state after:
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))
x y : (i : ℕ) → X i
this :
  Tendsto (fun n ↦ lmarginalPartialTraj κ p (a n) (χ n) (updateFinset x (Iic p) x₀)) atTop
    (𝓝 (l p (updateFinset x (Iic p) x₀)))
⊢ l p (updateFinset x (Iic p) x₀) = l p (updateFinset y (Iic p) 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 : γ) ∂(κ + η) a,
    x ∈ (κ.mutuallySingularSetSlice η a)ᶜ →
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 0 x

Tactic:
simp_rw [ofNNReal_toNNReal]

Goal state after:
α : 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
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 | ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x = 0 x}

Tactic:
simp_rw [ofNNReal_toNNReal]

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 ↦ ↑(κ.rnDerivAux (κ + η) a b).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a b).toNNReal * κ.rnDeriv η a b

Tactic:
simp_rw [ofNNReal_toNNReal]

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 ↦
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x)

Tactic:
simp_rw [ofNNReal_toNNReal]

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.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
⊢ Measurable fun a ↦ (κ a).singularPart (η a)

Tactic:
refine Measure.measurable_of_measurable_coe _ (fun s hs ↦ ?_)

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
s : Set γ
hs : MeasurableSet s
⊢ Measurable fun b ↦ ((κ b).singularPart (η b)) s
Module: Mathlib.Probability.Kernel.Composition.AbsolutelyContinuous

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 : ∀ (a : α), (η a) (Prod.mk a ⁻¹' s) = 0
a : α
ha : κ a ⟂ₘ η a
⊢ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
← Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero κ η a,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
inst✝² : IsFiniteKernel κ
inst✝¹ : IsFiniteKernel η
inst✝ : MeasurableSpace.CountableOrCountablyGenerated α β
μ ν : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ⟂ₘ η a
hμ : SFinite μ
hν : SFinite ν
s : Set (α × β) := κ.mutuallySingularSet η
hs : MeasurableSet s
h_eq : ∀ (a : α), Prod.mk a ⁻¹' s = κ.mutuallySingularSetSlice η a
h1 : ∀ (a : α), (η a) (Prod.mk a ⁻¹' s) = 0
a : α
ha : κ a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0
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 : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
⊢ ∃ N S, MeasurableSet S ∧ t = cylinder (Iic N) S

Tactic:
by
      simpa [measurableCylinders_nat] using ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
⊢ ∫⁻ (a : β) in t, (η a) s ∂κ a = ((η ∘ₖ κ) a) s * (κ a) t

Tactic:
rcases ((η ∘ₖ κ) a).zero_one s with (h₀ | h₁)

Goal state after:
case inl
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₀ : ((η ∘ₖ κ) a) s = 0
⊢ ∫⁻ (a : β) in t, (η a) s ∂κ a = ((η ∘ₖ κ) a) s * (κ a) t

case inr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
a : α
s : Set γ
t : Set β
hs : MeasurableSet s
ht : MeasurableSet t
this : ∀ (b : β), (η b) s * t.indicator 1 b = t.indicator (fun b ↦ (η b) s) b
h₁ : ((η ∘ₖ κ) a) s = 1
⊢ ∫⁻ (a : β) in t, (η a) s ∂κ a = ((η ∘ₖ κ) a) s * (κ a) t
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.deterministic f hf ∥ₖ (Kernel.deterministic f hf ∘ₖ Kernel.id)) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ =
    ⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ

Tactic:
Kernel.comp_id

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ =
    ⇑(Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ ⇑(Kernel.copy Ω) ∘ₘ μ
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_3
inst✝³ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
inst✝² : IsMarkovKernel κ
inst✝¹ : IsMarkovKernel η
inst✝ : IsDeterministic (η ∘ₖ κ)
⊢ η ∘ₖ κ ∥ₖ κ ∘ₖ copy α = η ∥ₖ Kernel.id ∘ₖ copy β ∘ₖ κ

Tactic:
by
  simp only [parallelComp_comp_copy]
  ext a : 1
  rw [prod_apply]
  refine Measure.prod_eq fun s t hs ht ↦ ?_
  rw [comp_apply' _ _ _ (hs.prod ht)]
  simp_rw [prod_apply_prod, Kernel.id_apply, Measure.dirac_apply' _ ht]
  have (b : β) : (η b) s * t.indicator 1 b = t.indicator (fun b ↦ η b s) b := by
    simp only [indicator]
    split_ifs
    all_goals simp_all
  simp_rw [this]
  rw [lintegral_indicator ht]
  rcases ((η ∘ₖ κ) a).zero_one s with (h₀ | h₁)
  · rw [h₀, zero_mul, setLIntegral_eq_zero_iff ht <| η.measurable_coe hs]
    rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff <| η.measurable_coe hs] at h₀
    filter_upwards [h₀] with x hx _ using hx
  · /- In Example 11.25 of [gritz2020], the case where `((η ∘ₖ κ) a) s = 1` is not explicitly
    treated. We prove it here by using the fact that the hypothesis implies that
    `((η ∘ₖ κ) a) sᶜ = 0`, and thus that the integral of `1 - (η b) s` over `κ a` is zero. -/
    rw [h₁, one_mul]
    have integral_le_kernel : ∫⁻ b in t, (η b) s ∂κ a ≤ κ a t := by
      calc
      _ ≤ ∫⁻ a in t, 1 ∂κ a := by
        refine lintegral_mono ?_
        intro b
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)
      _ = κ a t := by rw [setLIntegral_one]
    refine le_antisymm integral_le_kernel <| tsub_eq_zero_iff_le.mp ?_
    rw [← nonpos_iff_eq_zero]
    calc
    _ = ∫⁻ b in t, 1 ∂κ a - ∫⁻ b in t, (η b) s ∂κ a := by
      rw [setLIntegral_one]
    _ = ∫⁻ b in t, 1 - (η b) s ∂κ a := by
      rw [lintegral_sub]
      · exact η.measurable_coe hs
      · exact ne_top_of_le_ne_top (by simp) integral_le_kernel
      · refine ae_of_all _ fun b ↦ ?_
        rw [← measure_univ (μ := η b)]
        exact measure_mono (by simp)
    _ ≤ ∫⁻ b, 1 - (η b) s ∂κ a := setLIntegral_le_lintegral _ _
    _ = ∫⁻ x, (η x) sᶜ ∂κ a := by
        congr with x
        rw [measure_compl hs (by simp)]
        simp
    _ = (η ∘ₖ κ) a sᶜ := by
        rw [η.comp_apply' _ _ hs.compl]
    _ = 0 := by
      rw [measure_compl hs (by simp), measure_univ h₁, h₁, tsub_self]

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
hl : Measurable (uncurry ℓ)
P : Kernel Θ 𝓧
π : Measure Θ
⊢ bayesRisk ℓ P π ≤ ⨅ y, ∫⁻ (θ : Θ), ℓ θ y * (P θ) Set.univ ∂π

Tactic:
by
  simp_rw [le_iInf_iff, bayesRisk]
  refine fun y ↦ iInf_le_of_le (Kernel.const _ (Measure.dirac y)) ?_
  simp only [iInf_pos, avgRisk_const_right', mul_comm]
  gcongr with θ
  rw [lintegral_dirac' _ (by fun_prop)]

Goal state after:
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ⇑(P†π ×ₖ (κ ∘ₖ Kernel.id)) ∘ₘ ⇑P ∘ₘ π = ⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π

Tactic:
Kernel.comp_id

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ ⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π = ⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π
Module: Mathlib.Probability.Decision.Risk.Countable

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Countable Θ
inst✝ : MeasurableSingletonClass Θ
⊢ avgRisk ℓ P κ π = ∑' (θ : Θ), (∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P) θ) * π {θ}

Tactic:
simp [avgRisk, lintegral_countable']

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

Goal state before:
pp: case e_f.hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

pp: case e_f.hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X ↑i
⊢ MeasurableSet (Prod.mk x ⁻¹' s)

Tactic:
all_goals exact ms.preimage (by fun_prop)

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : MeasurableSpace α
p : PMF α
inst✝ : MeasurableSingletonClass α
s : Set α
⊢ p.toMeasure s = p.toOuterMeasure s

Tactic:
have hs := (p.support_countable.mono s.inter_subset_right).measurableSet

Goal state after:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : PMF α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : MeasurableSet (s ∩ p.support)
⊢ p.toMeasure s = p.toOuterMeasure s
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hXmeas : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
⊢ ∫ (ω : Ω), 1 - X ω ∂μ = μ.real {ω | X ω = 0}

Tactic:
by
  calc
    _ = μ.real {ω | 1 - X ω = 1} :=
      integral_of_ae_eq_zero_or_one (aemeasurable_const (b := 1).sub hXmeas)
        (by simpa [sub_eq_zero, or_comm, eq_comm (a := (1 : ℝ))] using hX)
    _ = μ.real {ω | X ω = 0} := by simp

Goal state after: