production module

`AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian`

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/ProbabilityDistributions/Gaussian.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.Gaussian

Imported by

AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributionsAutoSamplingTheory.TechnicalLemmas.RegistryAutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Girsanov

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/ProbabilityDistributions/Gaussian.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Gaussian

/-!
# Gaussian distribution technical lemmas

Preferred Mathlib-style import path for ASTIS-owned Gaussian leaves:
coordinate laws, moment integrability, centered means, and variance-one
normalization.

The original `TechnicalLemmas.Gaussian` module remains as a compatibility
surface.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace ProbabilityDistributions
namespace Gaussian

export AutoSamplingTheory.TechnicalLemmas.Gaussian (
  stdGaussianPi
  stdGaussianPi_isProbabilityMeasure
  stdGaussianPi_isFiniteMeasure
  map_eval_stdGaussianPi
  integral_id_gaussianReal_zero
  integral_exp_mul_gaussianReal
  integral_exp_mul_gaussianReal_zero_one
  integrable_eval_stdGaussianPi
  integrable_const_mul_eval_stdGaussianPi
  integrable_linearForm_stdGaussianPi
  integrable_const_mul_sq_gaussianReal_zero
  integrable_sq_eval_stdGaussianPi
  integral_eval_stdGaussianPi
  integral_const_mul_eval_stdGaussianPi
  integral_linearForm_stdGaussianPi
  integral_exp_linearForm_stdGaussianPi
  integral_exp_centered_linearForm_stdGaussianPi
  gaussianReal_withDensity_exp_shift
  pi_gaussianReal_withDensity_exp_shift
  pi_gaussianReal_shift_integral
  stdGaussianPi_withDensity_exp_shift
  stdGaussianPi_shift_integral
  pi_gaussianReal_shift_integral_map_toLp
  stdGaussianPi_shift_integral_map_toLp
  inner_toLp_toLp_eq_sum_mul
  norm_sq_toLp_eq_sum_sq
  stdGaussian_shift_integral_map_toLp
  variance_id_gaussianReal_zero_one
  nnrealVarianceOneOfGaussianRealUnitLaw
  realVarianceOneOfNNRealVarianceOne
)

end Gaussian
end ProbabilityDistributions
end TechnicalLemmas
end AutoSamplingTheory