awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 : ι) ⋯))))

Tactic:
LinearMap.BilinForm.ext_basis (EuclideanSpace.basisFun J ℝ).toBasis fun i j ↦ ?_

Premises used: Real, Membership.mem, Subtype, EuclideanSpace.basisFun, LinearMap.BilinForm.ext_basis, OrthonormalBasis.toBasis
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
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 : ι) ⋯) fun (i : ↥J) ↦
                          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯))) :
                  (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) :
        ℝ)
⊢ 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 : ι) ⋯))))

Tactic:
refine LinearMap.BilinForm.ext_basis (EuclideanSpace.basisFun J ℝ).toBasis fun i j ↦ ?_

Premises used: Real, Membership.mem, Subtype, EuclideanSpace.basisFun, LinearMap.BilinForm.ext_basis, OrthonormalBasis.toBasis
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
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 : ι) ⋯)
⊢ 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 : ι) ⋯)

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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
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 : ι) ⋯)

Tactic:
simp [PiLp.inner_apply]

Premises used: PiLp.inner_apply
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥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 : ι) ⋯)

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]
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 : ι) ⋯)
hv :
  S (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑j : ι) ⋯) =
    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 : ι) ⋯) fun (i : ↥J) ↦
          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)
        (ofLp (p := 2) ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥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)

Tactic:
simp_rw [this, covariance_eval_multivariateGaussian hS,
        covarianceBilin_multivariateGaussian (hS.submatrix _)]

Premises used: ProbabilityTheory.covarianceBilin_multivariateGaussian, Matrix.PosSemidef.submatrix, ProbabilityTheory.covariance_eval_multivariateGaussian
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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 : ι) ⋯)
⊢ S (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑j : ι) ⋯) =
    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 : ι) ⋯) fun (i : ↥J) ↦
          Subtype.mk (p := fun (x : ι) ↦ x ∈ I) (↑i : ι) ⋯)
        (ofLp (p := 2) ((OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j)))

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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))
funProp₁ :
  MeasurableEmbedding (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
    ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫
⊢ Measurable (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
    ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
    (fun (u : EuclideanSpace ℝ ↥J) ↦
      ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) i, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
      (multivariateGaussian μ S))

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
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))
funProp₁ :
  MeasurableEmbedding (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
    ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j, u⟫
⊢ Measurable (β := ℝ) fun (u : EuclideanSpace ℝ ↥J) ↦
    ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j, u⟫

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i))
    (fun (u : EuclideanSpace ℝ ↥J) ↦
      ⟪(OrthonormalBasis.toBasis (EuclideanSpace.basisFun ↥J ℝ) : (a : ↥J) → EuclideanSpace ℝ ↥J) j, u⟫)
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
      (multivariateGaussian μ S))

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ AEMeasurable (β := EuclideanSpace ℝ ↥J)
    (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J) (multivariateGaussian μ S)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp (α := EuclideanSpace ℝ ↥J) (m0 := WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i)) id 2
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
      (multivariateGaussian μ S))

Tactic:
IsGaussian.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Multivariate
Goal:
ι : Type u_2
inst : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
i j : ↥J
⊢ MemLp (α := EuclideanSpace ℝ ↥J) (m0 := WithLp.measurableSpace 2 ((i : ↥J) → (fun (x : ↥J) ↦ ℝ) i)) id 2
    (Measure.map (⇑(EuclideanSpace.restrict₂ hJI) : (a : EuclideanSpace ℝ ↥I) → EuclideanSpace ℝ ↥J)
      (multivariateGaussian μ S))

Tactic:
exact IsGaussian.memLp_two_id

Premises used: ProbabilityTheory.IsGaussian.memLp_two_id
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ gaussianPDFReal μ v = fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))

Tactic:
rfl

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

Tactic:
ext1 x
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
m x : ℝ
⊢ gaussianPDFReal m 0 x = 0 x

Tactic:
simp [gaussianPDFReal]

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

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
x : ℝ
⊢ 0 ≤ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ Measurable (gaussianPDFReal μ v)

Tactic:
(((measurable_id.add_const _).pow_const _).neg.div_const _).exp.const_mul _

Premises used: measurable_id, Measurable.add_const, Measurable.div_const, Measurable.neg, ProbabilityTheory.gaussianPDFReal, Measurable.const_mul, Measurable.exp, Measurable.pow_const
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ StronglyMeasurable (gaussianPDFReal μ v)

Tactic:
(measurable_gaussianPDFReal μ v).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, ProbabilityTheory.measurable_gaussianPDFReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
pos :
  ∀ (hv : v = 0),
    @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
      (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ
neg :
  ∀ (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 : ℝ)))) ℙ

Tactic:
by_cases hv : v = 0
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ

Tactic:
simp [hv]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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)
rw :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)) ℙ
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g ℙ

Tactic:
rw [this]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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)) ℙ

Tactic:
(integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹

Premises used: Real.pi, HMul.hMul, MeasureTheory.Integrable.const_mul, Inv.inv, Real.sqrt, integrable_exp_neg_mul_sq, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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)
refine : 0 < (↑(2 * v)⁻¹ : ℝ)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)) ℙ

Tactic:
refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹

Premises used: Real.pi, HMul.hMul, MeasureTheory.Integrable.const_mul, Inv.inv, Real.sqrt, integrable_exp_neg_mul_sq, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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)
⊢ 0 < (↑(2 * v)⁻¹ : ℝ)

Tactic:
simpa [pos_iff_ne_zero]

Premises used: pos_iff_ne_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
suffices : g = fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g ℙ

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]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
h : ∀ (x : ℝ), g x = (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)
⊢ g = fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)

Tactic:
ext x
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
x : ℝ
h : -HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2) ∨ √(2 * π) = 0
⊢ g x = (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-(↑(2 * v)⁻¹ : ℝ) * HPow.hPow (β := ℕ) x 2)

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]

Premises used: inv_eq_zero, Real.exp_eq_exp, NNReal.coe_eq_zero, mul_eq_mul_left_iff, false_or, mul_eq_zero, NNReal.coe_inv, NNReal.coe_ofNat, neg_mul, NNReal.coe_mul, mul_inv_rev, NNReal.zero_le_coe, Real.sqrt_mul', Real.sqrt_eq_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
x : ℝ
h : -HPow.hPow (β := ℕ) x 2 / ((↑v : ℝ) * 2) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2) ∨ √(2 * π) = 0
⊢ -HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2) ∨ √(2 * π) = 0

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
x : ℝ
h : -HPow.hPow (β := ℕ) x 2 / ((↑v : ℝ) * 2) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2)
⊢ -HPow.hPow (β := ℕ) x 2 / ((↑v : ℝ) * 2) = -((↑v : ℝ)⁻¹ * 2⁻¹ * HPow.hPow (β := ℕ) x 2) ∨ √(2 * π) = 0

Tactic:
left
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
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)

Tactic:
field
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
⊢ @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
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
hg : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g ℙ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ

Tactic:
Integrable.comp_sub_right hg μ

Premises used: MeasureTheory.Integrable.comp_sub_right
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) x 2 / (2 * (↑v : ℝ)))
hg : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace g ℙ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) ℙ

Tactic:
exact Integrable.comp_sub_right hg μ

Premises used: MeasureTheory.Integrable.comp_sub_right
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
rw : (∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x)).toReal = 1
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (gaussianPDFReal μ v x) = 1

Tactic:
rw [← ENNReal.toReal_eq_one_iff]

Premises used: ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : v ≠ 0
⊢ AEStronglyMeasurable (m₀ := MeasureSpace.toMeasurableSpace) (gaussianPDFReal μ v) ℙ

Tactic:
fun_prop