awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Eq (α := EuclideanSpace ℝ ↥J →L[ℝ] EuclideanSpace ℝ ↥J →L[ℝ] ℝ)
    (covarianceBilin
      (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
        (multivariateGaussian μ S)))
    (covarianceBilin
      (multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
        (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)))
have hv : Eq (α := LinearMap.BilinForm ℝ (EuclideanSpace ℝ ↥J))
  (ContinuousLinearMap.toBilinForm
    (covarianceBilin
      (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
        (multivariateGaussian μ S))))
  (ContinuousLinearMap.toBilinForm
    (covarianceBilin
      (multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
        (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry) fun (i : ↥J) ↦
          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry))))
Tactic: rw [← ContinuousLinearMap.toBilinForm_inj]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Eq (α := LinearMap.BilinForm ℝ (EuclideanSpace ℝ ↥J))
    (ContinuousLinearMap.toBilinForm
      (covarianceBilin
        (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
          (multivariateGaussian μ S))))
    (ContinuousLinearMap.toBilinForm
      (covarianceBilin
        (multivariateGaussian ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
          (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
            Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯))))
have hv : ∀ (i j : ↥J),
  Eq (α := ℝ)
    ((((ContinuousLinearMap.toBilinForm
                  (covarianceBilin
                    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
                      (multivariateGaussian μ S))) :
                (a : EuclideanSpace ℝ ↥J) → EuclideanSpace ℝ ↥J →ₗ[ℝ] ℝ)
              ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i :
                EuclideanSpace ℝ ↥J) :
            EuclideanSpace ℝ ↥J →ₗ[ℝ] ℝ) :
          (a : EuclideanSpace ℝ ↥J) → ℝ)
        ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j :
          EuclideanSpace ℝ ↥J) :
      ℝ)
    ((((ContinuousLinearMap.toBilinForm
                  (covarianceBilin
                    (multivariateGaussian
                      ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
                      (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry) fun (i : ↥J) ↦
                        Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry))) :
                (a : EuclideanSpace ℝ ↥J) → EuclideanSpace ℝ ↥J →ₗ[ℝ] ℝ)
              ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i :
                EuclideanSpace ℝ ↥J) :
            EuclideanSpace ℝ ↥J →ₗ[ℝ] ℝ) :
          (a : EuclideanSpace ℝ ↥J) → ℝ)
        ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j :
          EuclideanSpace ℝ ↥J) :
      ℝ)
Tactic: refine LinearMap.BilinForm.ext_basis (EuclideanSpace.basisFun J ℝ).toBasis fun i j ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i_1 j i : ↥J
⊢ Eq (α := EuclideanSpace ℝ ↥I → ℝ)
    ((fun (u : EuclideanSpace ℝ ↥J) ↦
        ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫) ∘
      (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J))
    fun (u : EuclideanSpace ℝ ↥I) ↦ u.ofLp (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)
have h : ∀ (x : EuclideanSpace ℝ ↥I),
  ((fun (u : EuclideanSpace ℝ ↥J) ↦
          ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫) ∘
        (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J))
      x =
    x.ofLp (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (hypothesis)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ cov[(fun (u : EuclideanSpace ℝ ↥J) ↦
          ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫) ∘
        (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J),
      (fun (u : EuclideanSpace ℝ ↥J) ↦
          ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j, u⟫) ∘
        (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J);
      multivariateGaussian μ S] =
    (((covarianceBilin
                (multivariateGaussian
                  ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
                  (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
                    Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)) :
              (a : EuclideanSpace ℝ ↥J) → EuclideanSpace ℝ ↥J →L[ℝ] ℝ)
            ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i :
              EuclideanSpace ℝ ↥J) :
          EuclideanSpace ℝ ↥J →L[ℝ] ℝ) :
        (a : EuclideanSpace ℝ ↥J) → ℝ)
      ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j :
        EuclideanSpace ℝ ↥J)
have this : ∀ (i : ↥J),
  Eq (α := EuclideanSpace ℝ ↥I → ℝ)
    ((fun (u : EuclideanSpace ℝ ↥J) ↦
        ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫) ∘
      (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J))
    fun (u : EuclideanSpace ℝ ↥I) ↦ u.ofLp (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry)
Tactic: have (i : J) : (fun u ↦ ⟪(EuclideanSpace.basisFun J ℝ).toBasis i, u⟫) ∘
          EuclideanSpace.restrict₂ hJI = fun u ↦ u ⟨i.1, hJI i.2⟩ := by ext; simp [PiLp.inner_apply]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
this :
  ∀ (i : ↥J),
    Eq (α := EuclideanSpace ℝ ↥I → ℝ)
      ((fun (u : EuclideanSpace ℝ ↥J) ↦
          ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫) ∘
        (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J))
      fun (u : EuclideanSpace ℝ ↥I) ↦ u.ofLp (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)
⊢ cov[(fun (u : EuclideanSpace ℝ ↥J) ↦
          ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫) ∘
        (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J),
      (fun (u : EuclideanSpace ℝ ↥J) ↦
          ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j, u⟫) ∘
        (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J);
      multivariateGaussian μ S] =
    (((covarianceBilin
                (multivariateGaussian
                  ((EuclideanSpace.restrict₂ hJI : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) μ)
                  (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) fun (i : ↥J) ↦
                    Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)) :
              (a : EuclideanSpace ℝ ↥J) → EuclideanSpace ℝ ↥J →L[ℝ] ℝ)
            ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i :
              EuclideanSpace ℝ ↥J) :
          EuclideanSpace ℝ ↥J →L[ℝ] ℝ) :
        (a : EuclideanSpace ℝ ↥J) → ℝ)
      ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j :
        EuclideanSpace ℝ ↥J)
have hv : S (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑j : ι) sorry) =
  dotProduct (m := ↥J)
    (ofLp (p := 2) ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i))
    (mulVec (n := ↥J)
      (S.submatrix (fun (i : ↥J) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry) fun (i : ↥J) ↦
        Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) sorry)
      (ofLp (p := 2) ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j)))
Tactic: simp_rw [this, covariance_eval_multivariateGaussian hS,
        covarianceBilin_multivariateGaussian (hS.submatrix _)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ Measurable (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
    ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫
have funProp : LE.le.{u_2} (α := MeasurableSpace (EuclideanSpace ℝ ↥J)) (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
  (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
funProp :
  LE.le.{u_2} (α := MeasurableSpace (EuclideanSpace ℝ ↥J)) (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
    (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
⊢ Measurable (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
    ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
  ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ Measurable (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
    ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j, u⟫
have funProp : LE.le.{u_2} (α := MeasurableSpace (EuclideanSpace ℝ ↥J)) (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
  (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Multivariate (goal)
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
funProp :
  LE.le.{u_2} (α := MeasurableSpace (EuclideanSpace ℝ ↥J)) (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
    (WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
⊢ Measurable (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
    ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j, u⟫
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
  ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j, u⟫
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
m : ℝ
⊢ gaussianPDFReal m 0 = 0
have h : ∀ (x : ℝ), gaussianPDFReal m 0 x = 0 x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ
have pos : ∀ (hv : v = 0),
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
pos :
  ∀ (hv : v = 0),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
      (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ
have neg : ∀ (hv : ¬v = 0),
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
this : g = fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g ℙ
have rw : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
  (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)) ℙ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
this : g = fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)) ℙ
have refine : 0 < (↑(2 * v)⁻¹ : ℝ)
Tactic: refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g ℙ
have suffices : g = fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)
Tactic: suffices g = fun x ↦ (√(2 * π * v))⁻¹ * rexp (-(2 * v)⁻¹ * x ^ 2) by
      rw [this]
      refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹
      simpa [pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
⊢ g = fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)
have h : ∀ (x : ℝ), g x = (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
x : ℝ
⊢ g x = (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)
have h : -HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2) ∨ √(2 * π) = 0
Tactic: simp only [g, NNReal.zero_le_coe, Real.sqrt_mul',
      mul_inv_rev, NNReal.coe_mul, NNReal.coe_inv, NNReal.coe_ofNat, neg_mul, mul_eq_mul_left_iff,
      Real.exp_eq_exp, mul_eq_zero, inv_eq_zero, Real.sqrt_eq_zero, NNReal.coe_eq_zero, hv,
      false_or]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
x : ℝ
⊢ -HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2) ∨ √(2 * π) = 0
have h : -HPow.hPow (β := ℕ) x 2 / ((↑v : ℝ) * 2) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2) ∨ √(2 * π) = 0
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
x : ℝ
⊢ -HPow.hPow (β := ℕ) x 2 / ((↑v : ℝ) * 2) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2) ∨ √(2 * π) = 0
have h : -HPow.hPow (β := ℕ) x 2 / ((↑v : ℝ) * 2) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2)
Tactic: left
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ
have hg : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g ℙ
Tactic: have hg : Integrable g := by
    suffices g = fun x ↦ (√(2 * π * v))⁻¹ * rexp (-(2 * v)⁻¹ * x ^ 2) by
      rw [this]
      refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹
      simpa [pos_iff_ne_zero]
    ext x
    simp only [g, NNReal.zero_le_coe, Real.sqrt_mul',
      mul_inv_rev, NNReal.coe_mul, NNReal.coe_inv, NNReal.coe_ofNat, neg_mul, mul_eq_mul_left_iff,
      Real.exp_eq_exp, mul_eq_zero, inv_eq_zero, Real.sqrt_eq_zero, NNReal.coe_eq_zero, hv,
      false_or]
    rw [mul_comm]
    left
    field
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1
have rw : (∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
Tactic: rw [← ENNReal.toReal_eq_one_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ (∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
have hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
Tactic: have hfm : AEStronglyMeasurable (gaussianPDFReal μ v) volume := by fun_prop
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
⊢ (∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
have hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
Tactic: have hf : 0 ≤ₐₛ gaussianPDFReal μ v := ae_of_all _ (gaussianPDFReal_nonneg μ v)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
⊢ (∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
have rw : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦ gaussianPDFReal μ v a) 1
Tactic: rw [← integral_eq_lintegral_of_nonneg_ae hf hfm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦ gaussianPDFReal μ v a) 1
have simp : ((√(2 * π * (↑v : ℝ)))⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦
      rexp (-HPow.hPow (β := ℕ) (a - μ) 2 / (2 * (↑v : ℝ)))) =
  1
Tactic: simp only [gaussianPDFReal,
    integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦
        rexp (-HPow.hPow (β := ℕ) (a - μ) 2 / (2 * (↑v : ℝ)))) =
    1
have rw : ((√(2 * π * (↑v : ℝ)))⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))) =
  1
Tactic: rw [integral_sub_right_eq_self (μ := volume) (fun a ↦ rexp (-a ^ 2 / ((2 : ℝ) * v))) μ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))) =
    1
have simp : ((√(2 * π * (↑v : ℝ)))⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      rexp (-((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2))) =
  1
Tactic: simp only [div_eq_inv_mul, mul_inv_rev,
    mul_neg]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2))) =
    1
have simp_rw : ((√(2 * π * (↑v : ℝ)))⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      rexp (-(↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2)) =
  1
Tactic: simp_rw [← neg_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
hfm : AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ
hf : 0 ≤ᶠ[ae (F := Measure ℝ) ℙ] gaussianPDFReal μ v
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-(↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2)) =
    1
have rw : √((2 * π * (↑v : ℝ))⁻¹ * (π / ((↑v : ℝ)⁻¹ * 2⁻¹))) = 1
Tactic: rw [neg_mul, integral_gaussian, ← Real.sqrt_inv, ← Real.sqrt_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
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
⊢ ((√(2 * π * (↑v : ℝ)))⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        rexp (-(↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2)) =
    1
have hx : 0 ≤ (2 * π * (↑v : ℝ))⁻¹
Tactic: rw [neg_mul, integral_gaussian, ← Real.sqrt_inv, ← Real.sqrt_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x) 1
have h : ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1
Tactic: have h := lintegral_gaussianPDFReal_eq_one μ hv