mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ cexp (↑(∫ (ω : Ω), L fun i ↦ X i ω ∂P) * I - ↑Var[fun ω ↦ L fun i ↦ X i ω; P] / 2) =
    cexp
      ((∑ i, ↑(∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)) * I -
        ∑ x, ↑Var[fun ω ↦ (L ∘SL single ℝ E x) (X x ω); P] / 2)

Tactic:
this

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ cexp
      (↑(∫ (ω : Ω), ∑ i, (L ∘SL single ℝ E i) (X i ω) ∂P) * I -
        ↑Var[fun ω ↦ ∑ i, (L ∘SL single ℝ E i) (X i ω); P] / 2) =
    cexp
      ((∑ i, ↑(∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)) * I -
        ∑ x, ↑Var[fun ω ↦ (L ∘SL single ℝ E x) (X x ω); P] / 2)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ Integrable (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) (ν a)

Tactic:
this

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
this :
  (fun b ↦ ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x) = fun b ↦
    (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal
⊢ Integrable (fun b ↦ (ENNReal.ofReal (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x)).toReal) (ν a)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_a.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ ↑(∫ (ω : Ω), ∑ i, (L ∘SL single ℝ E i) (X i ω) ∂P) = ∑ i, ↑(∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)

Tactic:
[

Goal state after:
case e_a.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Finite ι
E : ι → Type u_3
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : (i : ι) → MeasurableSpace (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
X : (i : ι) → Ω → E i
hX : HasGaussianLaw (fun ω i ↦ X i ω) P
h :
  ∀ (i j : ι),
    i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), cov[fun x ↦ L₁ (X i x), fun x ↦ L₂ (X j x); P] = 0
this✝¹ : IsProbabilityMeasure P
this✝ : Fintype ι := Fintype.ofFinite ι
L : StrongDual ℝ ((x : ι) → E x)
this : ∀ (ω : Ω), (L fun x ↦ X x ω) = ∑ i, (L ∘SL single ℝ E i) (X i ω)
⊢ ↑(∫ (ω : Ω), ∑ i, (L ∘SL single ℝ E i) (X i ω) ∂P) = ∑ i, ↑(∫ (ω : Ω), (L ∘SL single ℝ E i) (X i ω) ∂P)
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Monotone fun r ↦ preCDF ρ r a

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Monotone fun r ↦ preCDF ρ r a
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (c : β) ∂ν a, ∀ ⦃a_1 b : ℚ⦄, a_1 ≤ b → f (a, c) a_1 ≤ f (a, c) b

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
⊢ ∀ᵐ (c : β) ∂ν a, ∀ ⦃a_1 b : ℚ⦄, a_1 ≤ b → f (a, c) a_1 ≤ f (a, c) b
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ‖(preCDF ρ x x_1).toReal‖ₑ ∂ρ.fst ≤ ρ.fst univ

Tactic:
[

Goal state after:
case refine_2
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
x : ℚ
t : Set α
x✝¹ : MeasurableSet t
x✝ : ρ.fst t ≠ ∞
⊢ ∫⁻ (x_1 : α) in t, ‖(preCDF ρ x x_1).toReal‖ₑ ∂ρ.fst ≤ ρ.fst univ
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝ : IsProbabilityMeasure P
this : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
⊢ iIndepFun (fun i ω j ↦ X i j ω) P

Tactic:
this

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝ : IsProbabilityMeasure P
this : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
⊢ iIndepFun (fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω) P
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) c).toReal ∂(Kernel.const Unit ρ.fst) a) atTop (𝓝 0)

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) c).toReal ∂(Kernel.const Unit ρ.fst) a) atTop (𝓝 0)
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
this : ∀ (t : ℝ≥0) (ω : Ω), (√↑c)⁻¹ * B (c * t) ω = (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ * B (c * t) ω) P

Tactic:
[

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
this : ∀ (t : ℝ≥0) (ω : Ω), (√↑c)⁻¹ * B (c * t) ω = (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ * B (c * t) ω) P
Module: Mathlib.Probability.BrownianMotion.Basic

Goal state before:
pp: case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
this : ∀ (t : ℝ≥0) (ω : Ω), (√↑c)⁻¹ * B (c * t) ω = (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ * B (c * t) ω) P

Tactic:
this

Goal state after:
case refine_1
Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
this : ∀ (t : ℝ≥0) (ω : Ω), (√↑c)⁻¹ * B (c * t) ω = (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω
⊢ IsGaussianProcess (fun t ω ↦ (√↑c)⁻¹ • (B ∘ fun x ↦ c * x) t ω) P
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) c).toReal ∂(Kernel.const Unit ρ.fst) a) atTop
    (𝓝 (((Kernel.const Unit ρ.fst) a).real univ))

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
x✝ : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun m ↦ ∫ (c : α), (preCDF ρ (s m) c).toReal ∂(Kernel.const Unit ρ.fst) a) atTop
    (𝓝 (((Kernel.const Unit ρ.fst) a).real univ))
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (fun p ↦ condCDF ρ p.2) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (fun p ↦ condCDF ρ p.2) (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)
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:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a ↦ ↑(condCDF ρ a) ↑r) =ᵐ[ρ.fst] fun a ↦ (preCDF ρ r a).toReal
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ s ∈ range Iic, Measurable fun a ↦ (condCDF ρ a).measure s

Tactic:
[

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ s ∈ range Iic, Measurable fun a ↦ (condCDF ρ a).measure s
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝² : IsProbabilityMeasure P
this✝¹ : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
this✝ : (i : ι) → Fintype (κ i) := fun i ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 (κ i → ℝ)
y : WithLp 2 (κ j → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ x_1, ((EuclideanSpace.basisFun (κ i) ℝ).repr x).ofLp x_1 • (EuclideanSpace.basisFun (κ i) ℝ) x_1,
        (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫,
      fun ω ↦
      ⟪∑ x, ((EuclideanSpace.basisFun (κ j) ℝ).repr y).ofLp x • (EuclideanSpace.basisFun (κ j) ℝ) x,
        (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫;
      P] =
    0

Tactic:
[

Goal state after:
case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝¹ : Finite ι
κ : ι → Type u_4
inst✝ : ∀ (i : ι), Finite (κ i)
X : (i : ι) → κ i → Ω → ℝ
hX : HasGaussianLaw (fun ω i j ↦ X i j ω) P
h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), cov[X i k, X j l; P] = 0
this✝² : IsProbabilityMeasure P
this✝¹ : (fun i ω j ↦ X i j ω) = fun i ↦ ofLp ∘ toLp 2 ∘ fun ω j ↦ X i j ω
this✝ : (i : ι) → Fintype (κ i) := fun i ↦ Fintype.ofFinite (κ i)
this : Fintype ι := Fintype.ofFinite ι
i j : ι
hij : i ≠ j
x : WithLp 2 (κ i → ℝ)
y : WithLp 2 (κ j → ℝ)
⊢ cov[fun ω ↦
      ⟪∑ x_1, ((EuclideanSpace.basisFun (κ i) ℝ).repr x).ofLp x_1 • (EuclideanSpace.basisFun (κ i) ℝ) x_1,
        (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫,
      fun ω ↦
      ⟪∑ x, ((EuclideanSpace.basisFun (κ j) ℝ).repr y).ofLp x • (EuclideanSpace.basisFun (κ j) ℝ) x,
        (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫;
      P] =
    0
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : 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]
⊢ TendstoInDistribution (fun n ω ↦ (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P))
    atTop Y (fun x ↦ P) P'

Tactic:
[

Goal state after:
Ω : 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]
⊢ TendstoInDistribution (fun n ω ↦ (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P))
    atTop Y (fun x ↦ P) P'
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : 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]
⊢ TendstoInDistribution (fun n ω ↦ (√(↑n * Var[X 0; P]))⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P))
    atTop Y (fun x ↦ P) P'

Tactic:
this

Goal state after:
Ω : 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]
⊢ TendstoInDistribution (fun n ω ↦ (√↑n)⁻¹ * ∑ k ∈ Finset.range n, (X k ω - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]) atTop Y
    (fun x ↦ P) P'
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic x) ∂ν a = (κ a) (s ×ˢ Iic x)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic x) ∂ν a = (κ a) (s ×ˢ Iic x)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y ↦ x ⊆ y) fun q ↦ Iic ↑q
h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q ↦ s ×ˢ Iic ↑q
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑i)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y ↦ x ⊆ y) fun q ↦ Iic ↑q
h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q ↦ s ×ˢ Iic ↑q
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ r, Iic ↑r) ∂ν a = (κ a) (⋃ i, s ×ˢ Iic ↑i)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y ↦ x ⊆ y) fun q ↦ Iic ↑q
h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q ↦ s ×ˢ Iic ↑q
⊢ ⨆ b, ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, a_1)) (Iic ↑b) ∂ν a = ⨆ i, (κ a) (s ×ˢ Iic ↑i)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y ↦ x ⊆ y) fun q ↦ Iic ↑q
h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q ↦ s ×ˢ Iic ↑q
⊢ ⨆ b, ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, a_1)) (Iic ↑b) ∂ν a = ⨆ i, (κ a) (s ×ˢ Iic ↑i)
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 ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (⇑κ ∘ₘ ν) (Prod.mk x ⁻¹' s) ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (⇑κ ∘ₘ ν) (Prod.mk x ⁻¹' s) ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (⋃ i, f i) ∂ν a = (κ a) (s ×ˢ ⋃ i, f i)

Tactic:
[

Goal state after:
case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (⋃ i, f i) ∂ν a = (κ a) (s ×ˢ ⋃ i, f i)
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρCond : Kernel α Ω
inst✝² : MeasurableSingletonClass α
x : α
s : Set Ω
hs : MeasurableSet s
inst✝¹ : IsCondKernel 0 ρCond
inst✝ : IsFiniteMeasure 0
hx : (fst 0) {x} ≠ 0
⊢ False

Tactic:
simp at hx

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

Goal state before:
pp: case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∑' (i : ℕ), ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, a_1)) (f i) ∂ν a = ∑' (i : ℕ), (κ a) (s ×ˢ f i)

Tactic:
[

Goal state after:
case iUnion
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f✝ : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f✝ κ ν
a : α
s : Set β
hs : MeasurableSet s
t : Set ℝ
f : ℕ → Set ℝ
hf_disj : Pairwise (Function.onFun Disjoint f)
hf_meas : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, b)) (f i) ∂ν a = (κ a) (s ×ˢ f i)
⊢ ∑' (i : ℕ), ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f✝ hf) (a, a_1)) (f i) ∂ν a = ∑' (i : ℕ), (κ a) (s ×ˢ f i)
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this✝ : IsSFiniteKernel ρCond
this : ∀ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) = {x}.indicator (fun x ↦ (ρCond x) s) a
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ∫⁻ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) ∂ρ.fst

Tactic:
[

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
ρ : Measure (α × Ω)
ρCond : Kernel α Ω
inst✝² : ρ.IsCondKernel ρCond
inst✝¹ : IsFiniteMeasure ρ
inst✝ : MeasurableSingletonClass α
x : α
hx : ρ.fst {x} ≠ 0
s : Set Ω
hs : MeasurableSet s
this✝ : IsSFiniteKernel ρCond
this : ∀ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) = {x}.indicator (fun x ↦ (ρCond x) s) a
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ∫⁻ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) ∂ρ.fst