mathlib-initiative/mathlib-tactics huggingface dataset:
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 : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
c : ℝ
x : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
x✝¹ : ↥I
x✝ : ↥(J x✝¹)
⊢ (c • x) ⟨⟨↑x✝¹, ↑x✝⟩, ⋯⟩ = ((RingHom.id ℝ) c • fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩) x✝¹ x✝

Tactic:
;

Goal state after:
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 : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
c : ℝ
x : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
x✝¹ : ↥I
x✝ : ↥(J x✝¹)
⊢ (c • x) ⟨⟨↑x✝¹, ↑x✝⟩, ⋯⟩ = ((RingHom.id ℝ) c • fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩) x✝¹ x✝
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 : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
x✝ : Ω
⊢ (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) x✝ = (∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k) x✝

Tactic:
;

Goal state after:
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 : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
x✝ : Ω
⊢ (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) x✝ = (∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k) x✝
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 : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
h1 : (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) = ∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k
x✝ : Ω
⊢ (⇑L₂ ∘ fun ω k ↦ X (↑j) (↑k) ω) x✝ = (∑ k, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑j ↑k) x✝

Tactic:
;

Goal state after:
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 : T → Type u_4
X : (t : T) → S t → Ω → E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess (fun p ω ↦ X p.fst p.snd ω) P
mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P
h :
  ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), cov[⇑L₁ ∘ X t₁ s₁, ⇑L₂ ∘ X t₂ s₂; P] = 0
this : IsProbabilityMeasure P
I : Finset T
J : (i : ↥I) → Finset (S ↑i)
i j : ↥I
hij : i ≠ j
L₁ : StrongDual ℝ (↥(J i) → E)
L₂ : StrongDual ℝ (↥(J j) → E)
h1 : (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) = ∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k
x✝ : Ω
⊢ (⇑L₂ ∘ fun ω k ↦ X (↑j) (↑k) ω) x✝ = (∑ k, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑j ↑k) x✝
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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
x✝ : Ω
⊢ x✝ ∈ (fun ω i ↦ X i ω) ⁻¹' (↑I).pi s ↔ x✝ ∈ (fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i

Tactic:
;

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
πX_gen : MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX
I : Finset S
s : (i : S) → Set (𝓧 i)
t : Set 𝓨
ht : MeasurableSet t
hs : ∀ (i : S), MeasurableSet (s i)
x✝ : Ω
⊢ x✝ ∈ (fun ω i ↦ X i ω) ⁻¹' (↑I).pi s ↔ x✝ ∈ (fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i
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
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
x✝ : Ω
⊢ (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) x✝ = (∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i) x✝

Tactic:
;

Goal state after:
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
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
x✝ : Ω
⊢ (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) x✝ = (∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i) x✝
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} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
x✝ : E
⊢ x✝ ∈ (fun x ↦ ‖x‖ ≤ b) ⁻¹' {True} ↔ x✝ ∈ {x | ‖x‖ ≤ b}

Tactic:
;

Goal state after:
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} ∧ μ {x | ‖x‖ ≤ a} < 1
b : ℝ
hb : μ {x | ‖x‖ ≤ b} = 1
x✝ : E
⊢ x✝ ∈ (fun x ↦ ‖x‖ ≤ b) ⁻¹' {True} ↔ x✝ ∈ {x | ‖x‖ ≤ b}
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
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
h1 : (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i
x✝ : Ω
⊢ (⇑L₂ ∘ fun ω j ↦ Y (↑j) ω) x✝ = (∑ j, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j) x✝

Tactic:
;

Goal state after:
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
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
h1 : (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i
x✝ : Ω
⊢ (⇑L₂ ∘ fun ω j ↦ Y (↑j) ω) x✝ = (∑ j, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) j) ∘ Y ↑j) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence

Goal state before:
pp: case refine_2
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
L₁ : StrongDual ℝ (↥I → E)
L₂ : StrongDual ℝ (↥J → E)
⊢ cov[⇑L₁ ∘ fun ω i ↦ X (↑i) ω, ⇑L₂ ∘ fun ω j ↦ Y (↑j) ω; P] = 0

Tactic:
have h1 : L₁ ∘ (fun ω i ↦ X i ω) = ∑ i : I, (L₁ ∘L .single ℝ _ i) ∘ X i := by
    ext; simp [-ContinuousLinearMap.comp_apply, ← L₁.sum_comp_single]
  have h2 : L₂ ∘ (fun ω j ↦ Y j ω) = ∑ j : J, (L₂ ∘L .single ℝ _ j) ∘ Y j := by
    ext; simp [-ContinuousLinearMap.comp_apply, ← L₂.sum_comp_single]
  rw [h1, h2, covariance_sum_sum]
  · exact sum_eq_zero fun i _ ↦ sum_eq_zero fun j _ ↦ h ..
  · exact fun s ↦ ((hXY.hasGaussianLaw_eval (.inl s)).map _).memLp_two
  · exact fun t ↦ ((hXY.hasGaussianLaw_eval (.inr t)).map _).memLp_two

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : LinearOrder T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
I : Finset T
x y : Fin #I → E
x✝ : ↥I
⊢ ∑ j ≤ (I.orderIsoOfFin ⋯).symm x✝, (x + y) j =
    ((fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, x j) + fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, y j) x✝

Tactic:
;

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : LinearOrder T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
I : Finset T
x y : Fin #I → E
x✝ : ↥I
⊢ ∑ j ≤ (I.orderIsoOfFin ⋯).symm x✝, (x + y) j =
    ((fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, x j) + fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, y j) x✝
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : LinearOrder T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
I : Finset T
m : R
x : Fin #I → E
x✝ : ↥I
⊢ ∑ j ≤ (I.orderIsoOfFin ⋯).symm x✝, (m • x) j = ((RingHom.id R) m • fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, x j) x✝

Tactic:
;

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : LinearOrder T
R : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid E
inst✝² : Module R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd E
I : Finset T
m : R
x : Fin #I → E
x✝ : ↥I
⊢ ∑ j ≤ (I.orderIsoOfFin ⋯).symm x✝, (m • x) j = ((RingHom.id R) m • fun i ↦ ∑ j ≤ (I.orderIsoOfFin ⋯).symm i, x j) x✝
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.IsGaussianProcess

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : LinearOrder T
inst✝⁶ : OrderBot T
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
⊢ HasGaussianLaw (fun ω ↦ I.restrict fun x ↦ X x ω) P

Tactic:
have := (law ⊥).isProbabilityMeasure

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : LinearOrder T
inst✝⁶ : OrderBot T
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
X : T → Ω → E
law : ∀ (t : T), HasGaussianLaw (X t) P
h_bot : ∀ᵐ (ω : Ω) ∂P, X ⊥ ω = 0
incr : HasIndepIncrements X P
I : Finset T
this : IsProbabilityMeasure P
⊢ HasGaussianLaw (fun ω ↦ I.restrict fun x ↦ X x ω) P
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 : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
x✝ : Ω
⊢ x✝ ∈ ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) ↔
    x✝ ∈ ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j

Tactic:
;

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 : (i : S) → (j : T i) → Ω → 𝓧 i j
hX : ∀ (i : S) (j : T i), Measurable (X i j)
h : ∀ (I : Finset S) (J : (i : ↥I) → Finset (T ↑i)), iIndepFun (fun i ω j ↦ X (↑i) (↑j) ω) κ P
hμ : P ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[P] ⇑η
hη : IsMarkovKernel η
π : S → Set (Set Ω) := fun i ↦ {s | ∃ t ∈ squareCylinders fun j ↦ {s | MeasurableSet s}, (fun ω j ↦ X i j ω) ⁻¹' t = s}
π_pi : ∀ (i : S), IsPiSystem (π i)
π_gen : ∀ (i : S), MeasurableSpace.comap (fun ω j ↦ X i j ω) MeasurableSpace.pi = generateFrom (π i)
I : Finset S
s : S → Set Ω
J : (i : S) → Finset (T i)
t : (i : S) → (i_1 : T i) → Set (𝓧 i i_1)
ht : ∀ i ∈ I, ∀ (i_1 : T i), MeasurableSet (t i i_1)
hs : ∀ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) = s i
x✝ : Ω
⊢ x✝ ∈ ⋂ i ∈ I, (fun ω j ↦ X i j ω) ⁻¹' (↑(J i)).pi (t i) ↔
    x✝ ∈ ⋂ i ∈ Finset.univ, (fun ω j ↦ X (↑i) (↑j) ω) ⁻¹' (↑Finset.univ).pi fun j ↦ t ↑i ↑j
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Monotone (f a)

pp: case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Monotone (g a)

Tactic:
;

Goal state after:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Monotone (f a)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Monotone (g a)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atTop (𝓝 1)

pp: case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atTop (𝓝 1)

Tactic:
;

Goal state after:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atTop (𝓝 1)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atTop (𝓝 1)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atBot (𝓝 0)

pp: case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atBot (𝓝 0)

Tactic:
;

Goal state after:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atBot (𝓝 0)

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atBot (𝓝 0)
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t

pp: case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ ∀ (t : ℚ), ⨅ r, g a ↑r = g a t

Tactic:
;

Goal state after:
case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ ∀ (t : ℚ), ⨅ r, f a ↑r = f a t

case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ ∀ (t : ℚ), ⨅ r, g a ↑r = g a t