awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
calc :
  Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
calc₁ :
  Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
    (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)
calc₂ :
  ∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v = iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0
calc₃ : iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0 = (↑v : ℝ)
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v = (↑v : ℝ)

Tactic:
calc ∫ ω, (ω - μ) ^ 2 ∂gaussianReal μ v
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal μ v).map (fun x ↦ x - μ) := by
    rw [integral_map (by fun_prop) (by fun_prop)]
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal 0 v) := by simp [gaussianReal_map_sub_const]
  _ = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 := by
    rw [iteratedDeriv_mgf_zero] <;> simp
  _ = v := by
    rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
    simp only [zero_mul, zero_add]
    have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) := by
      ext t
      rw [_root_.deriv_exp (by fun_prop)]
      simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
      ring
    rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
    simp

Premises used: HSub.hSub, ProbabilityTheory.gaussianReal, MeasureTheory.Measure.map, ProbabilityTheory.mgf, iteratedDeriv, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ Var[id; gaussianReal μ v] = (↑v : ℝ)

Tactic:
variance_fun_id_gaussianReal

Premises used: ProbabilityTheory.variance_fun_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v p : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet id (gaussianReal μ v))

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
p : ℝ≥0∞
hp : p ≠ ∞
⊢ p ≠ ∞

Tactic:
hp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
p : ℝ≥0∞
hp : p ≠ ∞
lift : ∀ (p : ℝ≥0), MemLp id (↑p : ℝ≥0∞) (gaussianReal μ v)
⊢ MemLp id p (gaussianReal μ v)

Tactic:
lift p to ℝ≥0 using hp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v p : ℝ≥0
⊢ MemLp id (↑p : ℝ≥0∞) (gaussianReal μ v)

Tactic:
memLp_id_gaussianReal p

Premises used: ProbabilityTheory.memLp_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v p : ℝ≥0
⊢ MemLp id (↑p : ℝ≥0∞) (gaussianReal μ v)

Tactic:
exact memLp_id_gaussianReal p

Premises used: ProbabilityTheory.memLp_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ₁ : ℝ
v₁ : ℝ≥0
⊢ gaussianReal μ₁ v₁ = gaussianReal μ₁ v₁

Tactic:
rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
refine : ∀ (h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂), μ₁ = μ₂ ∧ v₁ = v₂
⊢ gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂ ↔ μ₁ = μ₂ ∧ v₁ = v₂

Tactic:
refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
rw : Eq (α := ℝ) (∫ (x : ℝ), x ∂gaussianReal μ₂ v₂) (∫ (x : ℝ), x ∂gaussianReal μ₂ v₂) ∧ v₁ = v₂
⊢ μ₁ = μ₂ ∧ v₁ = v₂

Tactic:
rw [← integral_id_gaussianReal (μ := μ₁) (v := v₁),
    ← integral_id_gaussianReal (μ := μ₂) (v := v₂), h]

Premises used: ProbabilityTheory.integral_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
simp : v₁ = v₂
⊢ Eq (α := ℝ) (∫ (x : ℝ), x ∂gaussianReal μ₂ v₂) (∫ (x : ℝ), x ∂gaussianReal μ₂ v₂) ∧ v₁ = v₂

Tactic:
simp only [integral_id_gaussianReal, true_and]

Premises used: ProbabilityTheory.integral_id_gaussianReal, true_and
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
this : (↑v₁ : ℝ) = (↑v₂ : ℝ)
⊢ v₁ = v₂

Tactic:
simpa
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
suffices : (↑v₁ : ℝ) = (↑v₂ : ℝ)
⊢ v₁ = v₂

Tactic:
suffices (v₁ : ℝ) = v₂ by simpa
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
rw : Var[id; gaussianReal μ₁ v₁] = (↑v₂ : ℝ)
rw₁ : Var[id; gaussianReal μ₁ v₁] = Var[id; gaussianReal μ₂ v₂]
rw₂ rw₃ : Var[id; gaussianReal μ₂ v₂] = Var[id; gaussianReal μ₂ v₂]
⊢ (↑v₁ : ℝ) = (↑v₂ : ℝ)

Tactic:
rw [← variance_id_gaussianReal (μ := μ₁) (v := v₁),
    ← variance_id_gaussianReal (μ := μ₂) (v := v₂), h]

Premises used: ProbabilityTheory.variance_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x

Tactic:
have : (L : ℝ → ℝ) = fun x ↦ L 1 * x := by simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x
rw :
  gaussianReal (HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) μ)
      (NNReal.mk (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) ⋯ * v) =
    gaussianReal ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) μ)
      ((HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) 1) 2).toNNReal * v)
⊢ Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v) =
    gaussianReal ((L : (a : ℝ) → ℝ) μ) ((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v)

Tactic:
rw [this, gaussianReal_map_const_mul]

Premises used: ProbabilityTheory.gaussianReal_map_const_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x
e_v :
  HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2 =
    max (HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) 1) 2) 0
⊢ gaussianReal (HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) μ)
      (NNReal.mk (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) ⋯ * v) =
    gaussianReal ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) μ)
      ((HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) 1) 2).toNNReal * v)

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x
e_v : 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2 =
    max (HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) 1) 2) 0

Tactic:
simp only [mul_one, left_eq_sup]

Premises used: left_eq_sup, mul_one
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x
⊢ 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →L[ℝ] ℝ
⊢ Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v) =
    gaussianReal ((L : (a : ℝ) → ℝ) μ) ((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v)

Tactic:
gaussianReal_map_linearMap L

Premises used: ProbabilityTheory.gaussianReal_map_linearMap, ContinuousLinearMap.toLinearMap
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ AEMeasurable (β := ℝ) (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (x : ℝ) ↦ x)
    (Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
rw rw₁ :
  Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v)
⊢ Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v)) fun (x : ℝ) ↦ x)

Tactic:
rw [integral_map (φ := L) (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v)) fun (x : ℝ) ↦ x)

Tactic:
have : ∫ x, L x ∂(gaussianReal μ v) = ∫ x, x ∂((gaussianReal μ v).map L) := by
    rw [integral_map (φ := L) (by fun_prop) (by fun_prop)]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this :
  Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v)) fun (x : ℝ) ↦ x)
⊢ Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v : ℝ) ((L : (a : ℝ) → ℝ) μ : ℝ)

Tactic:
simp [this, gaussianReal_map_linearMap]

Premises used: ProbabilityTheory.gaussianReal_map_linearMap
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →L[ℝ] ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v : ℝ) ((L : (a : ℝ) → ℝ) μ : ℝ)

Tactic:
integral_linearMap_gaussianReal L

Premises used: ContinuousLinearMap.toLinearMap, ProbabilityTheory.integral_linearMap_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
rw :
  (↑((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v) : ℝ) =
    (↑(HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal : ℝ) * (↑v : ℝ)
rw₁ : AEMeasurable (β := ℝ) (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v)
⊢ Var[(⇑L : (a : ℝ) → ℝ); gaussianReal μ v] =
    (↑(HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal : ℝ) * (↑v : ℝ)

Tactic:
rw [← variance_id_map, gaussianReal_map_linearMap, variance_id_gaussianReal]

Premises used: ProbabilityTheory.gaussianReal_map_linearMap, ProbabilityTheory.variance_id_gaussianReal, ProbabilityTheory.variance_id_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ (↑((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v) : ℝ) =
    (↑(HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal : ℝ) * (↑v : ℝ)

Tactic:
simp only [NNReal.coe_mul, Real.coe_toNNReal']

Premises used: Real.coe_toNNReal', NNReal.coe_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →L[ℝ] ℝ
⊢ Var[(⇑L : (a : ℝ) → ℝ); gaussianReal μ v] =
    (↑(HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal : ℝ) * (↑v : ℝ)

Tactic:
variance_linearMap_gaussianReal L

Premises used: ContinuousLinearMap.toLinearMap, ProbabilityTheory.variance_linearMap_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂ = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
Measure.ext_of_charFun ?_

Premises used: MeasureTheory.Measure.ext_of_charFun
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
refine : charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂))
⊢ gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂ = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
refine Measure.ext_of_charFun ?_

Premises used: MeasureTheory.Measure.ext_of_charFun
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
h : ∀ (t : ℝ), charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) t = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂)) t
⊢ charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂))

Tactic:
ext t
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
h :
  cexp ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) *
      cexp ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) =
    cexp ((↑t : ℂ) * (↑(m₁ + m₂) : ℂ) * Complex.I - (↑(↑(v₁ + v₂) : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
⊢ charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) t = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂)) t

Tactic:
simp_rw [charFun_conv, charFun_gaussianReal]

Premises used: MeasureTheory.charFun_conv, ProbabilityTheory.charFun_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
h :
  cexp
      ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 +
        ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) =
    cexp ((↑t : ℂ) * (↑(m₁ + m₂) : ℂ) * Complex.I - (↑(↑(v₁ + v₂) : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
⊢ cexp ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) *
      cexp ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) =
    cexp ((↑t : ℂ) * (↑(m₁ + m₂) : ℂ) * Complex.I - (↑(↑(v₁ + v₂) : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)

Tactic:
rw [← Complex.exp_add]

Premises used: Complex.exp_add
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
h :
  cexp
      ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 +
        ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) =
    cexp
      ((↑t : ℂ) * ((↑m₁ : ℂ) + (↑m₂ : ℂ)) * Complex.I -
        ((↑(↑v₁ : ℝ) : ℂ) + (↑(↑v₂ : ℝ) : ℂ)) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
⊢ cexp
      ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 +
        ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) =
    cexp ((↑t : ℂ) * (↑(m₁ + m₂) : ℂ) * Complex.I - (↑(↑(v₁ + v₂) : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)

Tactic:
simp only [Complex.ofReal_add, NNReal.coe_add]

Premises used: NNReal.coe_add, Complex.ofReal_add
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ cexp
      ((↑t : ℂ) * (↑m₁ : ℂ) * Complex.I - (↑(↑v₁ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2 +
        ((↑t : ℂ) * (↑m₂ : ℂ) * Complex.I - (↑(↑v₂ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)) =
    cexp
      ((↑t : ℂ) * ((↑m₁ : ℂ) + (↑m₂ : ℂ)) * Complex.I -
        ((↑(↑v₁ : ℝ) : ℂ) + (↑(↑v₂ : ℝ) : ℂ)) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)

Tactic:
ring_nf
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
hf : AEMeasurable X P
hg : AEMeasurable Y P
σf : SigmaFinite (m0 := Real.measurableSpace) (Measure.map X P)
σg : SigmaFinite (m0 := Real.measurableSpace) (Measure.map Y P)
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]

Premises used: ProbabilityTheory.IndepFun.map_add_eq_map_conv_map₀', ProbabilityTheory.gaussianReal_conv_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
hf : Ne (α := Measure ℝ) (Measure.map X P) 0
⊢ AEMeasurable X P

Tactic:
apply AEMeasurable.of_map_ne_zero

Premises used: AEMeasurable.of_map_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Ne (α := Measure ℝ) (Measure.map X P) 0

Tactic:
simp [NeZero.ne, hX]

Premises used: NeZero.ne
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
hg : Ne (α := Measure ℝ) (Measure.map Y P) 0
⊢ AEMeasurable Y P

Tactic:
apply AEMeasurable.of_map_ne_zero

Premises used: AEMeasurable.of_map_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Ne (α := Measure ℝ) (Measure.map Y P) 0

Tactic:
simp [NeZero.ne, hY]

Premises used: NeZero.ne
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
σf : SigmaFinite (gaussianReal m₁ v₁)
⊢ SigmaFinite (m0 := Real.measurableSpace) (Measure.map X P)

Tactic:
rw [hX]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₁ v₁)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Premises used: MeasureTheory.IsFiniteMeasure.toSigmaFinite
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
σg : SigmaFinite (gaussianReal m₂ v₂)
⊢ SigmaFinite (m0 := Real.measurableSpace) (Measure.map Y P)

Tactic:
rw [hY]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₂ v₂)

Tactic:
apply IsFiniteMeasure.toSigmaFinite

Premises used: MeasureTheory.IsFiniteMeasure.toSigmaFinite
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
⊢ geometricMeasure p =
    Measure.sum fun (n : ℕ) ↦
      HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n)

Tactic:
if_pos hp

Premises used: if_pos, ProbabilityTheory.geometricMeasure
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
n : ℕ
⊢ 0 ≤ 1 - (↑p : ℝ)

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < 1 - (↑p : ℝ)

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < (↑p : ℝ)

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
n : ℕ
rw :
  (Measure.sum fun (n : ℕ) ↦
          HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n) :
        (a : Set ℕ) → ℝ≥0∞)
      {n} =
    ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))
rw₁ rw₂ : ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) = ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))
⊢ (geometricMeasure p : (a : Set ℕ) → ℝ≥0∞) {n} = ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))

Tactic:
rw [geometricMeasure_eq hp, Measure.sum_smul_dirac_singleton]

Premises used: MeasureTheory.Measure.sum_smul_dirac_singleton, ProbabilityTheory.geometricMeasure_eq
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
n : ℕ
rw : ENNReal.toReal ((geometricMeasure p : (a : Set ℕ) → ℝ≥0∞) {n}) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
rw₁ : (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))).toReal = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
rw₂ rw₃ : (1 - (↑p : ℝ)) ^ n * (↑p : ℝ) = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
⊢ (geometricMeasure p).real {n} = (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)

Tactic:
rw [measureReal_def, geometricMeasure_singleton hp,
    ENNReal.toReal_ofReal (geometricMeasure_nonneg p n)]

Premises used: ProbabilityTheory.geometricMeasure_singleton, ProbabilityTheory.geometricMeasure_nonneg, ENNReal.toReal_ofReal, MeasureTheory.measureReal_def
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
rw : 0 < (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)
⊢ 0 < (geometricMeasure p).real {n}

Tactic:
rw [geometricMeasure_real_singleton h1]

Premises used: ProbabilityTheory.geometricMeasure_real_singleton
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)

Tactic:
geometricMeasure_pos h1 h2 n

Premises used: ProbabilityTheory.geometricMeasure_pos
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)

Tactic:
exact geometricMeasure_pos h1 h2 n

Premises used: ProbabilityTheory.geometricMeasure_pos
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
⊢ 0 ≤ 1 - (↑p : ℝ)

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
⊢ 1 - (↑p : ℝ) < 1

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
h : 1 = (1 - (1 - (↑p : ℝ)))⁻¹ * (↑p : ℝ)
⊢ HasSum (α := ℝ) (fun (n : ℕ) ↦ (1 - (↑p : ℝ)) ^ n * (↑p : ℝ)) 1

Tactic:
convert! (hasSum_geometric_of_lt_one (r := 1 - p) (by grind) (by grind)).mul_right (p : ℝ)

Premises used: HasSum.mul_right, Subtype.val, hasSum_geometric_of_lt_one
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
hp : p ≠ 0
⊢ 1 = (1 - (1 - (↑p : ℝ)))⁻¹ * (↑p : ℝ)

Tactic:
grind
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
pos :
  ∀ (h : p ≠ 0),
    IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace)
      (Measure.sum fun (n : ℕ) ↦
        HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n))
neg : ∀ (h : ¬p ≠ 0), IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace) (Measure.dirac 0)
⊢ IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace)
    (if p ≠ 0 then
      Measure.sum fun (n : ℕ) ↦
        HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n)
    else Measure.dirac 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Distributions.Geometric
Goal:
p : (↑unitInterval : Type)
h : p ≠ 0
⊢ IsProbabilityMeasure (α := ℕ) (m0 := Nat.instMeasurableSpace)
    (Measure.sum fun (n : ℕ) ↦
      HSMul.hSMul (β := Measure ℕ) (ENNReal.ofReal ((1 - (↑p : ℝ)) ^ n * (↑p : ℝ))) (Measure.dirac n))

Tactic:
(hasSum_one_geometricMeasure h).isProbabilityMeasure_sum_dirac
      (geometricMeasure_nonneg p)

Premises used: ProbabilityTheory.geometricMeasure_nonneg, HasSum.isProbabilityMeasure_sum_dirac, ProbabilityTheory.hasSum_one_geometricMeasure