mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
this : (1 / 2) ^ n ≤ P (⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)})
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ (∫ (x : Ω), (fun ω ↦ rexp (t * X ω) ^ ↑p) x ∂κ ω') ^ (1 / ↑p) *
      (∫ (x : Ω), (fun ω ↦ rexp (t * Y ω) ^ ↑q) x ∂κ ω') ^ (1 / ↑q) ≤
    rexp (↑cX * (t * ↑p) ^ 2 / 2) ^ (1 / ↑p) * rexp (↑cY * (t * ↑q) ^ 2 / 2) ^ (1 / ↑q)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
M : MeasurableSet (Set.Ioc 0 A)
M' : MeasurableSet (Set.Ioc A 0)
hA : A < 0
this : ∀ᵐ (x : ℝ) ∂Measure.map f μ, 0 ≤ x
x : ℝ
hx : 0 ≤ x
a✝ : A < x
h''x : x ≤ 0
⊢ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
⊢ ∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in -A..A, y ∂Measure.map f μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
h'f : 0 ≤ f
⊢ ∫ (x : α), truncation f A x ∂μ = ∫ (y : ℝ) in 0..A, y ∂Measure.map f μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
h'f : 0 ≤ f
A : ℝ
⊢ ∫ (x : α), truncation f A x ∂μ ≤ ∫ (x : α), f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ rexp (↑cX * (t * ↑p) ^ 2 / 2) ^ (1 / ↑p) * rexp (↑cY * (t * ↑q) ^ 2 / 2) ^ (1 / ↑q) =
    rexp ((↑(NNReal.sqrt cX) + ↑(NNReal.sqrt cY)) ^ 2 * t ^ 2 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Tendsto (fun A ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
⊢ HasSubgaussianMGF (fun ω ↦ X ω + Y ω) ((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) κ ν

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ T, Tendsto T atTop atTop ∧ ∀ (n : ℕ), ∃ k, P {ω | σ n k ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n

Tactic:
by

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

Goal state before:
pp: x : ℕ → ℕ
n : ℕ
⊢ mkStrictMonoAux x n < mkStrictMonoAux x (n + 1)

Tactic:
by

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

Goal state before:
pp: x : ℕ → ℕ
⊢ x 0 ≤ mkStrictMonoAux x 0

Tactic:
by

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

Goal state before:
pp: x : ℕ → ℕ
n : ℕ
⊢ x (n + 1) ≤ mkStrictMonoAux x (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ = ∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ nk T, StrictMono nk ∧ Tendsto T atTop atTop ∧ ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
h2 : ∀ᵐ (ω' : Ω) ∂Measure.map Prod.snd (ν ⊗ₘ κ), ∀ (t : ℝ), mgf Y (η ω') t ≤ rexp (↑cY * t ^ 2 / 2)
⊢ AEMeasurable Prod.snd (ν ⊗ₘ κ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
⊢ HasSubgaussianMGF Y cY (prodMkLeft Ω' η) (ν ⊗ₘ κ)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
⊢ 1 / 2 < 1

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ j ∈ range K, ∑ i ∈ Ico j N, ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ =
    ∑ i ∈ range N, ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ i ∈ range N, ∑ j ∈ range (min (i + 1) K), ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ ≤
    ∑ i ∈ range N, (↑i + 1) * ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
⊢ ↑i ≤ ↑(i + 1)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
this : ∑' (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) ↑(T n)
hωτ : Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤)
⊢ ∀ᶠ (b : ℕ) in atTop, min (τ b ω) ((WithTop.some ∘ T) b) ≤ σ b (nk b) ω

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
this : ∑' (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) ↑(T n)
hωτ : Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤)
⊢ ∀ᶠ (b : ℕ) in atTop, σ b (nk b) ω ≤ min ⊤ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
h : MemLp (fun ω ↦ rexp (t * X ω)) 2 (⇑κ ∘ₘ ν)
⊢ ⇑κ ∘ₘ ν = Measure.map Prod.fst (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ nk, StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (τ i ω) (σ i (nk i) ω)) P

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ i ∈ range N, (↑i + 1) * ∫ (x : ℝ) in ↑i..↑(i + 1), 1 ∂ρ ≤ ∑ i ∈ range N, ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ i ∈ range N, ∫ (x : ℝ) in ↑i..↑(i + 1), x + 1 ∂ρ = ∫ (x : ℝ) in 0..↑N, x + 1 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (X ω.1 + Y ω.2))) (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∫ (x : ℝ) in 0..↑N, x + 1 ∂ρ = ∫ (x : ℝ) in 0..↑N, x ∂ρ + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∫ (x : ℝ) in 0..↑N, x ∂ρ + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ = (∫ (a : Ω), truncation X (↑N) a) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ (∫ (a : Ω), truncation X (↑N) a) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ (∫ (a : Ω), X a) + ∫ (x : ℝ) in 0..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
⊢ ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} = ∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ∑ j ∈ range K, ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
A : ∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ ≤ (∫ (a : Ω), X a) + 1
B : ∀ (a b : ℝ), ℙ {ω | X ω ∈ Set.Ioc a b} = ENNReal.ofReal (∫ (x : ℝ) in Set.Ioc a b, 1 ∂ρ)
⊢ ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in Set.Ioc ↑j ↑N, 1 ∂ρ) =
    ENNReal.ofReal (∑ j ∈ range K, ∫ (x : ℝ) in ↑j..↑N, 1 ∂ρ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ mgf (fun p ↦ X p.1 + Y p.2) ((κ ⊗ₖ η) ω') ↑q =
    ∫ (x : Ω), rexp (↑q * X x) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', x) ∂κ ω'

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
⊢ Tendsto (fun N ↦ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
ω : Ω
⊢ 0 ≤ rexp (↑q * X ω)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
⊢ ∑' (j : ℕ), ℙ {ω | X ω ∈ Set.Ioi ↑j} < ∞

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁸ : ConditionallyCompleteLinearOrderBot ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : IsFiniteMeasure P
inst✝³ : DenselyOrdered ι
inst✝² : NoMaxOrder ι
inst✝¹ : Zero E
inst✝ : 𝓕.IsRightContinuous
hp : IsStable 𝓕 p
⊢ Locally (fun Y ↦ Locally p 𝓕 Y P) 𝓕 X P ↔ Locally p 𝓕 X P

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
ω : Ω
x✝ : Ω''
⊢ 0 x✝ ≤ rexp (↑q * Y x✝)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
⊢ ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
⊢ MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ 1)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
x✝¹ x✝ : G
⊢ MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ (x✝¹ * x✝))) =
    MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ x✝¹)) *
      MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ x✝))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Action (Type w) G
g : G
x : X.V
⊢ ((linearize k G X) g) (MonoidAlgebra.single x 1) = MonoidAlgebra.single ((ConcreteCategory.hom (X.ρ g)) x) 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁵ : Monoid G
inst✝⁴ : Semiring k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AddCommGroup W
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
f : X ⟶ Y
g : G
⊢ MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom f.hom) ∘ₗ (linearize k G X) g =
    (linearize k G Y) g ∘ₗ MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom f.hom)

Tactic:
by

Goal state after: