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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : ℕ → Ω → ℝ
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
n : ℕ
t : ℝ
⊢ charFun (Measure.map (fun ω ↦ (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P) t =
    charFun (Measure.map (X 0) P) ((√↑n)⁻¹ * t) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
⊢ (fun n ↦ ‖1 / ↑n‖) = fun n ↦ ‖1 / ↑n‖

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
⊢ IsPreBrownianReal (fun t ω ↦ B (t₀ + t) ω - B t₀ ω) P

Tactic:
by

Goal state after:
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
⊢ iIndepFun (fun i ω j ↦ X i j ω) P

Tactic:
by

Goal state after:
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 κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ (κ a).real (A ×ˢ Iic ↑↑r)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝ : Finite ι
X : ι → Ω → ℝ
hX : HasGaussianLaw (fun ω x ↦ X x ω) P
h : ∀ (i j : ι), i ≠ j → cov[X i, X j; P] = 0
i j : ι
hij : i ≠ j
L₁ L₂ : StrongDual ℝ ℝ
⊢ cov[⇑L₁ ∘ X i, ⇑L₂ ∘ X j; P] = 0

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
x : ↥{t₀, t₀ + t} → ℝ
⊢ t₀ + t ∈ {t₀, t₀ + t}

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
x : ↥{t₀, t₀ + t} → ℝ
⊢ t₀ ∈ {t₀, t₀ + t}

Tactic:
by

Goal state after:
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 κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
h : ∀ (r : ↑(Ioi q)), ∫ (t : β) in A, ⨅ r', f (a, t) ↑r' ∂ν a ≤ (κ a).real (A ×ˢ Iic ↑↑r)
⊢ ⨅ r, (κ a).real (A ×ˢ Iic ↑↑r) = (κ a).real (A ×ˢ Iic ↑q)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
x y : ↥{t₀, t₀ + t} → ℝ
⊢ (x + y) ⟨t₀ + t, ⋯⟩ - (x + y) ⟨t₀, ⋯⟩ = x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩ + (y ⟨t₀ + t, ⋯⟩ - y ⟨t₀, ⋯⟩)

Tactic:
by

Goal state after:
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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
⊢ AEMeasurable X P

Tactic:
by

Goal state after:
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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
⊢ AEMeasurable Y P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
c : ℝ
x : ↥{t₀, t₀ + t} → ℝ
⊢ (c • x) ⟨t₀ + t, ⋯⟩ - (c • x) ⟨t₀, ⋯⟩ = (RingHom.id ℝ) c • (x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
⊢ ∀ (ω : Ω),
    Sum.elim (fun s ω ↦ B (t₀ + s) ω - B t₀ ω) (fun t ↦ B ↑t) (Sum.inl t) ω =
      { toFun := fun x ↦ x ⟨t₀ + t, ⋯⟩ - x ⟨t₀, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
        ({t₀, t₀ + t}.restrict fun x ↦ B x ω)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
this :
  (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -((↑(√↑n)⁻¹ * ↑t) ^ 2 / 2))) =o[atTop] fun n ↦
    ((√↑n)⁻¹ * t) ^ 2
⊢ (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) - (1 + -↑t ^ 2 / 2 / ↑n)) =o[atTop] fun n ↦ 1 / ↑n

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
ht : t ∈ Set.Iic t₀
x : ↥{t} → ℝ
⊢ t ∈ {t}

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
ht : t ∈ Set.Iic t₀
x y : ↥{t} → ℝ
⊢ (x + y) ⟨t, ⋯⟩ = x ⟨t, ⋯⟩ + y ⟨t, ⋯⟩

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
ht : t ∈ Set.Iic t₀
c : ℝ
x : ↥{t} → ℝ
⊢ (c • x) ⟨t, ⋯⟩ = (RingHom.id ℝ) c • x ⟨t, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
⊢ Tendsto (fun n ↦ (√↑n)⁻¹ * t) atTop (𝓝 0)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
mX : ∀ (t : ℝ≥0), AEMeasurable (B t) P
t : ℝ≥0
ht : t ∈ Set.Iic t₀
⊢ ∀ (ω : Ω),
    Sum.elim (fun s ω ↦ B (t₀ + s) ω - B t₀ ω) (fun t ↦ B ↑t) (Sum.inr ⟨t, ht⟩) ω =
      { toFun := fun x ↦ x ⟨t, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ({t}.restrict fun x ↦ B x ω)

Tactic:
by

Goal state after:
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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
⊢ (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : IsProbabilityMeasure P
X : Ω → ℝ
hX : AEMeasurable X P
h0 : ∫ (x : Ω), X x ∂P = 0
h1 : ∫ (x : Ω), (X ^ 2) x ∂P = 1
t : ℝ
⊢ Tendsto (fun n ↦ charFun (Measure.map X P) ((√↑n)⁻¹ * t) ^ n) atTop (𝓝 (cexp (-↑t ^ 2 / 2)))

Tactic:
by

Goal state after:
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 κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
A : Set β
hA : MeasurableSet A
⊢ ∫ (t : β) in A, ⨅ r, f (a, t) ↑r ∂ν a = (κ a).real (A ×ˢ Iic ↑q)

Tactic:
by

Goal state after:
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'
h0 : ∫ (x : Ω), X 0 x ∂P = 0
h1 : ∫ (x : Ω), (X 0 ^ 2) x ∂P = 1
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
⊢ Tendsto (fun n ↦ ⟨Measure.map (fun ω ↦ (√↑n)⁻¹ * ∑ k ∈ Finset.range n, X k ω) P, ⋯⟩) atTop (𝓝 ⟨Measure.map Y P', ⋯⟩)

Tactic:
by

Goal state after:
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
⊢ 1 ≤ 2

Tactic:
by

Goal state after:
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 κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, ∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q

Tactic:
by

Goal state after:
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
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]

Tactic:
by

Goal state after:
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 κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, IsRatStieltjesPoint f (a, t)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫ (b : β), ↑(f (a, b)) x ∂ν a = (κ a).real (univ ×ˢ Iic x)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
t₀ : ℝ≥0
⊢ (fun ω t ↦ B (t₀ + t) ω - B t₀ ω) ⟂ᵢ[P] fun ω t ↦ B (↑t) ω

Tactic:
by

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

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

Tactic:
by

Goal state after:
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]
⊢ Integrable (fun a ↦ ∫ (x : Ω), X 0 x ∂P) P

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
inst✝ : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫⁻ (b : β), ENNReal.ofReal (↑(f (a, b)) x) ∂ν a = (κ a) (univ ×ˢ Iic x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x✝ : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ ((toKernel f hf) p) (Iic x) = ENNReal.ofReal (↑(f p) x)

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ Directed (fun x y ↦ x ⊆ y) fun q ↦ Iic ↑q

Tactic:
by

Goal state after:
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
⊢ cov[fun ω ↦ ↑s * B (1 / s) ω, fun ω ↦ ↑t * B (1 / t) ω; P] = ↑s

Tactic:
· have := hB.isGaussianProcess.isProbabilityMeasure
    rw [covariance_const_mul_left, covariance_const_mul_right, hB.covariance_eval]
    obtain rfl | hs := eq_or_ne s 0
    · simp
    have : 0 < t := (pos_of_ne_zero hs).trans_le hst
    rw [min_eq_right]
    · norm_cast
      field_simp
    exact one_div_le_one_div_of_le (pos_of_ne_zero hs) hst

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
B : ℝ≥0 → Ω → ℝ
P : Measure Ω
hB : IsPreBrownianReal B P
⊢ IsPreBrownianReal (fun t ω ↦ ↑t * B (1 / t) ω) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
x✝¹ : Ω
x✝ : Continuous fun x ↦ B x x✝¹
⊢ Continuous fun x ↦ (-B) x x✝¹

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
c : ℝ≥0
hc : c ≠ 0
⊢ ∀ᵐ (ω : Ω) ∂P, Continuous fun x ↦ (√↑c)⁻¹ * B (c * x) ω

Tactic:
by

Goal state after:
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
⊢ Directed (fun x y ↦ x ⊆ y) fun q ↦ s ×ˢ Iic ↑q

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
t₀ : ℝ≥0
⊢ ∀ᵐ (ω : Ω) ∂P, Continuous fun x ↦ B (t₀ + x) ω - B t₀ ω

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
B : ℝ≥0 → Ω → ℝ
hB : IsBrownianReal B P
⊢ ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun x ↦ B x ω) (𝓝 0) (𝓝 0)

Tactic:
by

Goal state after:
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]
⊢ ∀ (i : ℕ), Measurable fun x ↦ (x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (β × ε) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
⊢ ξ ×ₖ prodMkLeft β η ∘ₖ (κ ×ₖ deterministic f hf) = ξ ∘ₖ (κ ×ₖ deterministic f hf) ×ₖ (η ∘ₖ deterministic f hf)

Tactic:
by

Goal state after:
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]
n : ℕ
⊢ Measurable fun x ↦ (x - ∫ (x : Ω), X 0 x ∂P) / √Var[X 0; P]

Tactic:
by

Goal state after:
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
⊢ 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:
by

Goal state after:
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
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a = (κ a) (s ×ˢ univ)

Tactic:
by

Goal state after:
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 : α
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a = (κ a) univ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: β : Type u_2
γ : Type u_3
δ : Type u_4
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
β' : Type u_5
ε : Type u_6
mβ' : MeasurableSpace β'
mε : MeasurableSpace ε
κ : Kernel γ β
inst✝² : IsSFiniteKernel κ
η : Kernel ε β'
inst✝¹ : IsSFiniteKernel η
ξ : Kernel (ε × β) δ
inst✝ : IsSFiniteKernel ξ
f : γ → ε
hf : Measurable f
⊢ ξ ×ₖ prodMkRight β η ∘ₖ (deterministic f hf ×ₖ κ) = ξ ∘ₖ (deterministic f hf ×ₖ κ) ×ₖ (η ∘ₖ deterministic f hf)

Tactic:
by

Goal state after:
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
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) tᶜ ∂ν a =
    ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ - ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝ : SFinite μ
⊢ μ ⊗ₘ κ = ⇑(Kernel.id ∥ₖ κ) ∘ₘ ⇑(Kernel.copy α) ∘ₘ μ

Tactic:
by

Goal state after:
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 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] = 0
⊢ ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P

Tactic:
by

Goal state after: