test module

`Tests.IsotropicGaussianDensity`

3 named declarations scanned from Tests/IsotropicGaussianDensity.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

theorem Tests.IsotropicGaussianDensity.real_scale_density Partial Not mapped

No declaration docstring.

theorem real_scale_density (η : ℝ) (hη : 0 < η) :
    (stdGaussian ℝ).map (fun z : ℝ => Real.sqrt η • z) =
      (volume : Measure ℝ).withDensity (fun z =>
        ENNReal.ofReal
          ((Real.sqrt (2 * Real.pi * η))⁻¹ *
            Real.exp (-‖z‖ ^ 2 / (2 * η)))) := by
  simpa using (map_sqrt_smul_stdGaussian_eq_withDensity (E := ℝ) η hη)

Tests/IsotropicGaussianDensity.lean:8published source at ed709a7f320d

theorem Tests.IsotropicGaussianDensity.two_dimensional_density Partial Not mapped

No declaration docstring.

theorem two_dimensional_density (η : ℝ) (hη : 0 < η) :
    (stdGaussian (EuclideanSpace ℝ (Fin 2))).map (fun z => Real.sqrt η • z) =
      (volume : Measure (EuclideanSpace ℝ (Fin 2))).withDensity (fun z =>
        ENNReal.ofReal
          (((Real.sqrt (2 * Real.pi * η))⁻¹) ^ 2 *
            Real.exp (-‖z‖ ^ 2 / (2 * η)))) := by
  simpa using (map_sqrt_smul_stdGaussian_eq_withDensity
    (E := EuclideanSpace ℝ (Fin 2)) η hη)

Tests/IsotropicGaussianDensity.lean:16published source at ed709a7f320d

theorem Tests.IsotropicGaussianDensity.zero_dimensional_density Partial Not mapped

No declaration docstring.

theorem zero_dimensional_density (η : ℝ) (hη : 0 < η) :
    (stdGaussian (EuclideanSpace ℝ (Fin 0))).map (fun z => Real.sqrt η • z) =
      (volume : Measure (EuclideanSpace ℝ (Fin 0))) := by
  have hnorm0 (z : EuclideanSpace ℝ (Fin 0)) : ‖z‖ = 0 := by
    rw [show z = 0 from Subsingleton.elim _ _, norm_zero]
  simpa [hnorm0] using (map_sqrt_smul_stdGaussian_eq_withDensity
    (E := EuclideanSpace ℝ (Fin 0)) η hη)

#print axioms map_sqrt_smul_stdGaussian_eq_withDensity

end Tests.IsotropicGaussianDensity

Tests/IsotropicGaussianDensity.lean:25published source at ed709a7f320d

Complete Lean source

Tests/IsotropicGaussianDensity.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity

open MeasureTheory ProbabilityTheory
open AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity

namespace Tests.IsotropicGaussianDensity

theorem real_scale_density (η : ℝ) (hη : 0 < η) :
    (stdGaussian ℝ).map (fun z : ℝ => Real.sqrt η • z) =
      (volume : Measure ℝ).withDensity (fun z =>
        ENNReal.ofReal
          ((Real.sqrt (2 * Real.pi * η))⁻¹ *
            Real.exp (-‖z‖ ^ 2 / (2 * η)))) := by
  simpa using (map_sqrt_smul_stdGaussian_eq_withDensity (E := ℝ) η hη)

theorem two_dimensional_density (η : ℝ) (hη : 0 < η) :
    (stdGaussian (EuclideanSpace ℝ (Fin 2))).map (fun z => Real.sqrt η • z) =
      (volume : Measure (EuclideanSpace ℝ (Fin 2))).withDensity (fun z =>
        ENNReal.ofReal
          (((Real.sqrt (2 * Real.pi * η))⁻¹) ^ 2 *
            Real.exp (-‖z‖ ^ 2 / (2 * η)))) := by
  simpa using (map_sqrt_smul_stdGaussian_eq_withDensity
    (E := EuclideanSpace ℝ (Fin 2)) η hη)

theorem zero_dimensional_density (η : ℝ) (hη : 0 < η) :
    (stdGaussian (EuclideanSpace ℝ (Fin 0))).map (fun z => Real.sqrt η • z) =
      (volume : Measure (EuclideanSpace ℝ (Fin 0))) := by
  have hnorm0 (z : EuclideanSpace ℝ (Fin 0)) : ‖z‖ = 0 := by
    rw [show z = 0 from Subsingleton.elim _ _, norm_zero]
  simpa [hnorm0] using (map_sqrt_smul_stdGaussian_eq_withDensity
    (E := EuclideanSpace ℝ (Fin 0)) η hη)

#print axioms map_sqrt_smul_stdGaussian_eq_withDensity

end Tests.IsotropicGaussianDensity