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
x y : ↥(image t univ) → E
⊢ (fun i ↦ (x + y) ⟨t i.succ, ⋯⟩ - (x + y) ⟨t i.castSucc, ⋯⟩) =
    (fun i ↦ x ⟨t i.succ, ⋯⟩ - x ⟨t i.castSucc, ⋯⟩) + fun i ↦ y ⟨t i.succ, ⋯⟩ - y ⟨t i.castSucc, ⋯⟩

Tactic:
by

Goal state after:
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✝ : NormedSpace ℝ E
this : IsProbabilityMeasure P
i : ι
s : Finset ι
hi : i ∉ s
hs :
  (∀ i ∈ s, AEMeasurable (X i) P) →
    iIndepFun (s.restrict X) P → charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)
mX : ∀ i_1 ∈ insert i s, AEMeasurable (X i_1) P
hX : iIndepFun ((insert i s).restrict X) P
⊢ ⟨i, ⋯⟩ ∉ {x | ↑x ∈ s}

Tactic:
by

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

Goal state after:
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
⊢ HasGaussianLaw (fun ω i ↦ X (t i.succ) ω - X (t i.castSucc) ω) P

Tactic:
by

Goal state after:
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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
h_iUnion : Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
this :
  ∫⁻ (x : E) in closedBall 0 (t 0) ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n),
      ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t 0), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ +
      ∑' (i : ℕ), ∫⁻ (x : E) in closedBall 0 (t (i + 1)) \ closedBall 0 (t i), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
n : ℕ
⊢ 1 - μ {x | ‖x‖ ≤ a} < ∞

Tactic:
by

Goal state after:
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✝ : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
⊢ charFunDual (Measure.map (∑ i ∈ s, X i) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
X : ι → Ω → E
inst✝¹ : Fintype ι
inst✝ : NormedSpace ℝ E
mX : ∀ (i : ι), AEMeasurable (X i) P
hX : iIndepFun X P
⊢ ∀ i ∈ univ, AEMeasurable (X i) P

Tactic:
by

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

Goal state after:
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✝ : NormedSpace ℝ E
mX : ∀ i ∈ s, AEMeasurable (X i) P
hX : iIndepFun (s.restrict X) P
⊢ charFunDual (Measure.map (fun ω ↦ ∑ i ∈ s, X i ω) P) = ∏ i ∈ s, charFunDual (Measure.map (X i) P)

Tactic:
by

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

Goal state after:
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✝¹ : NormedSpace ℝ E
μ : ι → Measure E
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μ i)
⊢ charFunDual (Measure.map (fun p ↦ ∑ i, p i) (Measure.pi μ)) = ∏ i, charFunDual (μ i)

Tactic:
by

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

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
E : Type u_3
inst✝⁵ : MeasurableSpace E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : BorelSpace E
inst✝² : SecondCountableTopology E
X : ι → Ω → E
inst✝¹ : Fintype ι
inst✝ : InnerProductSpace ℝ E
mX : ∀ (i : ι), AEMeasurable (X i) P
hX : iIndepFun X P
⊢ ∀ i ∈ univ, AEMeasurable (X i) P

Tactic:
by

Goal state after:
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 (fun ω ↦ ∑ i ∈ s, X i ω) P) = ∏ i ∈ s, charFun (Measure.map (X i) P)

Tactic:
by

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

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝ : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ AEMeasurable (toLp 2) (Measure.map (fun ω i ↦ X i ω) P)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝ : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ AEMeasurable (fun ω i ↦ X i ω) P

Tactic:
by

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

Goal state after:
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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
⊢ ∫⁻ (x : E), ENNReal.ofReal (rexp (logRatio c' * a⁻¹ ^ 2 * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} *
      (ENNReal.ofReal (rexp (logRatio c')) +
        ∑' (n : ℕ), ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c' / (1 - c')).toReal * 2 ^ n)))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁶ : Fintype ι
inst✝⁵ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : ∀ (i : ι), CompleteSpace (E i)
inst✝² : ∀ (i : ι), BorelSpace (E i)
inst✝¹ : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝ : (i : ι) → InnerProductSpace ℝ (E i)
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (t : WithLp 2 ((x : ι) → E x)),
      charFun (Measure.map (fun ω ↦ toLp 2 fun x ↦ X x ω) P) t = ∏ i, charFun (Measure.map (X i) P) (t.ofLp i)

Tactic:
by

Goal state after:
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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
h_neg : a < 0
⊢ {x | ‖x‖ ≤ a} = ∅

Tactic:
by

Goal state after:
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
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
⊢ 0 ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (L : StrongDual ℝ ((x : ι) → E x)),
      charFunDual (Measure.map (fun ω x ↦ X x ω) P) L =
        ∏ i, charFunDual (Measure.map (X i) P) (L ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
by

Goal state after:
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
h : ∀ (s : S), ∃ I L, ∀ (ω : Ω), Y s ω = L (I.restrict fun x ↦ X x ω)
I : Finset S
⊢ HasGaussianLaw (fun ω ↦ I.restrict fun x ↦ Y x ω) P

Tactic:
by

Goal state after:
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
h : IsGaussianProcess X P
f : S → T
s : S
x : ↥{f s} → E
⊢ f s ∈ {f s}

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst✝⁸ : Fact (1 ≤ p)
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ AEMeasurable (toLp p) (Measure.map (fun ω i ↦ X i ω) P)

Tactic:
by

Goal state after:
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
h : IsGaussianProcess X P
f : S → T
s : S
⊢ ∀ (x y : ↥{f s} → E), (x + y) ⟨f s, ⋯⟩ = x ⟨f s, ⋯⟩ + y ⟨f s, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst✝⁸ : Fact (1 ≤ p)
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ AEMeasurable (fun ω i ↦ X i ω) P

Tactic:
by

Goal state after:
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
h : IsGaussianProcess X P
f : S → T
s : S
⊢ ∀ (m : ℝ) (x : ↥{f s} → E), (m • x) ⟨f s, ⋯⟩ = (RingHom.id ℝ) m • x ⟨f s, ⋯⟩

Tactic:
by

Goal state after:
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
h : IsGaussianProcess X P
f : S → T
s : S
⊢ ∀ (ω : Ω),
    (X ∘ f) s ω =
      { toFun := fun x ↦ x ⟨f s, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ({f s}.restrict fun x ↦ X x ω)

Tactic:
by

Goal state after:
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
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
L : T → E →L[ℝ] F
h : IsGaussianProcess X P
t : T
x : ↥{t} → E
⊢ t ∈ {t}

Tactic:
by

Goal state after:
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
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
L : T → E →L[ℝ] F
h : IsGaussianProcess X P
t : T
⊢ ∀ (x y : ↥{t} → E), (L t) ((x + y) ⟨t, ⋯⟩) = (L t) (x ⟨t, ⋯⟩) + (L t) (y ⟨t, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Independence.CharacteristicFunction

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
p : ℝ≥0∞
inst✝⁸ : Fact (1 ≤ p)
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : IsProbabilityMeasure P
E : ι → Type u_3
mE : (i : ι) → MeasurableSpace (E i)
inst✝⁵ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁴ : ∀ (i : ι), CompleteSpace (E i)
inst✝³ : ∀ (i : ι), BorelSpace (E i)
inst✝² : ∀ (i : ι), SecondCountableTopology (E i)
X : (i : ι) → Ω → E i
inst✝¹ : (i : ι) → NormedSpace ℝ (E i)
inst✝ : DecidableEq ι
hX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun X P ↔
    ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))),
      charFunDual (Measure.map (fun ω ↦ toLp p fun x ↦ X x ω) P) L =
        ∏ i,
          charFunDual (Measure.map (X i) P)
            (L ∘SL ↑(PiLp.continuousLinearEquiv p ℝ E).symm ∘SL ContinuousLinearMap.single ℝ E i)

Tactic:
by

Goal state after:
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
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
L : T → E →L[ℝ] F
h : IsGaussianProcess X P
t : T
⊢ ∀ (m : ℝ) (x : ↥{t} → E), (L t) ((m • x) ⟨t, ⋯⟩) = (RingHom.id ℝ) m • (L t) (x ⟨t, ⋯⟩)

Tactic:
by

Goal state after:
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
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
L : T → E →L[ℝ] F
h : IsGaussianProcess X P
t : T
⊢ ∀ (ω : Ω),
    (L t) (X t ω) =
      { toFun := fun x ↦ (L t) (x ⟨t, ⋯⟩), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ } ({t}.restrict fun x ↦ X x ω)

Tactic:
by

Goal state after:
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
inst✝ : Add T
h : IsGaussianProcess X P
t₀ t : T
x : ↥{t₀, t₀ + t} → E
⊢ t₀ + t ∈ {t₀, t₀ + t}

Tactic:
by

Goal state after:
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
inst✝ : Add T
h : IsGaussianProcess X P
t₀ t : T
x : ↥{t₀, t₀ + t} → E
⊢ t₀ ∈ {t₀, t₀ + t}

Tactic:
by

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 α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝¹ : (i : S) → MeasurableSpace (𝓧 i)
inst✝ : MeasurableSpace 𝓨
X X' : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
h1 : IndepFun (fun ω i ↦ X i ω) Y κ P
h2 : ∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i
t : Set 𝓨
ht : MeasurableSet t
I : Set S
u : Set ((i : ↑I) → 𝓧 ↑i)
hI : I.Countable
hs : MeasurableSet (I.domRestrict ⁻¹' u)
this :
  ∀ᵐ (a : α) ∂P, (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u ∩ Y ⁻¹' t) = (κ a) ((fun ω i ↦ X (↑i) ω) ⁻¹' u) * (κ a) (Y ⁻¹' t)
aux : ∀ (f : (i : S) → Ω → 𝓧 i), True
x✝ : Countable ↑I
a : α
ha : ∀ (i : ↑I), ∀ᵐ (ω : Ω) ∂κ a, X (↑i) ω = X' (↑i) ω
ω : Ω
hω : ∀ (i : ↑I), X (↑i) ω = X' (↑i) ω
⊢ (fun i ↦ X (↑i) ω) = fun i ↦ X' (↑i) ω

Tactic:
by

Goal state after: