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

Goal state before:
pp: case hv.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
i j : ↥I
⊢ AEStronglyMeasurable (fun ω ↦ ω i) (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)

pp: case hv.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
i j : ↥I
⊢ AEStronglyMeasurable (fun ω ↦ ω j) (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)

pp: case hv.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
i j : ↥I
⊢ AEMeasurable (fun ω ↦ I.restrict fun x ↦ X x ω) P

Tactic:
any_goals exact Measurable.aestronglyMeasurable (by fun_prop)

Goal state after:
case hv.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : ℝ≥0 → Ω → ℝ
P : Measure Ω
h1 : IsGaussianProcess X P
h2 : ∀ (t : ℝ≥0), ∫ (x : Ω), X t x ∂P = 0
h3 : ∀ (s t : ℝ≥0), s ≤ t → cov[X s, X t; P] = ↑s
I : Finset ℝ≥0
this : IsGaussian (Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P)
x : WithLp 2 (↥I → ℝ)
i j : ↥I
⊢ AEMeasurable (fun ω ↦ I.restrict fun x ↦ X x ω) P
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a ↦ ↑(condCDF ρ a) ↑r) =ᵐ[ρ.fst] fun a ↦ (preCDF ρ r a).toReal

Tactic:
by
  simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]
  exact stieltjesOfMeasurableRat_ae_eq (isRatCondKernelCDF_preCDF ρ) () r

Goal state after:
Module: Mathlib.Probability.CDF

Goal state before:
pp: μ ν : Measure ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h : cdf μ = cdf ν
⊢ μ = ν

Tactic:
rw [← measure_cdf μ, ← measure_cdf ν, h]

Goal state after:
Module: Mathlib.Probability.Process.PartitionFiltration

Goal state before:
pp: α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet ((fun a ↦ ⟨memPartitionSet t n a, ⋯⟩) ⁻¹' {⟨s, hs⟩})

Tactic:
suffices MeasurableSet[partitionFiltration ht n] {x | memPartitionSet t n x = s} by
    convert! this
    ext x
    simp

Goal state after:
α : Type u_1
m✝ : MeasurableSpace α
t : ℕ → Set α
ht : ∀ (n : ℕ), MeasurableSet (t n)
n : ℕ
m : MeasurableSpace ↑(memPartition t n)
s : Set α
hs : s ∈ memPartition t n
⊢ MeasurableSet {x | memPartitionSet t n x = s}
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
h1 : Measurable fun p ↦ (κ p.1) (↑p.2 ×ˢ s) / (ν p.1) ↑p.2
⊢ Measurable ((fun p ↦ (κ p.1) (↑p.2 ×ˢ s) / (ν p.1) ↑p.2) ∘ fun p ↦ (p.1, ⟨countablePartitionSet n p.2, ⋯⟩))

Tactic:
refine h1.comp (measurable_fst.prodMk ?_)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
n : ℕ
s : Set β
hs : MeasurableSet s
h1 : Measurable fun p ↦ (κ p.1) (↑p.2 ×ˢ s) / (ν p.1) ↑p.2
⊢ Measurable fun p ↦ ⟨countablePartitionSet n p.2, ⋯⟩
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
this : ∀ᵐ (x : α) ∂ρ.fst, ∀ (s : Set ℝ), MeasurableSet s → (ρ'.condKernel x) s = (ρ.condKernel x) (f ⁻¹' s)
⊢ ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

Tactic:
filter_upwards [hρ'', this] with x hx h

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
this : ∀ᵐ (x : α) ∂ρ.fst, ∀ (s : Set ℝ), MeasurableSet s → (ρ'.condKernel x) s = (ρ.condKernel x) (f ⁻¹' s)
x : α
hx : (κ.map f) x = ρ'.condKernel x
h : ∀ (s : Set ℝ), MeasurableSet s → (ρ'.condKernel x) s = (ρ.condKernel x) (f ⁻¹' s)
⊢ κ x = ρ.condKernel x
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))
hab : a ≤ b
⊢ partialTraj κ a (b + 1) =
    (Kernel.id ×ₖ (κ b).map ⇑(piSingleton b) ∘ₖ partialTraj κ a b).map (_root_.IicProdIoc b (b + 1))

Tactic:
by
  rw [partialTraj, dif_neg (by lia)]
  induction b, hab using Nat.le_induction with
  | base => simp
  | succ k hak hk => rw [Nat.leRec_succ, ← partialTraj_le_def]; lia

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

Goal state before:
pp: case inl.base
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
⊢ IsSFiniteKernel (partialTraj κ a a)

Tactic:
rw [partialTraj_self]

Goal state after:
case inl.base
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a✝ b✝ c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
⊢ IsSFiniteKernel Kernel.id
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl.base
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 : ℕ
⊢ IsFiniteKernel (partialTraj κ a a)

Tactic:
rw [partialTraj_self]

Goal state after:
case inl.base
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 : ℕ
⊢ IsFiniteKernel Kernel.id
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl.base
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 : ℕ
⊢ IsZeroOrMarkovKernel (partialTraj κ a a)

Tactic:
rw [partialTraj_self]

Goal state after:
case inl.base
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 : ℕ
⊢ IsZeroOrMarkovKernel Kernel.id
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl.base
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 : ℕ
⊢ IsMarkovKernel (partialTraj κ a a)

Tactic:
rw [partialTraj_self]

Goal state after:
case inl.base
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 : ℕ
⊢ IsMarkovKernel Kernel.id
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measure.map (restrict₂ ⋯) (μ (J.sup id)) = Measure.map (restrict₂ hJI) (Measure.map (restrict₂ ⋯) (μ (I.sup id)))

Tactic:
Measure.map_map,

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measure.map (restrict₂ ⋯) (μ (J.sup id)) = Measure.map (restrict₂ hJI ∘ restrict₂ ⋯) (μ (I.sup id))

case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ hJI)

case hf
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] = Var[X; μ]

Tactic:
calc
    μ[Var[X; μ | m]] + Var[μ[X | m]; μ]
    _ = μ[(μ[X ^ 2 | m] - μ[X | m] ^ 2 : Ω → ℝ)] + (μ[μ[X | m] ^ 2] - μ[μ[X | m]] ^ 2) := by
      congr 1
      · exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX
      · exact variance_eq_sub (hX.condExp one_le_two)
    _ = μ[X ^ 2] - μ[μ[X | m] ^ 2] + (μ[μ[X | m] ^ 2] - μ[X] ^ 2) := by
      rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
      exact (hX.condExp one_le_two).integrable_sq
    _ = Var[X; μ] := by rw [variance_eq_sub hX]; ring

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ (partialTraj (fun n ↦ const ((i : ↥(Iic n)) → X ↑i) (μ (n + 1))) a b).map (restrict₂ ⋯) =
    const ((i : ↥(Iic a)) → X ↑i) (Measure.pi fun i ↦ μ ↑i)

Tactic:
· have : IsEmpty (Ioc a b) := by simpa [hba] using Subtype.isEmpty_false
    ext x s ms
    by_cases hs : s.Nonempty
    · rw [Subsingleton.eq_univ_of_nonempty hs, @measure_univ .., measure_univ]
      exact (IsMarkovKernel.map _ (measurable_restrict₂ _)) |>.isProbabilityMeasure x
    · rw [Set.not_nonempty_iff_eq_empty.1 hs]
      simp

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 I.restrict (infinitePiNat μ) = map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))

Tactic:
← restrict₂_comp_restrict I.subset_Iic_sup_id,

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ map (restrict₂ ⋯ ∘ (Iic (I.sup id)).restrict) (infinitePiNat μ) =
    map (restrict₂ ⋯) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) (Iic (I.sup id)))
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
⊢ (map (⇑(piCongrLeft X e)) (infinitePiNat fun n ↦ μ (e n))) (cylinder I S) = (piContent μ) (cylinder I S)

Tactic:
map_apply _ hS.cylinder,

Goal state after:
ι : 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
⊢ (infinitePiNat fun n ↦ μ (e n)) (⇑(piCongrLeft X e) ⁻¹' cylinder I S) = (piContent μ) (cylinder I S)

ι : 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)
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 η
h_le : κ ≤ κ + η
this :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) +
      (κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) =
    κ + η
a : α
s : Set γ
a✝ : MeasurableSet s
h :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) s +
      (((κ + η).withDensity fun a x ↦ ↑(κ.rnDerivAux (κ + η) a x).toNNReal) a) s =
    (κ a) s + (η a) s
⊢ (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) s = (η a) s

Tactic:
rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at h

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

Goal state before:
pp: case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a ⟂ₘ η a ∧ (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0

Tactic:
rw [← Measure.MutuallySingular.self_iff]

Goal state after:
case refine_2
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a ⟂ₘ η a ∧ (κ.singularPart η) a ⟂ₘ η a
⊢ (η.withDensity (κ.rnDeriv η)) a ⟂ₘ (η.withDensity (κ.rnDeriv η)) 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 : α
h_eq_add : η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
Kernel.ext_iff,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : ∀ (a : α), (η.withDensity (κ.rnDeriv η) + κ.singularPart η) a = κ a
⊢ (κ.singularPart η) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a) = 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✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : η.withDensity (κ.rnDeriv η) + κ.singularPart η = κ
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0

Tactic:
Kernel.ext_iff,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h_eq_add : ∀ (a : α), (η.withDensity (κ.rnDeriv η) + κ.singularPart η) a = κ a
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (κ a) (κ.mutuallySingularSetSlice η a)ᶜ = 0
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ deterministic f hf ∥ₖ deterministic f hf ∘ₖ copy α = copy β ∘ₖ deterministic f hf

Tactic:
parallelComp_comp_copy,

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β
hf : Measurable f
⊢ deterministic f hf ×ₖ deterministic f hf = copy β ∘ₖ deterministic f hf
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : ((κ ∥ₖ κ ∘ₖ copy α) a) (s ×ˢ s) = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ (κ a) s = 0 ∨ (κ a) s = 1

Tactic:
parallelComp_comp_copy,

Goal state after:
case mp
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
h : IsDeterministic κ
a : α
s : Set β
hs : MeasurableSet s
this : ((κ ×ₖ κ) a) (s ×ˢ s) = ((copy β ∘ₖ κ) a) (s ×ˢ s)
⊢ (κ a) s = 0 ∨ (κ a) s = 1
Module: Mathlib.Probability.Kernel.Deterministic

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a✝¹ : ∀ (a : α), IsZeroOneMeasure (κ a)
a✝ : α
⊢ (κ ∥ₖ κ ∘ₖ copy α) a✝ = (copy β ∘ₖ κ) a✝

Tactic:
parallelComp_comp_copy,

Goal state after:
case mpr
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
a✝¹ : ∀ (a : α), IsZeroOneMeasure (κ a)
a✝ : α
⊢ (κ ×ₖ κ) a✝ = (copy β ∘ₖ κ) a✝
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 b : ℕ
hab : a ≤ b
⊢ traj κ b ∘ₖ partialTraj κ a b = traj κ a

Tactic:
refine eq_traj _ _ fun n ↦ ?_

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 b : ℕ
hab : a ≤ b
n : ℕ
⊢ (traj κ b ∘ₖ partialTraj κ a b).map (frestrictLe n) = partialTraj κ a n
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n : ℕ
p : ↑I
⊢ Bin(n, p).real {0} = (1 - ↑p) ^ n

Tactic:
simp [binomial_real_singleton]

Goal state after:
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n : ℕ
p : ↑I
⊢ Bin(n, p).real {n} = ↑p ^ n

Tactic:
simp [binomial_real_singleton]

Goal state after:
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: p : ↑I
k✝ k : ℕ
⊢ Bin(1, p).real {k + 2} = Ber(1, 0, p).real {k + 2}

Tactic:
simp [binomial_real_singleton]

Goal state after:
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: R : Type u_1
inst✝² : MeasurableSpace R
inst✝¹ : AddMonoidWithOne R
inst✝ : MeasurableSingletonClass R
n : ℕ
p : ↑I
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.Iic n
⊢ ENNReal.ofReal (↑(n.choose x✝¹) * ↑p ^ x✝¹ * (1 - ↑p) ^ (n - x✝¹)) • map Nat.cast (dirac x✝¹) =
    ENNReal.ofReal (↑(n.choose x✝¹) * ↑p ^ x✝¹ * (1 - ↑p) ^ (n - x✝¹)) • dirac ↑x✝¹

Tactic:
map_dirac

Goal state after:
R : Type u_1
inst✝² : MeasurableSpace R
inst✝¹ : AddMonoidWithOne R
inst✝ : MeasurableSingletonClass R
n : ℕ
p : ↑I
x✝¹ : ℕ
x✝ : x✝¹ ∈ Finset.Iic n
⊢ ENNReal.ofReal (↑(n.choose x✝¹) * ↑p ^ x✝¹ * (1 - ↑p) ^ (n - x✝¹)) • dirac ↑x✝¹ =
    ENNReal.ofReal (↑(n.choose x✝¹) * ↑p ^ x✝¹ * (1 - ↑p) ^ (n - x✝¹)) • dirac ↑x✝¹
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
⊢ p.toOuterMeasure {a} = p a

Tactic:
refine (p.toOuterMeasure_apply {a}).trans ((tsum_eq_single a fun b hb => ?_).trans ?_)

Goal state after:
case refine_1
α : Type u_1
p : PMF α
a b : α
hb : b ≠ a
⊢ {a}.indicator (⇑p) b = 0

case refine_2
α : Type u_1
p : PMF α
a : α
⊢ {a}.indicator (⇑p) a = p a
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
a : α
inst✝ : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ (pure a).toMeasure s = (Measure.dirac a) s

Tactic:
by rw [toMeasure_pure_apply a s hs, Measure.dirac_apply' a hs]; rfl

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
b : Bool
⊢ b ∈ (bernoulli p h).support ↔ bif b then p ≠ 0 else p ≠ 1

Tactic:
by
  simp [support_bernoulli]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ (μ.trim hm ⊗ₘ condExpKernel μ m).snd = μ

Tactic:
compProd_trim_condExpKernel

Goal state after:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ (Measure.map Function.diag μ).snd = μ
Module: Mathlib.Probability.Kernel.Category.Stoch

Goal state before:
pp: X Y : Stoch
κ✝ : X ⟶ Y
X✝ Y✝ : Stoch
κ : X✝ ⟶ Y✝
⊢ κ ≫ ε = ε

Tactic:
by ext : 2; simp

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ s_1 ∈ {s}, MeasurableSet s_1

Tactic:
intro s' hs'
    rw [Set.mem_singleton_iff] at hs'
    rwa [hs']

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ s ∈ {t}, MeasurableSet s

Tactic:
intro s' hs'
    rw [Set.mem_singleton_iff] at hs'
    rwa [hs']

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']

Tactic:
classical
    let g := fun i ↦ if hi : i ∈ s then (h_sets i hi).choose else Set.univ
    specialize h s (sets := g) (fun i hi ↦ ?_)
    · simp only [g, dif_pos hi]
      exact (h_sets i hi).choose_spec.1
    · have hg : ∀ i ∈ s, sets i = f i ⁻¹' g i := by
        intro i hi
        rw [(h_sets i hi).choose_spec.2.symm]
        simp only [g, dif_pos hi]
      convert! h with i hi i hi <;> exact hg i hi

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e'_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ Measure.map (Prod.map id fun ω ↦ (f ω, g ω)) (μ.trim hm' ⊗ₘ condExpKernel μ m') =
    Measure.map (fun ω ↦ (ω, f ω, g ω)) μ

Tactic:
compProd_trim_condExpKernel

Goal state after:
case e'_2
Ω : Type u_1
β : Type u_3
β' : Type u_4
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
hf : Measurable f
hg : Measurable g
⊢ Measure.map (Prod.map id fun ω ↦ (f ω, g ω)) (Measure.map Function.diag μ) = Measure.map (fun ω ↦ (ω, f ω, g ω)) μ