mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), Measurable (X i)
h_indep : iIndepFun X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
⊢ ∀ (i : ι), AEMeasurable (X i) μ

Tactic:
by fun_prop

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

Goal state before:
pp: case coe
Ω : Type u_1
β : Type u_2
u : ℕ → Ω → β
τ : Ω → ℕ∞
inst✝ : AddCommMonoid β
n : ℕ
x ω : Ω
t : ℕ
⊢ ↑n + 1 ≤ ↑t ↔ ↑n < ↑t

Tactic:
simp only [Nat.cast_lt]
          norm_cast

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : RCLike 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace E
inst✝⁵ : CompleteSpace F
inst✝⁴ : MeasurableSpace E
μ : Measure E
inst✝³ : OpensMeasurableSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ AEMeasurable (⇑L) μ

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : RCLike 𝕜
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : NormedSpace ℝ F
inst✝⁶ : CompleteSpace E
inst✝⁵ : CompleteSpace F
inst✝⁴ : MeasurableSpace E
μ : Measure E
inst✝³ : OpensMeasurableSpace E
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
inst✝ : SecondCountableTopology F
h : Integrable id μ
L : E →L[𝕜] F
⊢ AEStronglyMeasurable (fun x ↦ x) (Measure.map (⇑L) μ)

Tactic:
by fun_prop

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
h : ¬Integrable (fun ω ↦ rexp (z.re * X ω)) μ
⊢ AEStronglyMeasurable (fun ω ↦ cexp (z * ↑(X ω))) μ

Tactic:
by fun_prop

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (ω : Ω), cexp (z * ↑(X ω)) ∂μ‖ ≤ mgf X μ z.re

Tactic:
← re_add_im z

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ ‖∫ (ω : Ω), cexp ((↑z.re + ↑z.im * I) * ↑(X ω)) ∂μ‖ ≤ mgf X μ (↑z.re + ↑z.im * I).re
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: x t p : ℝ
hp : 0 ≤ p
ht : 0 < t
hp_zero : ¬p = 0
h_x_le : ∀ (c : ℝ), 0 < c → x ≤ c⁻¹ * rexp (c * x)
h_neg_x_le : ∀ (c : ℝ), 0 < c → -x ≤ c⁻¹ * rexp (-c * x)
h_abs_le : ∀ (c : ℝ), 0 < c → |x| ≤ c⁻¹ * max (rexp (c * x)) (rexp (-c * x))
⊢ |x| ^ p ≤ ((t / p)⁻¹ * max (rexp (t / p * x)) (rexp (-t / p * x))) ^ p

Tactic:
gcongr
    convert! h_abs_le (t / p) (div_pos ht (hp.lt_of_ne' hp_zero)) using 5
    rw [neg_div]

Goal state after:
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1) ω ≤ (∑ k ∈ Finset.range (n + 1), (s (k + 1)).indicator 1) ω

Tactic:
← sub_nonneg,

Goal state after:
case refine_1
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
s : ℕ → Set Ω
hs : ∀ (n : ℕ), MeasurableSet (s n)
ω : Ω
n : ℕ
⊢ 0 ≤ (∑ k ∈ Finset.range (n + 1), (s (k + 1)).indicator 1) ω - (∑ k ∈ Finset.range n, (s (k + 1)).indicator 1) ω
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z✝ : ℂ
hz : z✝.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z✝.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z✝.re - l) (u - z✝.re) / 2
h_pos : 0 < min (z✝.re - l) (u - z✝.re)
ht : 0 < t
z : ℂ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω) ^ n * cexp (z * ↑(X ω))) μ

Tactic:
by fun_prop

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

Goal state before:
pp: case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ max (rexp (|t| * x)) (rexp (-|t| * x)) = rexp (|t| * |x|)

Tactic:
rw [abs_of_nonneg hx]
      simp only [neg_mul, sup_eq_left, exp_le_exp, neg_le_self_iff]
      positivity

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case refine_2
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) = rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))

Tactic:
congr 1

Goal state after:
case refine_2
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ -(c⁻¹ * x - μ) ^ 2 / (2 * ↑v) = -(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v))
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: ⊢ Measurable fun x ↦ gaussianPDFReal x.1 x.2.1 x.2.2

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Measure.dirac μ = Measure.dirac μ + 0

Tactic:
add_zero

Goal state after:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Measure.dirac μ = Measure.dirac μ
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / mgf X μ v ^ 2 -
      ((∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) / mgf X μ v ^ 2 =
    deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - deriv (cgf X μ) v ^ 2

Tactic:
congr 1

Goal state after:
case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / mgf X μ v ^ 2 =
    deriv (fun u ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v

case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ (∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ ∫ (x : Ω), (fun ω ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ ((∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) / mgf X μ v ^ 2 = deriv (cgf X μ) v ^ 2
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: ⊢ Measurable fun x ↦ Measure.dirac x.1

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: ⊢ Measurable fun x ↦ ℙ.withDensity (gaussianPDF x.1 x.2)

Tactic:
by fun_prop

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z

Tactic:
have h := hasDerivAt_complexMGF hz

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z ∈ {z | z.re ∈ interior (integrableExpSet X μ)}
h : HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun ω ↦ ↑(X ω) * cexp (z * ↑(X ω))) x ∂μ) z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} z
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
y : ℝ
this : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x
⊢ Measurable fun x ↦ y + x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
y : ℝ
this : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x
⊢ Measurable fun x ↦ -x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
y : ℝ
⊢ AEMeasurable (fun x ↦ x + y) (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
y : ℝ
⊢ AEMeasurable (HAdd.hAdd y) (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
y : ℝ
⊢ AEMeasurable (fun x ↦ x - y) (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
c : ℝ
⊢ AEMeasurable (HMul.hMul c) (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
c : ℝ
⊢ AEMeasurable (fun x ↦ x * c) (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
⊢ AEMeasurable Neg.neg (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
c : ℝ
⊢ AEMeasurable (fun x ↦ x / c) (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
y : ℝ
⊢ AEMeasurable (HSub.hSub y) (gaussianReal μ v)

Tactic:
by fun_prop

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

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

Tactic:
congr 1

Goal state after:
case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ deriv (cgf X μ) v ^ 2 =
    (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v -
      deriv (cgf X μ) v ^ 2 * mgf X μ v / mgf X μ v
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case e_a.e_f
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
x : ℝ
⊢ cexp (-(↑x - ↑μ) ^ 2 / (2 * ↑↑v) + z * ↑x) = cexp (-(2 * ↑↑v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v))

Tactic:
congr 1

Goal state after:
case e_a.e_f
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
x : ℝ
⊢ -(↑x - ↑μ) ^ 2 / (2 * ↑↑v) + z * ↑x = -(2 * ↑↑v)⁻¹ * ↑x ^ 2 + (z + ↑μ / ↑↑v) * ↑x + -↑μ ^ 2 / (2 * ↑↑v)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ↑(√(2 * π * ↑v))⁻¹ * (↑π / - -↑↑(2 * v)⁻¹) ^ (1 / 2) *
      cexp (-↑μ ^ 2 / (2 * ↑↑v) - (z + ↑μ / ↑↑v) ^ 2 / (4 * -↑↑(2 * v)⁻¹)) =
    1 * cexp (-↑μ ^ 2 / (2 * ↑↑v) - (z + ↑μ / ↑↑v) ^ 2 / (4 * -↑↑(2 * v)⁻¹))

Tactic:
congr 1

Goal state after:
case e_a
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ↑(√(2 * π * ↑v))⁻¹ * (↑π / - -↑↑(2 * v)⁻¹) ^ (1 / 2) = 1
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ - (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        deriv (cgf X μ) v ^ 2 * mgf X μ v) /
      mgf X μ v =
    (∫ (ω : Ω), (X ω ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * rexp (v * X ω) ∂μ) / mgf X μ v

Tactic:
congr 1

Goal state after:
case e_a
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ ∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ - (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      deriv (cgf X μ) v ^ 2 * mgf X μ v =
    ∫ (ω : Ω), (X ω ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * rexp (v * X ω) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ cexp (-↑μ ^ 2 / (2 * ↑↑v) - (z + ↑μ / ↑↑v) ^ 2 / (4 * -↑↑(2 * v)⁻¹)) = cexp (z * ↑μ + ↑↑v * z ^ 2 / 2)

Tactic:
congr 1

Goal state after:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ -↑μ ^ 2 / (2 * ↑↑v) - (z + ↑μ / ↑↑v) ^ 2 / (4 * -↑↑(2 * v)⁻¹) = z * ↑μ + ↑↑v * z ^ 2 / 2
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : IsGaussian μ
this : (Measure.map (⇑0) μ) Set.univ = 1
⊢ Measurable ⇑0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hX_meas : AEMeasurable X p
⊢ ↑(mgf X p t) = ↑(rexp (μ * t + ↑v * t ^ 2 / 2))

Tactic:
← mgf_id_map hX_meas,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hX_meas : AEMeasurable X p
⊢ ↑(mgf id (Measure.map X p) t) = ↑(rexp (μ * t + ↑v * t ^ 2 / 2))
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
h :
  ∫ (ω : Ω), cexp (↑(Multiplicative.toAdd w) * ↑(X ω) * I) ∂μ =
    ∫ (ω : Ω'), cexp (↑(Multiplicative.toAdd w) * ↑(Y ω) * I) ∂μ'
⊢ AEStronglyMeasurable (fun v ↦ cexp (↑w * ↑v * I)) (Measure.map X μ)

Tactic:
by fun_prop

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
h :
  ∫ (ω : Ω), cexp (↑(Multiplicative.toAdd w) * ↑(X ω) * I) ∂μ =
    ∫ (ω : Ω'), cexp (↑(Multiplicative.toAdd w) * ↑(Y ω) * I) ∂μ'
⊢ AEStronglyMeasurable (fun v ↦ cexp (↑w * ↑v * I)) (Measure.map Y μ')

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
mF : MeasurableSpace F
inst✝¹ : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst✝ : IsGaussian μ
hL : Measurable ⇑L
L' : F →L[ℝ] ℝ
⊢ Measurable ⇑L'

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (fun t ↦ μ * t + ↑v * t ^ 2 / 2) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (HMul.hMul μ) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (fun t ↦ ↑v * t ^ 2 / 2) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (fun y ↦ μ) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (fun y ↦ y) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ AEMeasurable (fun x ↦ x - μ) (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ AEStronglyMeasurable (fun ω ↦ ω ^ 2) (Measure.map (fun x ↦ x - μ) (gaussianReal μ v))

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEStronglyMeasurable id (Measure.map (⇑L) μ)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEMeasurable (⇑L) μ

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
t : ℝ
⊢ DifferentiableAt ℝ (fun t ↦ ↑v * t ^ 2 / 2) t

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ DifferentiableAt ℝ (HMul.hMul ↑v) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ DifferentiableAt ℝ (fun t ↦ rexp (↑v * t ^ 2 / 2)) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ DifferentiableAt ℝ (fun y ↦ ↑v) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
L : E →L[ℝ] F
⊢ Measurable ⇑L

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ DifferentiableAt ℝ (fun y ↦ y) 0

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
μ : Measure E
L : E ≃L[ℝ] F
h : IsGaussian (Measure.map (⇑L) μ)
⊢ Measurable ⇑L.symm

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
μ : Measure E
L : E ≃L[ℝ] F
h : IsGaussian (Measure.map (⇑L) μ)
⊢ Measurable ⇑L

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ AEMeasurable (⇑L) (gaussianReal μ v)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ AEStronglyMeasurable (fun x ↦ x) (Measure.map (⇑L) (gaussianReal μ v))

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEStronglyMeasurable id (Measure.map (⇑L) μ)

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEMeasurable (⇑L) μ

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ AEMeasurable (fun x ↦ c + x) μ

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ AEStronglyMeasurable
    (fun z ↦
      ⟪x, z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ * ⟪y, z - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫)
    (Measure.map (fun x ↦ c + x) μ)

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ AEMeasurable (fun x ↦ c + x) μ

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
μ✝ : Measure E
inst✝³ : IsGaussian μ✝
inst✝² : SecondCountableTopology E
μ ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
L : StrongDual ℝ E
⊢ AEMeasurable (⇑L) (μ ∗ ν)

Tactic:
by fun_prop

Goal state after: