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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ Tendsto (fun i ↦ ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 (∫ (a : β), 1 ∂ν a))

Tactic:
rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → ℚ
hseq : Monotone seq
hseq_tendsto : Tendsto seq atTop atTop
⊢ Tendsto (fun i ↦ ∫ (a_1 : β), f (a, a_1) (seq i) ∂ν a) atTop (𝓝 ((ν a).real univ))
Module: Mathlib.Probability.CDF

Goal state before:
pp: f : StieltjesFunction ℝ
hf0 : Tendsto (↑f) atBot (𝓝 0)
hf1 : Tendsto (↑f) atTop (𝓝 1)
⊢ cdf f.measure = f

Tactic:
refine (cdf f.measure).eq_of_measure_of_tendsto_atBot f ?_ (tendsto_cdf_atBot _) hf0
  have h_prob : IsProbabilityMeasure f.measure :=
    ⟨by rw [f.measure_univ hf0 hf1, sub_zero, ENNReal.ofReal_one]⟩
  exact measure_cdf f.measure

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case convert_6
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ ∫ (x : Ω), (X 0 x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P] ∂P = 0

Tactic:
integral_div,

Goal state after:
case convert_6
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ (∫ (a : Ω), X 0 a - ∫ (x : Ω), X 0 x ∂P ∂P) / √Var[X 0; P] = 0
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
⊢ ↑s * (↑t * ↑(min (1 / s) (1 / t))) = ↑s

Tactic:
obtain rfl | hs := eq_or_ne s 0

Goal state after:
case refine_3.inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t : ℝ≥0
this : IsProbabilityMeasure P
hst : 0 ≤ t
⊢ ↑0 * (↑t * ↑(min (1 / 0) (1 / t))) = ↑0

case refine_3.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
s t : ℝ≥0
hst : s ≤ t
this : IsProbabilityMeasure P
hs : s ≠ 0
⊢ ↑s * (↑t * ↑(min (1 / s) (1 / t))) = ↑s
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: case convert_7
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ ∫ (x : Ω), (X 0 x - ∫ (x : Ω), X 0 x ∂P) ^ 2 / √Var[X 0; P] ^ 2 ∂P = 1

Tactic:
integral_div,

Goal state after:
case convert_7
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst✝¹ : IsProbabilityMeasure P
inst✝ : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 1) P'
hX : Var[X 0; P] ≠ 0
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
mX0 : AEMeasurable (X 0) P
intX0 : Integrable (X 0) P
this :
  ∀ (n : ℕ) (ω : Ω),
    (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P) =
      (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]
⊢ (∫ (a : Ω), (X 0 a - ∫ (x : Ω), X 0 x ∂P) ^ 2 ∂P) / √Var[X 0; P] ^ 2 = 1
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.swap β α) ∘ₘ ν.prod μ = ⇑(Kernel.swap β γ) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ

Tactic:
Measure.comp_assoc,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) ∘ₘ ν.prod μ = ⇑(Kernel.swap β γ) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) ∘ₘ ν.prod μ = ⇑(Kernel.swap β γ) ∘ₘ ⇑(Kernel.id ∥ₖ κ) ∘ₘ ν.prod μ

Tactic:
Measure.comp_assoc,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝² : SFinite μ
inst✝¹ : SFinite ν
κ : Kernel α γ
inst✝ : IsSFiniteKernel κ
h1 : (⇑κ ∘ₘ μ).prod ν = map Prod.swap (ν.prod (⇑κ ∘ₘ μ))
⊢ ⇑(κ ∥ₖ Kernel.id ∘ₖ Kernel.swap β α) ∘ₘ ν.prod μ = ⇑(Kernel.swap β γ ∘ₖ (Kernel.id ∥ₖ κ)) ∘ₘ ν.prod μ
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (fun ω ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[⇑L₁ ∘ X, ⇑L₂ ∘ Y; P] = 0
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this : (⇑L ∘ fun ω ↦ (X ω, Y ω)) = ⇑(L ∘SL inl ℝ E F) ∘ X + ⇑(L ∘SL inr ℝ E F) ∘ Y
⊢ cexp (↑(∫ (x : Ω), (⇑L ∘ fun ω ↦ (X ω, Y ω)) x ∂P) * I - ↑Var[⇑L ∘ fun ω ↦ (X ω, Y ω); P] / 2) =
    charFunDual (Measure.map X P) (L ∘SL inl ℝ E F) * charFunDual (Measure.map Y P) (L ∘SL inr ℝ E F)

Tactic:
hXY.fst.charFunDual_map_eq,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hXY : HasGaussianLaw (fun ω ↦ (X ω, Y ω)) P
h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), cov[⇑L₁ ∘ X, ⇑L₂ ∘ Y; P] = 0
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this : (⇑L ∘ fun ω ↦ (X ω, Y ω)) = ⇑(L ∘SL inl ℝ E F) ∘ X + ⇑(L ∘SL inr ℝ E F) ∘ Y
⊢ cexp (↑(∫ (x : Ω), (⇑L ∘ fun ω ↦ (X ω, Y ω)) x ∂P) * I - ↑Var[⇑L ∘ fun ω ↦ (X ω, Y ω); P] / 2) =
    cexp (↑(∫ (x : Ω), (⇑(L ∘SL inl ℝ E F) ∘ X) x ∂P) * I - ↑Var[⇑(L ∘SL inl ℝ E F) ∘ X; P] / 2) *
      charFunDual (Measure.map Y P) (L ∘SL inr ℝ E F)
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η) ∘ₘ ⇑(Kernel.id ×ₖ κ) ∘ₘ μ = ⇑(Kernel.id ×ₖ (η ∘ₖ κ)) ∘ₘ μ

Tactic:
Measure.comp_assoc,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel β γ
inst✝ : IsSFiniteKernel η
hμ : SFinite μ
⊢ ⇑(Kernel.id ∥ₖ η ∘ₖ (Kernel.id ×ₖ κ)) ∘ₘ μ = ⇑(Kernel.id ×ₖ (η ∘ₖ κ)) ∘ₘ μ
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hn
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
h_disj : Pairwise (Disjoint on fun i ↦ ↑i)
u v : ↑↑S
huv : u ≠ v
⊢ Disjoint ↑u ↑v ∨ s = ⊥

Tactic:
exact Or.inl (h_disj huv)

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ ‖∫ (y : Ω), f (x, y) ∂ρ.condKernel x‖ ≤ ‖∫ (y : Ω), ‖f (x, y)‖ ∂ρ.condKernel x‖

Tactic:
refine (norm_integral_le_integral_norm _).trans_eq (Real.norm_of_nonneg ?_).symm

Goal state after:
α : Type u_1
Ω : Type u_2
E : Type u_3
mα : MeasurableSpace α
inst✝⁵ : MeasurableSpace Ω
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
ρ : Measure (α × Ω)
inst✝ : IsFiniteMeasure ρ
f : α × Ω → E
hf_int : Integrable f ρ
x : α
⊢ 0 ≤ ∫ (a : Ω), ‖f (x, a)‖ ∂ρ.condKernel x
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: case hc
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a✝ : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae : ∀ᵐ (t : β) ∂κ.fst a✝, (a✝, t) ∈ {p | (η p) (range e)ᶜ = 0}
a : β
ha : (η (a✝, a)) (range e)ᶜ = 0
⊢ (a✝, a) ∈ (fun a ↦ (η a) (range (embeddingReal Ω))ᶜ) ⁻¹' {0}

Tactic:
exact ha

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
| (ρ a) s

Tactic:
rw [← hκ]

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
s : Set (β × Ω)
hs : MeasurableSet s
| ((ρ.fst ⊗ₖ κ) a) 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 α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m ↦ ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 ((κ a).real univ))

Tactic:
simp_rw [integral_density hκν a (hseq_meas _)]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m ↦ (κ a).real (univ ×ˢ seq m)) atTop (𝓝 ((κ a).real univ))
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 α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m ↦ ∫ (x : γ), κ.density ν a x (seq m) ∂ν a) atTop (𝓝 0)

Tactic:
simp_rw [integral_density hκν a (hseq_meas _)]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
⊢ Tendsto (fun m ↦ (κ a).real (univ ×ˢ seq m)) atTop (𝓝 0)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}).toReal = 1

Tactic:
have : countablePartitionSet n x ×ˢ univ = {p : γ × β | p.1 ∈ countablePartitionSet n x} := by
      ext x
      simp

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
x : γ
h : ¬(κ.fst a) (countablePartitionSet n x) = 0
this : countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}
⊢ ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}).toReal = 1
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.1.1 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩

Tactic:
try rfl

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

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ↑i ≤ k
h✝ : ¬↑i ≤ a
⊢ x.1.2 ⟨↑i, ⋯⟩ = (prodAssoc x).2.1 ⟨↑i, ⋯⟩

Tactic:
try rfl

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ¬↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩

Tactic:
try rfl

Goal state after:
case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ¬↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ¬↑i ≤ k
h✝ : ¬↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).2.2 ⟨↑i, ⋯⟩

Tactic:
try rfl

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 (∫ (a : γ), 1 ∂κ.fst a))

Tactic:
rw [MeasureTheory.integral_const, smul_eq_mul, mul_one]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 ((κ.fst a).real univ))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
⊢ IsProjectiveLimit ν μ ↔ ∀ (n : ℕ), Measure.map (frestrictLe n) ν = μ (Iic n)

Tactic:
isProjectiveLimit_nat_iff' hμ _ 0

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
⊢ (∀ ⦃n : ℕ⦄, 0 ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)) ↔ ∀ (n : ℕ), Measure.map (frestrictLe n) ν = μ (Iic n)
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
hX : AEMeasurable X μ
⊢ Var[X; μ | ⊥] = fun _ω ↦ Var[X; μ]

Tactic:
by
  simp [condVar_bot', average_eq_integral, variance_eq_integral hX]

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
f_eq : ∀ (x : (n : ℕ) → X n) (n : ℕ), lmarginalPartialTraj κ k (a n) (f n) x = lmarginalPartialTraj κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (f n) x) atTop (𝓝 (lmarginalPartialTraj κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj κ k (k + 1) l (updateFinset x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (updateFinset x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this : ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (f n) (update (updateFinset x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ ↑(Iic (k + 1))
h1 : i = k + 1
⊢ ⋯ ▸ x = ⋯ ▸ x

Tactic:
try rfl

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
f_eq : ∀ (x : (n : ℕ) → X n) (n : ℕ), lmarginalPartialTraj κ k (a n) (f n) x = lmarginalPartialTraj κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (f n) x) atTop (𝓝 (lmarginalPartialTraj κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj κ k (k + 1) l (updateFinset x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (updateFinset x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this : ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (f n) (update (updateFinset x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ ↑(Iic (k + 1))
h1 : ¬i = k + 1
h2 : i ≤ k
⊢ y ⟨i, ⋯⟩ = y ⟨i, ⋯⟩

Tactic:
try rfl

Goal state after: