mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
⊢ (fun i ↦ (m • x) ⟨t i.succ, ⋯⟩ - (m • x) ⟨t i.castSucc, ⋯⟩) =
    (RingHom.id ℝ) m • fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩

Tactic:
ext

Goal state after:
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
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
n : ℕ
t : Fin (n + 1) → T
m : ℝ
x : ↥(image t univ) → E
x✝ : Fin n
⊢ (m • x) ⟨t x✝.succ, ⋯⟩ - (m • x) ⟨t x✝.castSucc, ⋯⟩ =
    ((RingHom.id ℝ) m • fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: S : Type u_1
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
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
x y : ↥(I.biUnion J) → E
⊢ (fun s ↦ (L ↑s) fun t ↦ (x + y) ⟨↑t, ⋯⟩) = (fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩) + fun s ↦ (L ↑s) fun t ↦ y ⟨↑t, ⋯⟩

Tactic:
ext

Goal state after:
S : Type u_1
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
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
x y : ↥(I.biUnion J) → E
x✝ : ↥I
⊢ ((L ↑x✝) fun t ↦ (x + y) ⟨↑t, ⋯⟩) = ((fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩) + fun s ↦ (L ↑s) fun t ↦ y ⟨↑t, ⋯⟩) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: S : Type u_1
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
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
c : ℝ
x : ↥(I.biUnion J) → E
⊢ (fun s ↦ (L ↑s) fun t ↦ (c • x) ⟨↑t, ⋯⟩) = (RingHom.id ℝ) c • fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩

Tactic:
ext

Goal state after:
S : Type u_1
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
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
c : ℝ
x : ↥(I.biUnion J) → E
x✝ : ↥I
⊢ ((L ↑x✝) fun t ↦ (c • x) ⟨↑t, ⋯⟩) = ((RingHom.id ℝ) c • fun s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩) x✝
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
⊢ charFun (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFun (Measure.map (X i) P)

Tactic:
ext

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
s : Finset ι
E : Type u_3
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : ι → Ω → E
inst✝ : InnerProductSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
x✝ : E
⊢ charFun (Measure.map (∑ i ∈ s, X i) P) x✝ = (∏ i ∈ s, charFun (Measure.map (X i) P)) x✝
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ charFun (Measure.map (fun p ↦ ∑ i, p i) (Measure.pi μ)) = ∏ i, charFun (μ i)

Tactic:
ext

Goal state after:
ι : Type u_2
E : Type u_3
inst✝⁶ : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : Fintype ι
inst✝¹ : InnerProductSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
x✝ : E
⊢ charFun (Measure.map (fun p ↦ ∑ i, p i) (Measure.pi μ)) x✝ = (∏ i, charFun (μ i)) x✝
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: S : Type u_1
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
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  { toFun := fun x s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
⊢ (fun ω ↦ I.restrict fun x ↦ Y x ω) = ⇑K ∘ fun ω ↦ (I.biUnion J).restrict fun x ↦ X x ω

Tactic:
ext

Goal state after:
S : Type u_1
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
inst✝⁵ : SecondCountableTopology E
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
Y : S → Ω → F
hX : IsGaussianProcess X P
I : Finset S
J : S → Finset T
L : (s : S) → (↥(J s) → E) →L[ℝ] F
hL : ∀ (s : S) (ω : Ω), Y s ω = (L s) ((J s).restrict fun x ↦ X x ω)
K : (↥(I.biUnion J) → E) →L[ℝ] ↥I → F :=
  { toFun := fun x s ↦ (L ↑s) fun t ↦ x ⟨↑t, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
x✝¹ : Ω
x✝ : ↥I
⊢ I.restrict (fun x ↦ Y x x✝¹) x✝ = (⇑K ∘ fun ω ↦ (I.biUnion J).restrict fun x ↦ X x ω) 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)
x y : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
⊢ (fun i j ↦ (x + y) ⟨⟨↑i, ↑j⟩, ⋯⟩) = (fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩) + fun i j ↦ y ⟨⟨↑i, ↑j⟩, ⋯⟩

Tactic:
ext

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)
x y : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
x✝¹ : ↥I
x✝ : ↥(J x✝¹)
⊢ (x + y) ⟨⟨↑x✝¹, ↑x✝⟩, ⋯⟩ = ((fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩) + fun i j ↦ y ⟨⟨↑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)
c : ℝ
x : ↥(I.sigma fun i ↦ if hi : i ∈ I then J ⟨i, hi⟩ else ∅) → E
⊢ (fun i j ↦ (c • x) ⟨⟨↑i, ↑j⟩, ⋯⟩) = (RingHom.id ℝ) c • fun i j ↦ x ⟨⟨↑i, ↑j⟩, ⋯⟩

Tactic:
ext

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)
⊢ (⇑L₁ ∘ fun ω k ↦ X (↑i) (↑k) ω) = ∑ k, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑i ↑k

Tactic:
ext

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
⊢ (⇑L₂ ∘ fun ω k ↦ X (↑j) (↑k) ω) = ∑ k, ⇑(L₂ ∘SL ContinuousLinearMap.single ℝ (fun j ↦ E) k) ∘ X ↑j ↑k

Tactic:
ext

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)
⊢ (fun ω i ↦ X i ω) ⁻¹' (↑I).pi s = (fun ω i ↦ X (↑i) ω) ⁻¹' (↑Finset.univ).pi fun i ↦ s ↑i

Tactic:
ext

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
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:
ext

Goal state after:
case fst
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
x✝ : ↥I
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩).1 x✝ =
    ((fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)).1
      x✝

case snd
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
x✝ : ↥J
⊢ (fun s ↦ (x + y) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (x + y) ⟨Sum.inr ↑t, ⋯⟩).2 x✝ =
    ((fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩) + (fun s ↦ y ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ y ⟨Sum.inr ↑t, ⋯⟩)).2
      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 : 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:
ext

Goal state after:
case fst
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
x✝ : ↥I
⊢ (fun s ↦ (c • x) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (c • x) ⟨Sum.inr ↑t, ⋯⟩).1 x✝ =
    ((RingHom.id ℝ) c • (fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩)).1 x✝

case snd
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
x✝ : ↥J
⊢ (fun s ↦ (c • x) ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ (c • x) ⟨Sum.inr ↑t, ⋯⟩).2 x✝ =
    ((RingHom.id ℝ) c • (fun s ↦ x ⟨Sum.inl ↑s, ⋯⟩, fun t ↦ x ⟨Sum.inr ↑t, ⋯⟩)).2 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 : 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)
⊢ (⇑L₁ ∘ fun ω i ↦ X (↑i) ω) = ∑ i, ⇑(L₁ ∘SL ContinuousLinearMap.single ℝ (fun i ↦ E) i) ∘ X ↑i

Tactic:
ext

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
⊢ (fun x ↦ ‖x‖ ≤ b) ⁻¹' {True} = {x | ‖x‖ ≤ b}

Tactic:
ext

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}