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)) μ)
⊢ ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.deterministic ⇑e ⋯ ∘ₖ (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))) ∘ₘ Measure.map k μ

Tactic:
]

Goal state after:
Ω : 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)) μ)
⊢ ⇑(Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ) ∘ₘ Measure.map k μ =
    ⇑(Kernel.deterministic ⇑e ⋯ ∘ₖ (Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ))) ∘ₘ Measure.map k μ
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
⊢ ∫ (x : Ω), (rexp (t * X x) / ∫ (x : Ω), rexp (t * X x) ∂μ) • g x ∂μ =
    ∫ (ω : Ω), (rexp (t * X ω) / ∫ (x : Ω), (fun ω ↦ rexp (t * X ω)) x ∂μ) • g ω ∂μ

Tactic:
]

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

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ = ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • g ω ∂μ

pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ

Tactic:
]

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ Integrable (fun ω ↦ rexp (t * X ω)) μ
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case e_f
Ω : 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)) μ)
⊢ Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ = Kernel.id ×ₖ condDistrib g k μ ×ₖ condDistrib f k μ

Tactic:
]

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

Goal state before:
pp: case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ ↑p ∂κ ω' < ∞

Tactic:
]

Goal state after:
case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ ↑p ∂κ ω' < ∞
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p).toReal ∂μ.tilted fun x ↦ t * X x) < ∞

pp: case neg.hp_ne_zero
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ ↑p ≠ 0

pp: case neg.hp_ne_top
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ ↑p ≠ ∞

Tactic:
]

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ‖X a‖ₑ ^ (↑p).toReal ∂μ.tilted fun x ↦ t * X x) < ∞

case neg.hp_ne_zero
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ ↑p ≠ 0

case neg.hp_ne_top
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ ↑p ≠ ∞
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X (μ.tilted fun x ↦ t * X x)

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AEMeasurable X (μ.tilted fun x ↦ t * X x)
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 κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp (↑p * t * X x)) ∂κ ω' < ∞
ω : Ω
⊢ ENNReal.ofReal (rexp (↑p * t * X ω)) = ENNReal.ofReal (rexp (↑p * t * X ω))

pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp (↑p * t * X x)) ∂κ ω' < ∞
ω : Ω
⊢ 0 ≤ ↑p

Tactic:
]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
hf : ∫⁻ (x : Ω), ENNReal.ofReal (rexp (↑p * t * X x)) ∂κ ω' < ∞
ω : Ω
⊢ 0 ≤ ↑p
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 μ)
⊢ ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ =
    ⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ

Tactic:
]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • (X ω - deriv (cgf X μ) t) ^ 2 ∂μ =
    ∫ (a : Ω), (X a - deriv (cgf X μ) t) ^ 2 * rexp (t * X a) / mgf X μ t ∂μ

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ ∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • (X ω - deriv (cgf X μ) t) ^ 2 ∂μ =
    ∫ (a : Ω), (X a - deriv (cgf X μ) t) ^ 2 * rexp (t * X a) / mgf X μ t ∂μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg.right
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p).toReal ∂⇑κ ∘ₘ ν < ∞

Tactic:
]

Goal state after:
case neg.right
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ (↑p).toReal ∂⇑κ ∘ₘ ν < ∞
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg.right
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ ↑p ∂⇑κ ∘ₘ ν < ∞

Tactic:
]

Goal state after:
case neg.right
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ ↑p ∂⇑κ ∘ₘ ν < ∞
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: case e'_2
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (∑ i ∈ Finset.range (n + 1),
      if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    ∑ m ∈ Finset.range (n + 1), p ^ m * (1 - p) ^ (n - m) * ↑(n.choose m)

Tactic:
]

Goal state after:
case e'_2
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (∑ i ∈ Finset.range (n + 1),
      if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    ∑ m ∈ Finset.range (n + 1), p ^ m * (1 - p) ^ (n - m) * ↑(n.choose m)
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: case e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i < n + 1
⊢ (if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)

Tactic:
]

Goal state after:
case e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i < n + 1
⊢ (if h : i < n + 1 then p ^ ↑⟨i, h⟩ * (1 - p) ^ (n - ↑⟨i, h⟩) * ↑(n.choose ↑⟨i, h⟩) else 0) =
    p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: case e'_2
p : ℝ≥0
h : p ≤ 1
n i : ℕ
hi : i < n + 1
⊢ p ^ ↑⟨i, hi⟩ * (1 - p) ^ (n - ↑⟨i, hi⟩) * ↑(n.choose ↑⟨i, hi⟩) = p ^ i * (1 - p) ^ (n - i) * ↑(n.choose i)

Tactic:
]

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

Goal state before:
pp: case e'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = 1

Tactic:
]

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 : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
ω : Ω
⊢ ENNReal.ofReal (rexp (↑p * t * X ω)) = ENNReal.ofReal (rexp (↑p * t * X ω))

pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
ω : Ω
⊢ 0 ≤ ↑p

Tactic:
]

Goal state after:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
p : ℝ≥0
hp0 : ¬p = 0
h' : ∫⁻ (a : Ω), ‖rexp (↑p * t * X a)‖ₑ ∂⇑κ ∘ₘ ν < ∞
ω : Ω
⊢ 0 ≤ ↑p
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 (fun ω ↦ (k ω, g ω, f ω)) μ = ⇑(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 μ) =
    Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)

Tactic:
]

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

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ ENNReal.ofReal ↑x ^ k * ENNReal.ofReal (1 - ↑x) ^ (b - k) * ↑(b.choose k) =
    ENNReal.ofReal ↑x ^ k * ENNReal.ofReal (1 - ↑x) ^ (b - k) * ↑(b.choose k)

pp: case hp
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ 0 ≤ 1 - ↑x

pp: case hp
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ 0 ≤ ↑x

pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ 0 ≤ ↑x ^ k

pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ 0 ≤ ↑x ^ k * (1 - ↑x) ^ (b - k)

Tactic:
]

Goal state after:
case hp
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ 0 ≤ 1 - ↑x

case hp
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ 0 ≤ ↑x

k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ 0 ≤ ↑x ^ k

k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ 0 ≤ ↑x ^ k * (1 - ↑x) ^ (b - k)
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 (⇑e.symm)
      (Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ)) =
    Measure.map (⇑e.symm)
      (Measure.map (⇑e) (⇑(Kernel.id ×ₖ (condDistrib g k μ ×ₖ condDistrib f k μ)) ∘ₘ Measure.map k μ))

Tactic:
]

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 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h_int : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
⊢ ↑c * t ^ 2 / 2 ≤ ↑c * t ^ 2 / 2

Tactic:
]

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 : α), f a ∂p.toMeasure

Tactic:
]

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
⊢ Integrable f p.toMeasure

Tactic:
]

Goal state after:
α : 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
⊢ Integrable f p.toMeasure
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
⊢ ∑ x, p.toMeasure.real {x} • f x = ∑ a, (p a).toReal • f a

Tactic:
]

Goal state after:
α : 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
⊢ ∑ x, p.toMeasure.real {x} • f x = ∑ a, (p a).toReal • f a
Module: Mathlib.Probability.ProbabilityMassFunction.Integrals

Goal state before:
pp: case e_f
α : 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
x : α
⊢ (p.toMeasure {x}).toReal • f x = (p x).toReal • f x

Tactic:
]

Goal state after:
case e_f
α : 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
x : α
⊢ (p.toMeasure {x}).toReal • f x = (p x).toReal • f x
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).toReal ≤ 1

Tactic:
]

Goal state after:
Ω : 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).toReal ≤ 1
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:
]

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