awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ

Tactic:
have hfm : AEStronglyMeasurable (gaussianPDFReal μ v) volume := by fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v

Tactic:
have hf : 0 ≤ₐₛ gaussianPDFReal μ v := ae_of_all _ (gaussianPDFReal_nonneg μ v)
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
rw : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦ gaussianPDFReal μ v a) 1
⊢ (∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1

Tactic:
rw [← integral_eq_lintegral_of_nonneg_ae hf hfm]

Premises used: MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
simp :
  ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦
        rexp (-HPow.hPow (β := ℕ) (a - μ) 2 / (2 * (↑v : ℝ)))) =
    1
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦ gaussianPDFReal μ v a) 1

Tactic:
simp only [gaussianPDFReal,
    integral_const_mul]

Premises used: MeasureTheory.integral_const_mul, ProbabilityTheory.gaussianPDFReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
rw :
  ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))) =
    1
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦
        rexp (-HPow.hPow (β := ℕ) (a - μ) 2 / (2 * (↑v : ℝ)))) =
    1

Tactic:
rw [integral_sub_right_eq_self (μ := volume) (fun a ↦ rexp (-a ^ 2 / ((2 : ℝ) * v))) μ]

Premises used: HMul.hMul, HDiv.hDiv, Real.exp, HPow.hPow, OfNat.ofNat, NNReal.toReal, MeasureTheory.integral_sub_right_eq_self, Neg.neg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
simp :
  ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2))) =
    1
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))) =
    1

Tactic:
simp only [div_eq_inv_mul, mul_inv_rev,
    mul_neg]

Premises used: mul_inv_rev, div_eq_inv_mul, mul_neg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
simp_rw :
  ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-(↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2)) =
    1
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2))) =
    1

Tactic:
simp_rw [← neg_mul]

Premises used: neg_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
rw : √((2 * π * (↑v : ℝ))⁻¹ * (π / ((↑v : ℝ)⁻¹ * 2⁻¹))) = 1
hx : 0 ≤ (2 * π * (↑v : ℝ))⁻¹
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-(↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2)) =
    1

Tactic:
rw [neg_mul, integral_gaussian, ← Real.sqrt_inv, ← Real.sqrt_mul]

Premises used: Real.sqrt_inv, Real.sqrt_mul, integral_gaussian, neg_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
⊢ √((2 * π * (↑v : ℝ))⁻¹ * (π / ((↑v : ℝ)⁻¹ * 2⁻¹))) = 1

Tactic:
simp [field]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
⊢ 0 ≤ (2 * π * (↑v : ℝ))⁻¹

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1

Tactic:
have h := lintegral_gaussianPDFReal_eq_one μ hv
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1
⊢ ENNReal.ofReal (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x) =
    ENNReal.ofReal 1

Tactic:
rw [← ofReal_integral_eq_lintegral_ofReal (integrable_gaussianPDFReal _ _)
    (ae_of_all _ (gaussianPDFReal_nonneg _ _)), ← ENNReal.ofReal_one] at h

Premises used: ENNReal.ofReal_one, MeasureTheory.ae_of_all, MeasureTheory.ofReal_integral_eq_lintegral_ofReal, ProbabilityTheory.integrable_gaussianPDFReal, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h :
  ENNReal.ofReal (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x) =
    ENNReal.ofReal 1
rwa rwa₁ rwa₂ rwa₃ :
  ENNReal.ofReal (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x) =
    ENNReal.ofReal 1
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x) 1

Tactic:
rwa [← ENNReal.ofReal_eq_ofReal_iff (integral_nonneg (gaussianPDFReal_nonneg _ _)) zero_le_one]

Premises used: MeasureTheory.integral_nonneg, ENNReal.ofReal_eq_ofReal_iff, zero_le_one, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
x y : ℝ
rw rw₁ :
  (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - y - μ) 2 / (2 * (↑v : ℝ))) =
    (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - y - μ) 2 / (2 * (↑v : ℝ)))
⊢ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - y - μ) 2 / (2 * (↑v : ℝ))) =
    (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - (μ + y)) 2 / (2 * (↑v : ℝ)))

Tactic:
rw [sub_add_eq_sub_sub_swap]

