awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
neg :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |c⁻¹| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)

Tactic:
simp only [e, Homeomorph.mulLeft₀,
    Equiv.mulLeft₀_symm_apply, Homeomorph.toMeasurableEquiv_coe, Homeomorph.homeomorph_mk_coe_symm,
    gaussianPDFReal_inv_mul hc]

Premises used: Homeomorph.mulLeft₀, Equiv.mulLeft₀_symm_apply, ProbabilityTheory.gaussianPDFReal_inv_mul, Homeomorph.homeomorph_mk_coe_symm, Homeomorph.toMeasurableEquiv_coe
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
neg :
  ∀ (x : ℝ),
    |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x) =
      gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)

Tactic:
congr with x
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
this : |c⁻¹| * |c| = 1
rw :
  |c⁻¹| * |c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
rw₁ :
  1 * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
rw₂ rw₃ :
  gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x) =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x

Tactic:
rw [← mul_assoc, this, one_mul]

Premises used: mul_assoc, one_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
neg : |c⁻¹| * |c| = 1
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x) =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x

Tactic:
suffices |c⁻¹| * |c| = 1 by rw [← mul_assoc, this, one_mul]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
neg : |c| ≠ 0
⊢ |c⁻¹| * |c| = 1

Tactic:
rw [abs_inv, inv_mul_cancel₀]

Premises used: abs_inv, inv_mul_cancel₀
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
neg : ¬|c| = 0
neg₁ neg₂ neg₃ neg₄ : ¬c = 0
⊢ |c| ≠ 0

Tactic:
rwa [ne_eq, abs_eq_zero]

Premises used: ne_eq, abs_eq_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
simp_rw :
  Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
⊢ Measure.map (fun (x : ℝ) ↦ x * c) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)

Tactic:
simp_rw [mul_comm _ c]

Premises used: mul_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)

Tactic:
gaussianReal_map_const_mul c

Premises used: ProbabilityTheory.gaussianReal_map_const_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)

Tactic:
exact gaussianReal_map_const_mul c

Premises used: ProbabilityTheory.gaussianReal_map_const_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ Measure.map (fun (x : ℝ) ↦ -x) (gaussianReal μ v) = gaussianReal (-μ) v

Tactic:
simpa using gaussianReal_map_const_mul (μ := μ) (v := v) (-1)

Premises used: ProbabilityTheory.gaussianReal_map_const_mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ x * c⁻¹) (gaussianReal μ v) =
    gaussianReal (c⁻¹ * μ) (NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v)

Tactic:
gaussianReal_map_mul_const c⁻¹

Premises used: ProbabilityTheory.gaussianReal_map_mul_const, Inv.inv
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
h : μ * c⁻¹ = c⁻¹ * μ
h₁ : v * (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹ = NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v
⊢ Measure.map (fun (x : ℝ) ↦ x * c⁻¹) (gaussianReal μ v) =
    gaussianReal (μ * c⁻¹) (v * (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹)

Tactic:
convert! gaussianReal_map_mul_const c⁻¹ using 2

Premises used: ProbabilityTheory.gaussianReal_map_mul_const, Inv.inv
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
h h₁ : c⁻¹ * μ = c⁻¹ * μ
⊢ μ * c⁻¹ = c⁻¹ * μ

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
h : (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹ * v = NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v
⊢ v * (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹ = NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
h : (↑((NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹ * v) : ℝ) = (↑(NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v) : ℝ)
⊢ (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹ * v = NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ (↑((NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹ * v) : ℝ) = (↑(NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v) : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
h : ∀ (x : ℝ), y + -x = ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) x
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y x : ℝ
⊢ y + -x = ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) x

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)

Tactic:
have : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x := by ext; simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ y + x

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ -x

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
rw : Measure.map ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
rw₁ : Measure.map (fun (x : ℝ) ↦ y + x) (Measure.map (fun (x : ℝ) ↦ -x) (gaussianReal μ v)) = gaussianReal (y + -μ) v
rw₂ : Measure.map (fun (x : ℝ) ↦ y + x) (gaussianReal (-μ) v) = gaussianReal (y + -μ) v
rw₃ : gaussianReal (-μ + y) v = gaussianReal (y + -μ) v
rw₄ rw₅ : gaussianReal (y + -μ) v = gaussianReal (y + -μ) v
⊢ Measure.map (fun (x : ℝ) ↦ y + -x) (gaussianReal μ v) = gaussianReal (y + -μ) v

Tactic:
rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), gaussianReal_map_neg,
    gaussianReal_map_const_add, add_comm]

Premises used: ProbabilityTheory.gaussianReal_map_neg, add_comm, ProbabilityTheory.gaussianReal_map_const_add, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
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:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
y : ℝ
⊢ AEMeasurable (HAdd.hAdd y) (gaussianReal μ v)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
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:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
c : ℝ
⊢ AEMeasurable (HMul.hMul c) (gaussianReal μ v)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
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:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
⊢ AEMeasurable Neg.neg (gaussianReal μ v)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
⊢ HasLaw (Neg.neg ∘ X) (gaussianReal (-μ) v) P

Tactic:
exact HasLaw.comp ⟨by fun_prop, gaussianReal_map_neg⟩ hX

Premises used: ProbabilityTheory.gaussianReal_map_neg, ProbabilityTheory.HasLaw.mk, ProbabilityTheory.HasLaw.comp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
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:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
hX : HasLaw X (gaussianReal μ v) P
y : ℝ
⊢ AEMeasurable (HSub.hSub y) (gaussianReal μ v)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
pos :
  ∀ (hv : v = 0),
    complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
neg :
  ∀ (hv : ¬v = 0),
    complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : v = 0
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)

Tactic:
simp [complexMGF, hv]

Premises used: ProbabilityTheory.complexMGF
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
simp_rw :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x • cexp (z * (↑x : ℂ)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))
⊢ Eq (α := ℂ) (∫ (x : ℝ), cexp (z * (↑x : ℂ)) ∂gaussianReal μ v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))

Tactic:
simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]

Premises used: Complex.real_smul, ProbabilityTheory.integral_gaussianReal_eq_integral_smul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
push_cast :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑√(2 * π * (↑v : ℝ)) : ℂ)⁻¹ * cexp (-HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ))) *
        cexp (z * (↑x : ℂ))) =
    (↑√(2 * π * (↑v : ℝ)) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑((√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) : ℂ) * cexp (z * (↑x : ℂ))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))

Tactic:
push_cast
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
simp_rw :
  ((↑√(2 * (π * (↑v : ℝ))) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦
        cexp (-HPow.hPow (β := ℕ) ((↑a : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑a : ℂ))) =
    (↑√(2 * (π * (↑v : ℝ))) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑√(2 * π * (↑v : ℝ)) : ℂ)⁻¹ * cexp (-HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ))) *
        cexp (z * (↑x : ℂ))) =
    (↑√(2 * π * (↑v : ℝ)) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))

Tactic:
simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]

Premises used: MeasureTheory.integral_const_mul, Complex.exp_add, mul_assoc
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
e_a :
  ∀ (x : ℝ),
    cexp (-HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑x : ℂ)) =
      cexp
        (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
          -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
⊢ ((↑√(2 * (π * (↑v : ℝ))) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦
        cexp (-HPow.hPow (β := ℕ) ((↑a : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑a : ℂ))) =
    (↑√(2 * (π * (↑v : ℝ))) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))

Tactic:
congr with x
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
x : ℝ
e_a :
  -HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑x : ℂ) =
    -(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
      -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ))
⊢ cexp (-HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑x : ℂ)) =
    cexp
      (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
        -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))

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

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)).re < 0

Tactic:
simpa using pos_iff_ne_zero.mpr hv

Premises used: Iff.mpr, pos_iff_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
rw :
  (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      (((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
        cexp
          (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
            HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
rw₁ rw₂ :
  (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
⊢ ((↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))

Tactic:
rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]

Premises used: mul_assoc, integral_cexp_quadratic
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
e_a : (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) = 1
⊢ (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    1 *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))

Tactic:
congr 1
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
e_a : HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = (↑(HPow.hPow (β := ℝ) (2 * π * (↑v : ℝ)) 2⁻¹) : ℂ)
⊢ (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) = 1

Tactic:
simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul,
        NNReal.coe_ofNat, ofReal_mul, ofReal_ofNat, neg_neg, div_inv_eq_mul,
        ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]

Premises used: Real.rpow_eq_zero, neg_neg, ne_eq, Complex.ofReal_eq_zero, NNReal.coe_inv, one_div, NNReal.coe_ofNat, div_inv_eq_mul, NNReal.coe_mul, Complex.ofReal_ofNat, not_false_eq_true, Complex.ofReal_inv, Real.sqrt_eq_rpow, Complex.ofReal_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ 0 ≤ 2 * π * (↑v : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
e_a : HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = (↑(2 * π * (↑v : ℝ)) : ℂ) ^ (↑2⁻¹ : ℂ)
⊢ HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = (↑(HPow.hPow (β := ℝ) (2 * π * (↑v : ℝ)) 2⁻¹) : ℂ)

Tactic:
rw [Complex.ofReal_cpow (by positivity)]

Premises used: Complex.ofReal_cpow
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
e_a :
  HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = HPow.hPow (β := ℂ) (2 * (↑π : ℂ) * (↑(↑v : ℝ) : ℂ)) 2⁻¹
⊢ HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = (↑(2 * π * (↑v : ℝ)) : ℂ) ^ (↑2⁻¹ : ℂ)

Tactic:
push_cast
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = HPow.hPow (β := ℂ) (2 * (↑π : ℂ) * (↑(↑v : ℝ) : ℂ)) 2⁻¹

Tactic:
ring_nf
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
rw :
  cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
⊢ 1 *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
e_z :
  -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
      HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) =
    z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2
⊢ cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)

Tactic:
congr 1
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (↑(↑v : ℝ) : ℂ) ≠ 0

Tactic:
simpa