mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g 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
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : Ω → E
s : Set Ω
inst✝ : SFinite 0
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (∫ (x : Ω) in s, g x ∂Measure.tilted 0 fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X 0 t) • g x ∂0

pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
g : Ω → E
s : Set Ω
inst✝ : SFinite 0
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (∫ (x : Ω) in s, g x ∂Measure.tilted 0 fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X 0 t) • g x ∂0
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
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g 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
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ (∫ (x : Ω) in s, g x ∂μ.tilted fun x ↦ t * X x) = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (∫ (ω : Ω), g ω ∂Measure.tilted 0 fun x ↦ t * X x) = ∫ (ω : Ω), rexp (t * X ω - cgf X 0 t) • g ω ∂0

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 μ
⊢ (∫ (ω : Ω), g ω ∂μ.tilted fun x ↦ t * X x) = ∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ

Tactic:
·

Goal state after:
case inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
ht : Integrable (fun ω ↦ rexp (t * X ω)) 0
⊢ (∫ (ω : Ω), g ω ∂Measure.tilted 0 fun x ↦ t * X x) = ∫ (ω : Ω), rexp (t * X ω - cgf X 0 t) • g ω ∂0
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 μ
⊢ (∫ (ω : Ω), g ω ∂μ.tilted fun x ↦ t * X x) = ∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ

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 μ
⊢ (∫ (ω : Ω), g ω ∂μ.tilted fun x ↦ t * X x) = ∫ (ω : Ω), rexp (t * X ω - cgf X μ t) • g ω ∂μ
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case left
Ω : 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 : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) (κ ω')

pp: case right
Ω : 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 : ℝ
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞

Tactic:
·

Goal state after:
case left
Ω : 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 : ℝ
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) (κ ω')
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case right
Ω : 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 : ℝ
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞

Tactic:
·

Goal state after:
case right
Ω : 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 : ℝ
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : 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
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞

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
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞

Tactic:
·

Goal state after:
case pos
Ω : 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
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case hf
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ Integrable (fun x ↦ A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) x + f 0 * ∏ x_1, (g x_1) (X x_1 x)) P

pp: case hg
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ Integrable (A.indicator fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) P

Tactic:
·

Goal state after:
case hf
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ Integrable (fun x ↦ A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) x + f 0 * ∏ x_1, (g x_1) (X x_1 x)) P
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : p = 0
⊢ MemLp X (↑p) (μ.tilted fun x ↦ t * X x)

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

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : p = 0
⊢ MemLp X (↑p) (μ.tilted fun x ↦ t * X x)
Module: Mathlib.Probability.Independence.BoundedContinuousFunction

Goal state before:
pp: case hg
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ Integrable (A.indicator fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) P

Tactic:
·

Goal state after:
case hg
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : Fintype S
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : (s : S) → E s →ᵇ ℝ), ∫ (ω : Ω) in A, ∏ s, (f s) (X s ω) ∂P = P.real A * ∫ (ω : Ω), ∏ s, (f s) (X s ω) ∂P
f : ℝ →ᵇ ℝ
g : (t : S) → E t →ᵇ ℝ
h1 :
  ∀ (ω : Ω),
    f (A.indicator 1 ω) * ∏ s, (g s) (X s ω) =
      A.indicator (fun ω ↦ f 1 * ∏ s, (g s) (X s ω)) ω + f 0 * ∏ s, (g s) (X s ω) -
        A.indicator (fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) ω
h2 : ∀ (ω : Ω), f (A.indicator 1 ω) = A.indicator (fun x ↦ f 1) ω + Aᶜ.indicator (fun x ↦ f 0) ω
hg : ∀ {c : ℝ}, Integrable (fun ω ↦ c * ∏ s, (g s) (X s ω)) P
⊢ Integrable (A.indicator fun ω ↦ f 0 * ∏ s, (g s) (X s ω)) P
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
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 ≠ ∞

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) < ∞

Tactic:
·

Goal state after:
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
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
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 ≠ ∞

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) < ∞

Tactic:
·

Goal state after:
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 μ)
⊢ AEMeasurable X (μ.tilted fun x ↦ t * X x)

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

Tactic:
·

Goal state after:
Ω : 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: case pos
Ω : 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
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (⇑κ ∘ₘ ν)

pp: case neg
Ω : 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
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (⇑κ ∘ₘ ν)

Tactic:
·

Goal state after:
case pos
Ω : 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
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (⇑κ ∘ₘ ν)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg.left
Ω : 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
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)

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
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (⇑κ ∘ₘ ν) < ∞

Tactic:
·

Goal state after:
case neg.left
Ω : 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
⊢ AEStronglyMeasurable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ ν)
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
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑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
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (⇑κ ∘ₘ ν) < ∞
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

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

pp: case e'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = (p + (1 - p)) ^ n

Tactic:
·

Goal state after:
case e'_2
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ ∑ x, p ^ ↑x * (1 - p) ^ (n - ↑x) * ↑(n.choose ↑x) =
    ∑ 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'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = (p + (1 - p)) ^ n

Tactic:
·

Goal state after:
case e'_3
p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ 1 = (p + (1 - p)) ^ n
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case pos
Ω : 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 : ℝ
h0 : κ ω' = 0
⊢ log (mgf X (κ ω') t) ≤ log (rexp (↑c * t ^ 2 / 2))

pp: case neg
Ω : 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 : ℝ
h0 : ¬κ ω' = 0
⊢ log (mgf X (κ ω') t) ≤ log (rexp (↑c * t ^ 2 / 2))

Tactic:
·

Goal state after:
case pos
Ω : 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 : ℝ
h0 : κ ω' = 0
⊢ log (mgf X (κ ω') t) ≤ log (rexp (↑c * t ^ 2 / 2))
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hx
Ω : 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 : ℝ
h0 : ¬κ ω' = 0
⊢ 0 < mgf X (κ ω') t

pp: case hxy
Ω : 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 : ℝ
h0 : ¬κ ω' = 0
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
·

Goal state after:
case hx
Ω : 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 : ℝ
h0 : ¬κ ω' = 0
⊢ 0 < mgf X (κ ω') t
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case hxy
Ω : 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 : ℝ
h0 : ¬κ ω' = 0
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
·

Goal state after:
case hxy
Ω : 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 : ℝ
h0 : ¬κ ω' = 0
⊢ mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

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

pp: case mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (0 ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
·

Goal state after:
case integrable_exp_mul
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑0 ∘ₘ ν)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (0 ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
·

Goal state after:
case mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf X (0 ω') t ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF id c (κ.map X) ν
⊢ HasSubgaussianMGF X c κ ν

pp: case refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (⇑(κ.map X) ∘ₘ ν)

pp: case refine_3
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf id ((κ.map X) ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
·

Goal state after:
case refine_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF id c (κ.map X) ν
⊢ HasSubgaussianMGF X c κ ν
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (⇑(κ.map X) ∘ₘ ν)

pp: case refine_3
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf id ((κ.map X) ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
·

Goal state after:
case refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (⇑(κ.map X) ∘ₘ ν)