Premises used: sub_add_eq_sub_sub_swap
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
x y : ℝ
rw : gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ + -y) v x
rw₁ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x - -y)
rw₂ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x + - -y)
rw₃ rw₄ : gaussianPDFReal μ v (x + y) = gaussianPDFReal μ v (x + y)
⊢ gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x

Tactic:
rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]

Premises used: sub_eq_add_neg, neg_neg, ProbabilityTheory.gaussianPDFReal_sub
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
simp :
  (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    |c| *
      ((√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
        rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ)))))
⊢ gaussianPDFReal μ v (c⁻¹ * x) = |c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x

Tactic:
simp only [gaussianPDFReal.eq_1, NNReal.zero_le_coe,
    Real.sqrt_mul', mul_inv_rev, NNReal.coe_mul, NNReal.coe_mk]

Premises used: NNReal.coe_mk, ProbabilityTheory.gaussianPDFReal.eq_1, NNReal.coe_mul, mul_inv_rev, NNReal.zero_le_coe, Real.sqrt_mul'
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
rw :
  (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
      rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))
⊢ (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    |c| *
      ((√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
        rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ)))))

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
      rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))

Tactic:
congr_arg₂ _ ?_ ?_

Premises used: congr_arg₂
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
refine_1 : (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹
refine_2 :
  rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))
⊢ (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ * rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹ *
      rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))

Tactic:
refine congr_arg₂ _ ?_ ?_

Premises used: congr_arg₂
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
refine_1 : √(HPow.hPow (β := ℕ) c 2) / √(↑v : ℝ) = |c| / √(↑v : ℝ)
⊢ (√(↑v : ℝ))⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))⁻¹

Tactic:
simp (disch := positivity) only [Real.sqrt_mul, mul_inv_rev, field]

Premises used: Real.sqrt_mul, mul_inv_rev
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
refine_1 refine_1₁ : |c| / √(↑v : ℝ) = |c| / √(↑v : ℝ)
⊢ √(HPow.hPow (β := ℕ) c 2) / √(↑v : ℝ) = |c| / √(↑v : ℝ)

Tactic:
rw [Real.sqrt_sq_eq_abs]

Premises used: Real.sqrt_sq_eq_abs
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
refine_2 :
  -HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ)) =
    -HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ)))
⊢ rexp (-HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ))) =
    rexp (-HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ))))

Tactic:
congr 1
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ -HPow.hPow (β := ℕ) (c⁻¹ * x - μ) 2 / (2 * (↑v : ℝ)) =
    -HPow.hPow (β := ℕ) (x - c * μ) 2 / (2 * (HPow.hPow (β := ℕ) c 2 * (↑v : ℝ)))

Tactic:
field
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
rw : |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v) x
| gaussianPDFReal μ v (c * x)

Tactic:
rw [← inv_inv c, gaussianPDFReal_inv_mul (inv_ne_zero hc)]

Premises used: ProbabilityTheory.gaussianPDFReal_inv_mul, inv_inv, inv_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
conv_lhs :
  |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v) x =
    |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2)⁻¹ ⋯ * v) x
⊢ gaussianPDFReal μ v (c * x) = |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2)⁻¹ ⋯ * v) x

Tactic:
conv_lhs => rw [← inv_inv c, gaussianPDFReal_inv_mul (inv_ne_zero hc)]

Premises used: ProbabilityTheory.gaussianPDFReal_inv_mul, inv_inv, inv_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v) x =
    |c⁻¹| * gaussianPDFReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2)⁻¹ ⋯ * v) x

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ gaussianPDF μ v = fun (x : ℝ) ↦ ENNReal.ofReal (gaussianPDFReal μ v x)

Tactic:
rfl

Premises used: ProbabilityTheory.gaussianPDF, rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
h : ∀ (x : ℝ), gaussianPDF μ 0 x = 0 x
⊢ gaussianPDF μ 0 = 0

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ x : ℝ
⊢ gaussianPDF μ 0 x = 0 x

Tactic:
simp [gaussianPDF]

Premises used: ProbabilityTheory.gaussianPDF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
x : ℝ
rw : (ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = gaussianPDFReal μ v x
rw₁ rw₂ : gaussianPDFReal μ v x = gaussianPDFReal μ v x
⊢ (gaussianPDF μ v x).toReal = gaussianPDFReal μ v x

Tactic:
rw [gaussianPDF, ENNReal.toReal_ofReal (gaussianPDFReal_nonneg μ v x)]

Premises used: ENNReal.toReal_ofReal, ProbabilityTheory.gaussianPDF, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
rw : 0 < gaussianPDFReal μ v x
⊢ 0 < gaussianPDF μ v x

Tactic:
rw [gaussianPDF, ENNReal.ofReal_pos]

Premises used: ENNReal.ofReal_pos, ProbabilityTheory.gaussianPDF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ 0 < gaussianPDFReal μ v x

Tactic:
gaussianPDFReal_pos _ _ _ hv

Premises used: ProbabilityTheory.gaussianPDFReal_pos
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ 0 < gaussianPDFReal μ v x

Tactic:
exact gaussianPDFReal_pos _ _ _ hv

Premises used: ProbabilityTheory.gaussianPDFReal_pos
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
x : ℝ
⊢ gaussianPDF μ v x < ∞

Tactic:
simp [gaussianPDF]

Premises used: ProbabilityTheory.gaussianPDF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
x : ℝ
⊢ gaussianPDF μ v x ≠ ∞

Tactic:
simp [gaussianPDF]

Premises used: ProbabilityTheory.gaussianPDF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
h : ∀ (x : ℝ), x ∈ Function.support (gaussianPDF μ v) ↔ Membership.mem (γ := Set ℝ) Set.univ x
⊢ Function.support (gaussianPDF μ v) = Set.univ

Tactic:
ext x
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
h : x ∈ Function.support (gaussianPDF μ v)
⊢ x ∈ Function.support (gaussianPDF μ v) ↔ Membership.mem (γ := Set ℝ) Set.univ x

Tactic:
simp only [Set.mem_univ, iff_true]

Premises used: iff_true, Set.mem_univ
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ x ∈ Function.support (gaussianPDF μ v)

Tactic:
(gaussianPDF_pos _ hv x).ne'

Premises used: Set.Mem, setOf, ProbabilityTheory.gaussianPDF_pos, LT.lt.ne', Function.support, Not
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ x ∈ Function.support (gaussianPDF μ v)

Tactic:
exact (gaussianPDF_pos _ hv x).ne'

Premises used: ProbabilityTheory.gaussianPDF_pos, LT.lt.ne'
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ Measurable (gaussianPDF μ v)

Tactic:
(measurable_gaussianPDFReal _ _).ennreal_ofReal

Premises used: Measurable.ennreal_ofReal, ProbabilityTheory.measurable_gaussianPDFReal, ProbabilityTheory.gaussianPDF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ ∫⁻ (x : ℝ), gaussianPDF μ v x = 1

Tactic:
lintegral_gaussianPDFReal_eq_one μ h

Premises used: ProbabilityTheory.lintegral_gaussianPDFReal_eq_one, ProbabilityTheory.gaussianPDF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ gaussianReal μ v = Measure.withDensity ℙ (gaussianPDF μ v)

Tactic:
if_neg hv

Premises used: ProbabilityTheory.gaussianReal, if_neg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
⊢ gaussianReal μ 0 = Measure.dirac μ

Tactic:
if_pos rfl

Premises used: ProbabilityTheory.gaussianReal, if_pos, rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
pos : ∀ (h : v = 0), Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
neg : ∀ (h : ¬v = 0), Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
by_cases h : v = 0
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v = 0
⊢ Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [gaussianReal_of_var_ne_zero, h]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : ¬v = 0
⊢ Eq (α := ℝ≥0∞) ((gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [gaussianReal_of_var_ne_zero, h]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
rw : NoAtoms (m0 := Real.measurableSpace) (Measure.withDensity ℙ (gaussianPDF μ v))
⊢ NoAtoms (gaussianReal μ v)

Tactic:
rw [gaussianReal_of_var_ne_zero _ h]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ NoAtoms (m0 := Real.measurableSpace) (Measure.withDensity ℙ (gaussianPDF μ v))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
rw : (Measure.withDensity ℙ (gaussianPDF μ v) : (a : Set ℝ) → ℝ≥0∞) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
rw₁ rw₂ : ∫⁻ (a : ℝ) in s, gaussianPDF μ v a = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x
⊢ (gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply' _ s]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero, MeasureTheory.withDensity_apply'
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
rw : ∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)
hfi : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (gaussianPDFReal μ v) (Measure.restrict ℙ s)
f_nn : 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict ℙ s)] gaussianPDFReal μ v
⊢ (gaussianReal μ v : (a : Set ℝ) → ℝ≥0∞) s =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s) fun (x : ℝ) ↦ gaussianPDFReal μ v x)

Tactic:
rw [gaussianReal_apply _ hv s, ofReal_integral_eq_lintegral_ofReal]

Premises used: ProbabilityTheory.gaussianReal_apply, MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ ∫⁻ (x : ℝ) in s, gaussianPDF μ v x = ∫⁻ (x : ℝ) in s, ENNReal.ofReal (gaussianPDFReal μ v x)

Tactic:
rfl
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (gaussianPDFReal μ v) (Measure.restrict ℙ s)

Tactic:
(integrable_gaussianPDFReal _ _).restrict

Premises used: MeasureTheory.Integrable.restrict, ProbabilityTheory.integrable_gaussianPDFReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (gaussianPDFReal μ v) (Measure.restrict ℙ s)

Tactic:
exact (integrable_gaussianPDFReal _ _).restrict

Premises used: MeasureTheory.Integrable.restrict, ProbabilityTheory.integrable_gaussianPDFReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict ℙ s)] gaussianPDFReal μ v

Tactic:
ae_of_all _ (gaussianPDFReal_nonneg _ _)

Premises used: MeasureTheory.ae_of_all, Filter.EventuallyLE, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ 0 ≤ᶠ[ae (F := Measure ℝ) (Measure.restrict ℙ s)] gaussianPDFReal μ v

Tactic:
exact ae_of_all _ (gaussianPDFReal_nonneg _ _)

Premises used: MeasureTheory.ae_of_all, ProbabilityTheory.gaussianPDFReal_nonneg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
rw : Measure.withDensity ℙ (gaussianPDF μ v) ≪ ℙ
⊢ gaussianReal μ v ≪ ℙ

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ Measure.withDensity ℙ (gaussianPDF μ v) ≪ ℙ

Tactic:
withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ Measure.withDensity ℙ (gaussianPDF μ v) ≪ ℙ

Tactic:
exact withDensity_absolutelyContinuous _ _

Premises used: MeasureTheory.withDensity_absolutelyContinuous
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
rw : ℙ ≪ Measure.withDensity ℙ (gaussianPDF μ v)
⊢ ℙ ≪ gaussianReal μ v

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv]

Premises used: ProbabilityTheory.gaussianReal_of_var_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ℙ ≪ Measure.withDensity ℙ (gaussianPDF μ v)

Tactic:
withDensity_absolutelyContinuous' ?_ ?_

Premises used: MeasureTheory.withDensity_absolutelyContinuous'
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
refine_1 : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) (gaussianPDF μ v) ℙ
refine_2 : ∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0
⊢ ℙ ≪ Measure.withDensity ℙ (gaussianPDF μ v)

Tactic:
refine withDensity_absolutelyContinuous' ?_ ?_

Premises used: MeasureTheory.withDensity_absolutelyContinuous'
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ AEMeasurable (_m := MeasureSpace.toMeasurableSpace) (gaussianPDF μ v) ℙ

Tactic:
(measurable_gaussianPDF _ _).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.measurable_gaussianPDF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ AEMeasurable (_m := MeasureSpace.toMeasurableSpace) (gaussianPDF μ v) ℙ

Tactic:
exact (measurable_gaussianPDF _ _).aemeasurable

Premises used: Measurable.aemeasurable, ProbabilityTheory.measurable_gaussianPDF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0

Tactic:
ae_of_all _ (fun _ ↦ (gaussianPDF_pos _ hv _).ne')

Premises used: ProbabilityTheory.gaussianPDF_pos, LT.lt.ne', MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ ∀ᵐ (x : ℝ), gaussianPDF μ v x ≠ 0

Tactic:
exact ae_of_all _ (fun _ ↦ (gaussianPDF_pos _ hv _).ne')

Premises used: ProbabilityTheory.gaussianPDF_pos, LT.lt.ne', MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
pos : ∀ (hv : v = 0), ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
neg : ∀ (hv : ¬v = 0), ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v
⊢ ∂gaussianReal μ v/∂ℙ =ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDF μ v

Tactic:
by_cases hv : v = 0