mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
e : γ × β' × β ≃ᵐ (γ × β') × β := MeasurableEquiv.prodAssoc.symm
h_eq :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ Kernel.prodMkRight β' (condDistrib f k μ)) ∘ₘ Measure.map (fun a ↦ (k a, g a)) μ
h1 : Measure.map (fun x ↦ ((k x, g x), f x)) μ = Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ)
h1_symm : Measure.map (fun a ↦ (k a, g a, f a)) μ = Measure.map (⇑e.symm) (Measure.map (fun x ↦ ((k x, g x), f x)) μ)
h2 :
  ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
h2_symm :
  ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    Measure.map (⇑e.symm) (⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ)
h :
  Measure.map (⇑e) (Measure.map (fun a ↦ (k a, g a, f a)) μ) =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)
⊢ Measure.map (fun ω ↦ (k ω, g ω, f ω)) μ = ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ

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
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), cgf X (κ ω') t ≤ ↑c * t ^ 2 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∫ (a : α), f a ∂p.toMeasure = ∫ (a : α) in p.support, f a ∂p.toMeasure

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∫ (a : α) in p.support, f a ∂p.toMeasure = ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
⊢ ∑' (a : ↑p.support), (p.toMeasure {↑a}).toReal • f ↑a = ∑' (a : ↑p.support), (p ↑a).toReal • f ↑a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁴ : MeasurableSpace α
inst✝³ : MeasurableSingletonClass α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
p : PMF α
f : α → E
hf : Integrable f p.toMeasure
x : α
h1 : x ∈ Function.support fun a ↦ (p a).toReal
h2 : p x = 0
⊢ (fun a ↦ (p a).toReal) x = 0

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
⊢ ∀ (t : T), X t =ᵐ[P] X t

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X Y : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
h : ∀ (t : T), X t =ᵐ[P] Y t
⊢ IsAEKolmogorovProcess Y P p q M

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsKolmogorovProcess X P p q M
s t : T
⊢ StronglyMeasurable fun ω ↦ edist (X s ω) (X t ω)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: α : Type u_1
inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSingletonClass α
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Fintype α
p : PMF α
f : α → E
⊢ ∫ (a : α), f a ∂p.toMeasure = ∑ a, (p a).toReal • f a

Tactic:
by

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
⊢ ∫ (b : Bool), bif b then 1 else 0 ∂(bernoulli p h).toMeasure = ↑p

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
β : Type u_3
β' : Type u_4
mΩ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
f : Ω → β
g : Ω → β'
γ : Type u_5
mγ : MeasurableSpace γ
mβ : MeasurableSpace β
mβ' : MeasurableSpace β'
inst✝³ : StandardBorelSpace β
inst✝² : Nonempty β
inst✝¹ : StandardBorelSpace β'
inst✝ : Nonempty β'
hf : Measurable f
hg : Measurable g
k : Ω → γ
hk : Measurable k
⊢ g ⟂ᵢ[k, hk; μ] f ↔
    ⇑(condDistrib f (fun ω ↦ (k ω, g ω)) μ) =ᵐ[Measure.map (fun ω ↦ (k ω, g ω)) μ]
      ⇑(Kernel.prodMkRight β' (condDistrib f k μ))

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
ω : Ω
hω₁ : X s ω = IsAEKolmogorovProcess.mk X hX s ω
hω₂ : X t ω = IsAEKolmogorovProcess.mk X hX t ω
⊢ edist (X s ω) (X t ω) = edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω)

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
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, IsFiniteMeasure (κ ω')

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ AEStronglyMeasurable (fun ω ↦ edist (X s ω) (X t ω)) P

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hX : IsAEKolmogorovProcess X P p q M
s : T
⊢ AEMeasurable (X s) P

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' f μ
hf : ∀ (i : ι), Measurable (f i)
i✝ j✝ k l : ι
hik : i✝ ≠ k
hil : i✝ ≠ l
hjk : j✝ ≠ k
hjl : j✝ ≠ l
g : (i j : ι) → ((x : ↥{i, j}) → β ↑x) → β i × β j := fun i j v ↦ (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
i j : ι
⊢ Measurable (g i 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
h✝ : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : IsFiniteMeasure (κ ω')
h_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
this : (κ ω').real Set.univ ≤ 1
⊢ (κ ω') Set.univ ≤ 1

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝⁴ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
this : Measurable fun ω ↦ (X s ω, X t ω)
⊢ Measurable fun ω ↦ (X s ω, X t ω)

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
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, (κ ω') Set.univ ≤ 1

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
g : (i j : ι) → ((x : ↥{i, j}) → β ↑x) → β i × β j := fun i j v ↦ (v ⟨i, ⋯⟩, v ⟨j, ⋯⟩)
hg : ∀ (i j : ι), Measurable (g i j)
⊢ Disjoint {i, j} {k, l}

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝⁴ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
⊢ Measurable fun ω ↦ (X s ω, X t ω)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → Ω → β i
h_indep : iCondIndepFun m' hm' f μ
hf : ∀ (i : ι), Measurable (f i)
i j k l : ι
hik : i ≠ k
hil : i ≠ l
hjk : j ≠ k
hjl : j ≠ l
⊢ CondIndepFun m' hm' (fun a ↦ (f i a, f j a)) (fun a ↦ (f k a, f l a)) μ

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
this : (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ↑M * edist s t ^ q = 0

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
h : edist s t = 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
this : (fun ω ↦ edist (X s ω) (X t ω) ^ p) =ᵐ[P] 0
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ 0 * edist s t ^ q = 0

Tactic:
by

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

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0

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
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * 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 : Ω → ℝ
c : ℝ≥0
h_int✝¹ : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf✝ : ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℚ), mgf X (κ a) ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int✝ : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
ω' : Ω'
h_mgf : ∀ (i : ℚ), mgf X (κ ω') ↑i ≤ rexp (↑c * ↑i ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ Continuous fun b ↦ rexp (↑c * b ^ 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 : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
h_mgf : ∀ (q : ℚ), ∀ᵐ (ω' : Ω') ∂ν, mgf X (κ ω') ↑q ≤ rexp (↑c * ↑q ^ 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * 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 Ω' Ω
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsZeroOrMarkovKernel κ
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * 0)) (⇑κ ∘ₘ ν)

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 Ω' Ω
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsZeroOrMarkovKernel κ
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf (fun x ↦ 0) (κ ω') t ≤ rexp (↑0 * 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 Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ HasSubgaussianMGF X c 0 ν

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ 0)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂0, ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (-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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ω' : Ω'
hm : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
t : ℝ
⊢ mgf (-X) (κ ω') t ≤ rexp (↑c * 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf (-X) (κ ω') t ≤ rexp (↑c * 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 : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
t : ℝ
ω : Ω
hω : X ω = Y ω
⊢ rexp (t * Y ω) = rexp (t * 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 : Ω → ℝ
c : ℝ≥0
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * Y ω)) (⇑κ ∘ₘ ν)

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
Y : Ω → ℝ
h : HasSubgaussianMGF X c κ ν
h' : X =ᵐ[⇑κ ∘ₘ ν] Y
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑c * 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 Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
t : ℝ
h1 : Integrable (fun ω ↦ rexp (t * X ω)) (Measure.map Y (⇑κ ∘ₘ ν))
⊢ AEMeasurable Y (⇑κ ∘ₘ ν)

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 Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (X ∘ Y) ω)) (⇑κ ∘ₘ ν)

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 Ω'
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
κ : Kernel Ω' Ω''
Y : Ω'' → Ω
X : Ω → ℝ
hY : Measurable Y
h : HasSubgaussianMGF X c (κ.map Y) ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf (X ∘ Y) (κ ω') t ≤ rexp (↑c * 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 : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * id ω)) (Measure.map 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 : Ω → ℝ
c : ℝ≥0
hX : Measurable X
⊢ HasSubgaussianMGF id c (κ.map X) ν ↔ HasSubgaussianMGF X c κ ν

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
h : HasSubgaussianMGF X c κ ν
r t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * (r * 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
r : ℝ
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf (fun ω ↦ r * X ω) (κ ω') t ≤ rexp (↑(NNReal.mk (r ^ 2) ⋯ * c) * t ^ 2 / 2)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
𝓕 : Filtration ι mΩ
P : Measure Ω
n : ℕ
⊢ IsStoppingTime 𝓕 fun x ↦ ⊤

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
𝓕 : Filtration ι mΩ
P : Measure Ω
x✝³ : Ω
x✝² x✝¹ : ℕ
x✝ : x✝² ≤ x✝¹
⊢ (fun x ↦ ⊤) x✝² ≤ (fun x ↦ ⊤) x✝¹

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✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
⊢ ∀ᵐ (ω : Ω) ∂P, Tendsto (fun x ↦ (τ ⊓ σ) x ω) atTop (𝓝 ⊤)

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✝² : LinearOrder ι
𝓕 : Filtration ι mΩ
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
τ σ : ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : IsLocalizingSequence 𝓕 σ P
⊢ ∀ᵐ (ω : Ω) ∂P, Monotone fun x ↦ (τ ⊓ σ) x ω

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✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : Zero E
hp : p X
⊢ ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < (fun n x ↦ ⊤) n ω}.indicator (X i)) ((fun n x ↦ ⊤) 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
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h2 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
a✝ : IsFiniteMeasure (κ ω')
t : ℝ
ht : 0 ≤ t
⊢ rexp (-t * ε) * mgf X (κ ω') t ≤ rexp (-t * ε + ↑c * 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 : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * 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 : Ω → ℝ
c : ℝ≥0
h✝ : HasSubgaussianMGF X c κ ν
ε : ℝ
hε : 0 ≤ ε
hc0 : ¬c = 0
ω' : Ω'
h : ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)
⊢ 0 ≤ ε / ↑c

Tactic:
by

Goal state after: