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

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
a : ℝ
h_of_pos : ∀ (a' : ℝ), 0 < a' → μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹
⊢ μ {x | ‖x‖ ≤ a} ≤ 2⁻¹

Tactic:
rcases le_or_gt a 0 with ha | ha

Goal state after:
case inl
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
a : ℝ
h_of_pos : ∀ (a' : ℝ), 0 < a' → μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹
ha : a ≤ 0
⊢ μ {x | ‖x‖ ≤ a} ≤ 2⁻¹

case inr
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
a : ℝ
h_of_pos : ∀ (a' : ℝ), 0 < a' → μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹
ha : 0 < a
⊢ μ {x | ‖x‖ ≤ a} ≤ 2⁻¹
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
x y : ↥(I.disjSum J) → E
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩) =
    (fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)

Tactic:
by ext <;> simp

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
inst✝¹ : CompleteSpace E
S : Type u_4
X : S → Ω → E
Y : T → Ω → E
inst✝ : NormedSpace ℝ E
hXY : IsGaussianProcess (Sum.elim X Y) P
mX : ∀ (s : S), AEMeasurable (X s) P
mY : ∀ (t : T), AEMeasurable (Y t) P
h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X s, ⇑L₂ ∘ Y t; P] = 0
this : IsProbabilityMeasure P
I : Finset S
J : Finset T
c : ℝ
x : ↥(I.disjSum J) → E
⊢ (fun s ↦ (c • x) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (c • x) ⟨Sum.inr ↑t, ⋯⟩) =
    (RingHom.id ℝ) c • (fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩)

Tactic:
by ext <;> simp

Goal state after:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
inst✝¹ : LinearOrder T
I : Finset T
inst✝ : OrderBot T
i j : Fin (#I + 1)
hij : i ≤ j
hi : i ≠ 0
⊢ i.pred hi ≤ j.pred ⋯

Tactic:
by simpa

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
h1 : MeasurableSet {a | Monotone (f a)}
h2 : MeasurableSet {a | Tendsto (f a) atTop (𝓝 1)}
h3 : MeasurableSet {a | Tendsto (f a) atBot (𝓝 0)}
q : ℚ
⊢ MeasurableSet {x | ⨅ r, f x ↑r = f x q}

Tactic:
exact measurableSet_eq_fun (.iInf fun _ ↦ hf.eval) hf.eval

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : (fun ω i ↦ X i ω) ⟂ᵢ[P] Y
h2 : ∀ (i : S), X i =ᵐ[P] X' i
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : Y ⟂ᵢ[P] fun ω i ↦ X i ω
h2 : ∀ (i : S), X i =ᵐ[P] X' i
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : T → Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : (j : T) → MeasurableSpace (𝓨 j)
X X' : (i : S) → Ω → 𝓧 i
Y Y' : (j : T) → Ω → 𝓨 j
hXY : (fun ω i ↦ X i ω) ⟂ᵢ[P] fun ω j ↦ Y j ω
hX : ∀ (i : S), X i =ᵐ[P] X' i
hY : ∀ (j : T), Y j =ᵐ[P] Y' j
⊢ ∀ (i : S), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i =ᵐ[(Kernel.const Unit P) a] X' i

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
T : Type u_2
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : T → Type u_5
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : (j : T) → MeasurableSpace (𝓨 j)
X X' : (i : S) → Ω → 𝓧 i
Y Y' : (j : T) → Ω → 𝓨 j
hXY : (fun ω i ↦ X i ω) ⟂ᵢ[P] fun ω j ↦ Y j ω
hX : ∀ (i : S), X i =ᵐ[P] X' i
hY : ∀ (j : T), Y j =ᵐ[P] Y' j
⊢ ∀ (j : T), ∀ᵐ (a : Unit) ∂Measure.dirac (), Y j =ᵐ[(Kernel.const Unit P) a] Y' j

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) P
hY : AEMeasurable Y P
h : ∀ (I : Finset S), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] Y
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (X i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : S → Type u_4
𝓨 : Type u_5
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), AEMeasurable (X i) P
hY : AEMeasurable Y P
h : ∀ (I : Finset S), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] Y
inst✝ : IsZeroOrProbabilityMeasure P
⊢ AEMeasurable Y (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by simpa

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

Goal state before:
pp: ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
E : ι → Type u_3
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace ℝ (E i)
L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ
hL : ∀ (i : ι), (L i).toBilinForm.IsPosSemidef
x : StrongDual ℝ ((i : ι) → E i)
⊢ 0 ≤ ((diagonalStrongDualPi L).toBilinForm x) x

Tactic:
by
    rw [toBilinForm_diagonalStrongDualPi_apply]
    exact sum_nonneg fun i _ ↦ (hL i).nonneg _

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
inst✝² : MeasurableSpace 𝓧
inst✝¹ : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable X P
hY : ∀ (i : S), AEMeasurable (Y i) P
h : ∀ (I : Finset S), X ⟂ᵢ[P] fun ω i ↦ Y (↑i) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ AEMeasurable X (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : Type u_4
𝓨 : S → Type u_5
inst✝² : MeasurableSpace 𝓧
inst✝¹ : (i : S) → MeasurableSpace (𝓨 i)
X : Ω → 𝓧
Y : (i : S) → Ω → 𝓨 i
hX : AEMeasurable X P
hY : ∀ (i : S), AEMeasurable (Y i) P
h : ∀ (I : Finset S), X ⟂ᵢ[P] fun ω i ↦ Y (↑i) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (Y i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) P
hY : ∀ (j : T), AEMeasurable (Y j) P
h : ∀ (I : Finset S) (J : Finset T), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] fun ω j ↦ Y (↑j) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (i : S), AEMeasurable (X i) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : Type u_4
𝓧 : S → Type u_5
𝓨 : T → Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : (j : T) → MeasurableSpace (𝓨 j)
X : (i : S) → Ω → 𝓧 i
Y : (j : T) → Ω → 𝓨 j
hX : ∀ (i : S), AEMeasurable (X i) P
hY : ∀ (j : T), AEMeasurable (Y j) P
h : ∀ (I : Finset S) (J : Finset T), (fun ω i ↦ X (↑i) ω) ⟂ᵢ[P] fun ω j ↦ Y (↑j) ω
inst✝ : IsZeroOrProbabilityMeasure P
⊢ ∀ (j : T), AEMeasurable (Y j) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : S → Type u_4
𝓧 : (i : S) → T i → Type u_5
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), X i j =ᵐ[P] X' i j
⊢ ∀ (i : S) (j : T i), ∀ᵐ (a : Unit) ∂Measure.dirac (), X i j =ᵐ[(Kernel.const Unit P) a] X' i j

Tactic:
by simpa

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

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
T : S → Type u_4
𝓧 : (i : S) → T i → Type u_5
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), AEMeasurable (X i j) P
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) P
⊢ ∀ (i : S) (j : T i), AEMeasurable (X i j) (⇑(Kernel.const Unit P) ∘ₘ Measure.dirac ())

Tactic:
by simpa

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 : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : (ν a).restrict s = 0
q : ℚ
hq : x < ↑q
this : (κ a) (s ×ˢ Iic ↑q) = 0
⊢ 0 = (κ a) (s ×ˢ Iic x)

Tactic:
by
      symm
      refine measure_mono_null (fun p ↦ ?_) this
      simp only [mem_prod, mem_Iic, and_imp]
      exact fun h1 h2 ↦ ⟨h1, h2.trans hq.le⟩

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 ι
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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ IsGaussian (Measure.map (fun ω x ↦ X x ω) P)

Tactic:
isGaussian_iff_gaussian_charFunDual

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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
this✝ : IsProbabilityMeasure P
this : Fintype ι := Fintype.ofFinite ι
⊢ ∃ m f,
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ ((x : ι) → E x)),
        charFunDual (Measure.map (fun ω x ↦ X x ω) P) L = cexp (↑(L m) * I - ↑((f L) L) / 2)
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
hX1 : ∀ (i : ι), HasGaussianLaw (X i) P
hX2 : iIndepFun X P
⊢ IsGaussian (Measure.map (fun ω x ↦ X x ω) P)

Tactic:
have := hX2.isProbabilityMeasure
    let := Fintype.ofFinite ι
    rw [isGaussian_iff_gaussian_charFunDual]
    classical
    refine ⟨fun i ↦ ∫ x, x ∂P.map (X i),
      .diagonalStrongDualPi (fun i ↦ covarianceBilinDual (P.map (X i))),
      isPosSemidef_diagonalStrongDualPi (fun _ ↦ isPosSemidef_covarianceBilinDual), fun L ↦ ?_⟩
    rw [(iIndepFun_iff_charFunDual_pi (by fun_prop)).1 hX2]
    simp only [← LinearMap.sum_single_apply E (fun i ↦ ∫ x, x ∂P.map (X i)), map_sum, ofReal_sum,
      sum_mul, diagonalStrongDualPi_apply, sum_div, ← sum_sub_distrib, exp_sum]
    congr with i
    rw [(hX1 i).isGaussian_map.charFunDual_eq, integral_complex_ofReal, integral_comp_id_comm,
      covarianceBilinDual_self_eq_variance]
    · simp
    · exact (hX1 i).isGaussian_map.memLp_two_id
    · exact (hX1 i).isGaussian_map.integrable_id

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst
⊢ ∫⁻ (x : α) in s, 1 x ∂ρ.fst.withDensity (preCDF ρ r) = (ρ.IicSnd ↑r) s

pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst
⊢ Measurable 1

Tactic:
· simp only [withDensity_preCDF ρ r, Pi.one_apply, lintegral_one, Measure.restrict_apply,
      MeasurableSet.univ, univ_inter]

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst✝ : IsFiniteMeasure ρ
this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, (preCDF ρ r * 1) x ∂ρ.fst
⊢ Measurable 1
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 : ℝ
⊢ ∫ (b : β), ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = (κ a).real (univ ×ˢ Iic x)

Tactic:
by
  rw [← setIntegral_univ, setIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]

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 ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ‖⨅ r, f (a, t) ↑r‖ ≤ 1

Tactic:
rw [Real.norm_eq_abs, abs_of_nonneg]

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ ⨅ r, f (a, t) ↑r ≤ 1

α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
t : β
hbdd_below : ∀ (q : ℚ), BddBelow (range fun r ↦ f (a, t) ↑r)
h_nonneg : ∀ (q : ℚ), 0 ≤ f (a, t) q
h_le_one : ∀ (q : ℚ), f (a, t) q ≤ 1
⊢ 0 ≤ ⨅ r, f (a, t) ↑r
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
⊢ IsGaussian (Measure.map (fun ω ↦ (X ω, Y ω)) P)

Tactic:
isGaussian_iff_gaussian_charFunDual

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
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this : IsProbabilityMeasure P
⊢ ∃ m f,
    f.toBilinForm.IsPosSemidef ∧
      ∀ (L : StrongDual ℝ (E × F)),
        charFunDual (Measure.map (fun ω ↦ (X ω, Y ω)) P) L = cexp (↑(L m) * I - ↑((f L) L) / 2)
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 : β
ht_top : Tendsto (f (a, t)) atTop (𝓝 1)
⊢ Tendsto (f (a, t)) atBot (𝓝 0) →
    (∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q) → Monotone (f (a, t)) → IsRatStieltjesPoint f (a, t)

Tactic:
ht_bot

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
t : β
ht_top : Tendsto (f (a, t)) atTop (𝓝 1)
ht_bot : Tendsto (f (a, t)) atBot (𝓝 0)
⊢ (∀ (q : ℚ), ⨅ r, f (a, t) ↑r = f (a, t) q) → Monotone (f (a, t)) → IsRatStieltjesPoint f (a, t)
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
⊢ (ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)

Tactic:
by
  have := isSFiniteKernel ρ ρCond (by rintro rfl; simp at hx)
  nth_rewrite 2 [← ρ.disintegrate ρCond]
  rw [Measure.compProd_apply (measurableSet_prod.mpr (Or.inl ⟨measurableSet_singleton x, hs⟩))]
  have (a : _) : ρCond a (Prod.mk a ⁻¹' {x} ×ˢ s) = ({x} : Set α).indicator (ρCond · s) a := by
    obtain rfl | hax := eq_or_ne a x
    · simp only [singleton_prod, mem_singleton_iff, indicator_of_mem]
      congr with y
      simp
    · simp only [singleton_prod, mem_singleton_iff, hax, not_false_eq_true, indicator_of_notMem]
      have : Prod.mk a ⁻¹' Prod.mk x '' s = ∅ := by ext y; simp [Ne.symm hax]
      simp only [this, measure_empty]
  simp_rw [this]
  rw [MeasureTheory.lintegral_indicator (measurableSet_singleton x)]
  simp only [Measure.restrict_singleton, lintegral_smul_measure, lintegral_dirac, smul_eq_mul]
  rw [← mul_assoc, ENNReal.inv_mul_cancel hx (measure_ne_top _ _), one_mul]

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

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

Tactic:
convert! this
    ext x
    simp

Goal state after:
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 ≤ ν
n : ℕ
a : α
x : γ
s : Set β
⊢ (κ a) (countablePartitionSet n x ×ˢ s) ≤ (κ.fst a) (countablePartitionSet n x)

Tactic:
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]
        refine measure_mono (fun x ↦ ?_)
        simp only [mem_prod, mem_ofPred_eq, and_imp]
        exact fun h _ ↦ h

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

Goal state before:
pp: case hfm
α : 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
⊢ AEMeasurable (fun x ↦ (κ a) (countablePartitionSet n x ×ˢ s) / (ν a) (countablePartitionSet n x)) ((ν a).restrict u)

Tactic:
refine Measurable.aemeasurable ?_
    change Measurable ((fun (p : α × _) ↦ κ p.1 (countablePartitionSet n p.2 ×ˢ s)
      / ν p.1 (countablePartitionSet n p.2)) ∘ (fun x ↦ (a, x)))
    exact (measurable_densityProcess_aux κ ν n hs).comp measurable_prodMk_left

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

Goal state before:
pp: case hf
Ω : 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
⊢ Integrable (⇑(L ∘SL inl ℝ E F) ∘ X) P

Tactic:
exact (hXY.fst.map _).integrable

Goal state after: