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

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x - c) μ)

Tactic:
simp_rw [sub_eq_add_neg]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x + -c) μ)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c - x) μ)

Tactic:
simp_rw [sub_eq_add_neg]

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c + -x) μ)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) μ

Tactic:
simp_rw [← norm_mul]
      exact (MemLp.integrable_mul (h.continuousLinearMap_comp L₁)
        (h.continuousLinearMap_comp L₂)).norm

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
L : StrongDual ℝ F
⊢ charFunDual (Measure.map (⇑f) (stdGaussian E)) L = charFunDual (stdGaussian F) L

Tactic:
show ⇑f = f.toContinuousLinearEquiv.toContinuousLinearMap from rfl,

Goal state after:
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace ℝ E
inst✝⁶ : FiniteDimensional ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : E ≃ₗᵢ[ℝ] F
this : FiniteDimensional ℝ F
L : StrongDual ℝ F
⊢ charFunDual (Measure.map (⇑↑↑f) (stdGaussian E)) L = charFunDual (stdGaussian F) L
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
μ : Measure E
inst✝ : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
⊢ ∃ C, 0 < C ∧ Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ

Tactic:
refine ⟨C / 2, by positivity, ?_⟩

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
μ : Measure E
inst✝ : IsGaussian μ
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) (μ ∗ Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)
⊢ Integrable (fun x ↦ rexp (C / 2 * ‖x‖ ^ 2)) μ
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ IsGaussian (multivariateGaussian μ S)

Tactic:
have h : (fun x ↦ μ + (toEuclideanCLM (𝕜 := ℝ) (CFC.sqrt S)) x) =
    (fun x ↦ μ + x) ∘ ((toEuclideanCLM (𝕜 := ℝ) (CFC.sqrt S))) := rfl

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
h : (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) = (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S))
⊢ IsGaussian (multivariateGaussian μ S)
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : SecondCountableTopology E
inst✝⁵ : CompleteSpace E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : InnerProductSpace ℝ E
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν
hv : covarianceBilin μ = covarianceBilin ν
⊢ μ = ν

Tactic:
apply Measure.ext_of_charFun
  ext t
  simp_rw [IsGaussian.charFun_eq', hm, hv]

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

Goal state before:
pp: I : Finset ℝ≥0
⊢ Measure.map (toLp 2 ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (covMatrix I)) =
    multivariateGaussian 0 (covMatrix I)

pp: case hg
I : Finset ℝ≥0
⊢ Measurable (toLp 2)

pp: case hf
I : Finset ℝ≥0
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm

Tactic:
· simp [← MeasurableEquiv.coe_toLp]

Goal state after:
case hg
I : Finset ℝ≥0
⊢ Measurable (toLp 2)

case hf
I : Finset ℝ≥0
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
⊢ (PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ) (∫ (x : EuclideanSpace ℝ ↥I), x ∂multivariateGaussian 0 (covMatrix I)) = 0

Tactic:
integral_id_multivariateGaussian,

Goal state after:
I : Finset ℝ≥0
⊢ (PiLp.continuousLinearEquiv 2 ℝ fun a ↦ ℝ) 0 = 0
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case hg
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable (Finset.restrict₂ hJI)

pp: case hf
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm

Tactic:
· exact Finset.measurable_restrict₂ _

Goal state after:
case hf
I J : Finset ℝ≥0
hJI : J ⊆ I
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess X P
t : T
⊢ HasGaussianLaw (X t) P

Tactic:
exact (hX.hasGaussianLaw {t}).map (.proj ⟨t, by simp⟩)

Goal state after:
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f i
h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : ↑(I i)) → 𝓧 i ↑a)
hI : ∀ i ∈ s, (I i).Countable
hu : ∀ i ∈ s, g i = (I i).domRestrict ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' g i = ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i
h4' :
  ∀ (a : α) (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ∏ i ∈ s, (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' g i) =
      ∏ i ∈ s, (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i)
h6 :
  ∀ (i : S) (f : (j : T i) → Ω → 𝓧 i j), (fun ω j ↦ f j ω) ⁻¹' (I i).domRestrict ⁻¹' u i = (fun ω j ↦ f (↑j) ω) ⁻¹' u i
h5 : ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, (fun ω j ↦ X i (↑j) ω) ⁻¹' u i) = ∏ x ∈ s, (κ a) ((fun ω j ↦ X x (↑j) ω) ⁻¹' u x)
i : S
hi : i ∈ ↑s
⊢ ∀ᵐ (x : α) ∂P, (fun ω j ↦ X i (↑j) ω) =ᵐ[κ x] fun ω j ↦ X' i (↑j) ω

Tactic:
have := (hI i hi).to_subtype

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f i
h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
I : (i : S) → Set (T i)
u : (i : S) → Set ((a : ↑(I i)) → 𝓧 i ↑a)
hI : ∀ i ∈ s, (I i).Countable
hu : ∀ i ∈ s, g i = (I i).domRestrict ⁻¹' u i
h4 :
  ∀ (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' g i = ⋂ i ∈ s, (fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i
h4' :
  ∀ (a : α) (f : (i : S) → (j : T i) → Ω → 𝓧 i j),
    ∏ i ∈ s, (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' g i) =
      ∏ i ∈ s, (κ a) ((fun i ω j ↦ f i j ω) i ⁻¹' (I i).domRestrict ⁻¹' u i)
h6 :
  ∀ (i : S) (f : (j : T i) → Ω → 𝓧 i j), (fun ω j ↦ f j ω) ⁻¹' (I i).domRestrict ⁻¹' u i = (fun ω j ↦ f (↑j) ω) ⁻¹' u i
h5 : ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, (fun ω j ↦ X i (↑j) ω) ⁻¹' u i) = ∏ x ∈ s, (κ a) ((fun ω j ↦ X x (↑j) ω) ⁻¹' u x)
i : S
hi : i ∈ ↑s
this : Countable ↑(I i)
⊢ ∀ᵐ (x : α) ∂P, (fun ω j ↦ X i (↑j) ω) =ᵐ[κ x] fun ω j ↦ X' i (↑j) ω
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, (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫, fun ω ↦ ⟪y, (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫; P] = 0

Tactic:
rw [← (EuclideanSpace.basisFun _ _).sum_repr x, ← (EuclideanSpace.basisFun _ _).sum_repr y]

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 ω ↦
      ⟪∑ i_1, ((EuclideanSpace.basisFun (κ i) ℝ).repr x).ofLp i_1 • (EuclideanSpace.basisFun (κ i) ℝ) i_1,
        (toLp 2 ∘ fun ω j ↦ X i j ω) ω⟫,
      fun ω ↦
      ⟪∑ i, ((EuclideanSpace.basisFun (κ j) ℝ).repr y).ofLp i • (EuclideanSpace.basisFun (κ j) ℝ) i,
        (toLp 2 ∘ fun ω j_1 ↦ X j j_1 ω) ω⟫;
      P] =
    0
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_3
α : 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)
⊢ (fun t ↦ ⨅ r', f (a, t) ↑r') ≤ᵐ[ν a] fun c ↦ f (a, c) ↑r

Tactic:
filter_upwards [hf.bddBelow_range a] with t ht using ciInf_le (ht _) r

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:
simp_rw [IsCondKernelCDF.toKernel_Iic]
  exact hf.setLIntegral _ hs _

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

Goal state before:
pp: case e_f
β : 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
ω : γ
s : Set (δ × β')
hs : MeasurableSet s
b : β
⊢ ((ξ ×ₖ prodMkLeft β η) (b, f ω)) s = ∫⁻ (c : δ), ((η ∘ₖ deterministic f hf) ω) (Prod.mk c ⁻¹' s) ∂ξ (b, f ω)

Tactic:
rw [prod_apply' _ _ _ hs, prodMkLeft_apply, comp_deterministic_eq_comap, comap_apply]

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

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

Tactic:
rw [compProd_eq_comp_prod, ← Kernel.parallelComp_comp_copy, Measure.comp_assoc]

Goal state after:
Module: Mathlib.Probability.CentralLimitTheorem

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

Tactic:
have : ∀ᵐ ω ∂P, ∀ n, X n ω = P[X 0] := by
      refine ae_all_iff.2 fun n ↦ ?_
      convert! (ae_eq_integral_of_variance_eq_zero ((hident n).memLp_iff.2 hX)) ?_ using 3
      · rw [(hident n).integral_eq]
      · rwa [(hident n).variance_eq]

Goal state after:
case inl
Ω : 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
this : ∀ᵐ (ω : Ω) ∂P, ∀ (n : ℕ), X n ω = ∫ (x : Ω), X 0 x ∂P
⊢ TendstoInDistribution (fun n ω ↦ (√↑n)⁻¹ * (∑ k ∈ Finset.range n, X k ω - ↑n * ∫ (x : Ω), X 0 x ∂P)) atTop Y
    (fun x ↦ P) P'
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
⊢ ∀ (b : ℝ≥0∞), 1 < b → (κ.fst a) {x | b ≤ (κCond (a, x)) univ} = 0

Tactic:
intro r hr

Goal state after:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x ↦ r) ≤ s.indicator fun b ↦ (κCond (a, b)) univ
this : ∫⁻ (b : β), s.indicator (fun x ↦ r) b ∂κ.fst a ≤ (κ.fst a) s
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0

Tactic:
lintegral_indicator_const hs

Goal state after:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x ↦ r) ≤ s.indicator fun b ↦ (κCond (a, b)) univ
this : r * (κ.fst a) s ≤ (κ.fst a) s
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ ∀ᵐ (x : γ) ∂(ν a).restrict u, (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x) < ∞

pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ (∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a).toReal =
    (κ a).real (u ×ˢ s)

Tactic:
· refine ae_of_all _ (fun x ↦ ?_)
    by_cases h0 : ν a (countablePartitionSet n x) = 0
    · suffices κ a (countablePartitionSet n x ×ˢ s) = 0 by simp [h0, this]
      have h0' : fst κ a (countablePartitionSet n x) = 0 := by simpa using (hκν a _).trans h0.le
      rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h0'
      refine measure_mono_null (fun x ↦ ?_) h0'
      simp only [mem_prod, mem_ofPred_eq, and_imp]
      exact fun h _ ↦ h
    · finiteness

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
hν : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
u : Set γ
hu : u ∈ countablePartition γ n
this : IsFiniteKernel κ
hu_meas : MeasurableSet u
⊢ (∫⁻ (a_1 : γ) in u, (κ a) (countablePartitionSet n a_1 ×ˢ s) / (ν a) (countablePartitionSet n a_1) ∂ν a).toReal =
    (κ a).real (u ×ˢ s)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_4
κ : Type u_5
inst✝¹ : Finite ι
inst✝ : Finite κ
X : ι → Ω → ℝ
Y : κ → Ω → ℝ
hXY : HasGaussianLaw (fun ω ↦ (fun i ↦ X i ω, fun j ↦ Y j ω)) P
h : ∀ (i : ι) (j : κ), cov[X i, Y j; P] = 0
this✝¹ : IsProbabilityMeasure P
hX : (fun ω i ↦ X i ω) = ofLp ∘ toLp 2 ∘ fun ω i ↦ X i ω
hY : (fun ω j ↦ Y j ω) = ofLp ∘ toLp 2 ∘ fun ω j ↦ Y j ω
this✝ : Fintype ι := Fintype.ofFinite ι
this : Fintype κ := Fintype.ofFinite κ
x : WithLp 2 (ι → ℝ)
y : WithLp 2 (κ → ℝ)
⊢ cov[fun ω ↦ ⟪x, (toLp 2 ∘ fun ω i ↦ X i ω) ω⟫, fun ω ↦ ⟪y, (toLp 2 ∘ fun ω j ↦ Y j ω) ω⟫; P] = 0

Tactic:
rw [← (EuclideanSpace.basisFun _ _).sum_repr x, ← (EuclideanSpace.basisFun _ _).sum_repr y]

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

Goal state before:
pp: case pos.right
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
⊢ ∀ b < 1, (κ.fst a) {x | (κCond (a, x)) univ ≤ b} = 0

Tactic:
intro r hr

Goal state after:
case pos.right
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
⊢ (κ.fst a) {x | (κCond (a, x)) univ ≤ r} = 0