mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
n : ℕ
t : Fin (n + 1) → T
ht : Monotone t
t' : ℕ → T := fun k ↦ t ⟨min n k, ⋯⟩
⊢ ∀ (j : ℕ), n ≤ j → t' j = t' n

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
h : ∀ (t : ℕ → T), Monotone t → EventuallyConst t atTop → iIndepFun (fun i ω ↦ X (t (i + 1)) ω - X (t i) ω) P
⊢ HasIndepIncrements X P

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
τ : ℕ → T :=
  fun x ↦
    match x with
    | 0 => r
    | 1 => s
    | x => t
x✝ : ℕ
⊢ ∀ ⦃b : ℕ⦄, x✝ ≤ b → τ x✝ ≤ τ b

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
τ : ℕ → T :=
  fun x ↦
    match x with
    | 0 => r
    | 1 => s
    | x => t
⊢ 0 ≠ 1

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
⊢ (X s - X r) ⟂ᵢ[P] X t - X s

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
ω : Ω
hω : X r ω = 0
⊢ (X s - X r) ω = X s ω

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : SubNegZeroMonoid E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
h : ∀ᵐ (ω : Ω) ∂P, X r ω = 0
⊢ X s ⟂ᵢ[P] X t - X s

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁶ : Preorder T
inst✝⁵ : MeasurableSpace E
F : Type u_4
G : Type u_5
inst✝⁴ : MeasurableSpace G
inst✝³ : FunLike F E G
inst✝² : AddGroup E
inst✝¹ : SubtractionMonoid G
inst✝ : AddMonoidHomClass F E G
f : F
hf : Measurable ⇑f
hX : HasIndepIncrements X P
⊢ HasIndepIncrements (fun t ω ↦ f (X t ω)) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
⊢ charFun (Measure.map (X + Y) P) = charFun (Measure.map X P) * charFun (Measure.map Y P)

Tactic:
by

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

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : InnerProductSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ charFun (Measure.map (fun p ↦ p.1 + p.2) (μ.prod ν)) = charFun μ * charFun ν

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝¹⁰ : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
mF : MeasurableSpace F
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : CompleteSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst✝² : InnerProductSpace ℝ E
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ AEMeasurable (toLp 2) (Measure.map (fun ω ↦ (X ω, Y ω)) P)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝¹⁰ : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
mF : MeasurableSpace F
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : CompleteSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst✝² : InnerProductSpace ℝ E
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ AEMeasurable (fun ω ↦ (X ω, Y ω)) P

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : ∀ (t : T), AEMeasurable (X t) P
⊢ IsProjectiveMeasureFamily fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X : (t : T) → Ω → 𝓧 t
P : Measure Ω
hX : AEMeasurable (fun ω x ↦ X x ω) P
⊢ IsProjectiveLimit (Measure.map (fun ω x ↦ X x ω) P) fun I ↦ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝¹⁰ : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
mF : MeasurableSpace F
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : CompleteSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst✝² : InnerProductSpace ℝ E
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (t : WithLp 2 (E × F)),
      charFun (Measure.map (fun ω ↦ toLp 2 (X ω, Y ω)) P) t =
        charFun (Measure.map X P) t.ofLp.1 * charFun (Measure.map Y P) t.ofLp.2

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P
I : Finset T
⊢ AEMeasurable I.restrict (Measure.map (fun ω x ↦ X x ω) P)

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P
I : Finset T
⊢ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map I.restrict (Measure.map (fun ω x ↦ X x ω) P)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : IsFiniteMeasure P
E : Type u_2
mE : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
X : Ω → E
inst✝ : NormedSpace ℝ E
Y : Ω → E
mX : AEMeasurable X P
mY : AEMeasurable Y P
hXY : X ⟂ᵢ[P] Y
⊢ charFunDual (Measure.map (X + Y) P) = charFunDual (Measure.map X P) * charFunDual (Measure.map Y P)

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P
I : Finset T
hX' : Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map I.restrict (Measure.map (fun ω x ↦ X x ω) P)
⊢ AEMeasurable I.restrict (Measure.map (fun ω x ↦ Y x ω) P)

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P
I : Finset T
hX' : Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map I.restrict (Measure.map (fun ω x ↦ X x ω) P)
⊢ Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P = Measure.map I.restrict (Measure.map (fun ω x ↦ Y x ω) P)

Tactic:
by

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

Goal state before:
pp: E : Type u_2
mE : MeasurableSpace E
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : BorelSpace E
inst✝³ : SecondCountableTopology E
inst✝² : NormedSpace ℝ E
μ ν : Measure E
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
⊢ charFunDual (Measure.map (fun p ↦ p.1 + p.2) (μ.prod ν)) = charFunDual μ * charFunDual ν

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝¹⁰ : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
mF : MeasurableSpace F
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : CompleteSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (L : StrongDual ℝ (E × F)),
      charFunDual (Measure.map (fun ω ↦ (X ω, Y ω)) P) L =
        charFunDual (Measure.map X P) (L ∘SL ContinuousLinearMap.inl ℝ E F) *
          charFunDual (Measure.map Y P) (L ∘SL ContinuousLinearMap.inr ℝ E F)

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)
inst✝¹⁰ : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
mF : MeasurableSpace F
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : CompleteSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ AEMeasurable (toLp p) (Measure.map (fun ω ↦ (X ω, Y ω)) P)

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)
inst✝¹⁰ : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
mF : MeasurableSpace F
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : CompleteSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ AEMeasurable (fun ω ↦ (X ω, Y ω)) 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 : ℕ
⊢ 0 < 2⁻¹

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)
inst✝¹⁰ : IsFiniteMeasure P
E : Type u_2
F : Type u_3
mE : MeasurableSpace E
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
mF : MeasurableSpace F
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : CompleteSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
X : Ω → E
Y : Ω → F
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace E
hX : AEMeasurable X P
hY : AEMeasurable Y P
⊢ X ⟂ᵢ[P] Y ↔
    ∀ (L : StrongDual ℝ (WithLp p (E × F))),
      charFunDual (Measure.map (fun ω ↦ toLp p (X ω, Y ω)) P) L =
        charFunDual (Measure.map X P)
            (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inl ℝ E F) *
          charFunDual (Measure.map Y P)
            (L ∘SL ↑(prodContinuousLinearEquiv p ℝ E F).symm ∘SL ContinuousLinearMap.inr ℝ E F)

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 : ℕ
⊢ c' < ∞

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P ↔
    ∀ (I : Finset T),
      Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
⊢ IdentDistrib (fun ω x ↦ X x ω) (fun ω x ↦ Y x ω) P P ↔
    ∀ (I : Finset T), IdentDistrib (fun ω ↦ I.restrict fun x ↦ X x ω) (fun ω ↦ I.restrict fun x ↦ Y x ω) P P

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
⊢ ∀ᵐ (ω : Ω) ∂P, ∀ (i : ↥I), X (↑i) ω = Y (↑i) ω

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
h : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
⊢ Measure.map (fun ω ↦ I.restrict fun x ↦ X x ω) P = Measure.map (fun ω ↦ I.restrict fun x ↦ Y x ω) P

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
𝓧 : T → Type u_3
mΩ : MeasurableSpace Ω
mα : (t : T) → MeasurableSpace (𝓧 t)
X Y : (t : T) → Ω → 𝓧 t
P : Measure Ω
inst✝ : IsFiniteMeasure P
hX : AEMeasurable (fun ω x ↦ X x ω) P
hY : AEMeasurable (fun ω x ↦ Y x ω) P
h : ∀ (t : T), X t =ᵐ[P] Y t
⊢ Measure.map (fun ω x ↦ X x ω) P = Measure.map (fun ω x ↦ Y x ω) P

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✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
hX : IsGaussianProcess X P
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 Y : T → Ω → E
inst✝³ : MeasurableSpace E
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
hX : IsGaussianProcess X P
hXY : ∀ (t : T), X t =ᵐ[P] Y t
I : Finset T
⊢ 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: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : NormedSpace ℝ E
hX : IsGaussianProcess X P
t : T
⊢ 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
hX : IsGaussianProcess X P
t : T
⊢ HasGaussianLaw (X t) P

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
s t : T
⊢ s ∈ {s, 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
hX : IsGaussianProcess X P
s t : T
⊢ t ∈ {s, 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
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw (fun ω ↦ (X s ω, X t ω)) P

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
I : Finset T
⊢ HasGaussianLaw (∑ i ∈ I, X i) P

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
I : Finset T
⊢ HasGaussianLaw (fun ω ↦ ∑ i ∈ I, X i ω) P

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
x : ↥(image t univ) → E
i : Fin n
⊢ t i.succ ∈ image t univ

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
x : ↥(image t univ) → E
i : Fin n
⊢ t i.castSucc ∈ image t univ

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
x✝ : ↥s
⊢ ∀ ⦃a₂ : ↥s⦄, (fun x ↦ ⟨↑x, ⋯⟩) x✝ = (fun x ↦ ⟨↑x, ⋯⟩) a₂ → x✝ = a₂

Tactic:
by

Goal state after: