Real

📁 Source: Mathlib/Probability/Distributions/Gaussian/Real.lean

Statistics

Metric	Count
Definitions gaussianPDF, gaussianPDFReal, gaussianReal	3
Theorems gaussianReal_comap_apply, gaussianReal_map_symm_apply, cgf_gaussianReal, charFun_gaussianReal, complexMGF_gaussianReal, complexMGF_id_gaussianReal, gaussianPDFReal_add, gaussianPDFReal_def, gaussianPDFReal_inv_mul, gaussianPDFReal_mul, gaussianPDFReal_nonneg, gaussianPDFReal_pos, gaussianPDFReal_sub, gaussianPDFReal_zero_var, gaussianPDF_def, gaussianPDF_lt_top, gaussianPDF_ne_top, gaussianPDF_pos, gaussianPDF_zero_var, gaussianReal_absolutelyContinuous, gaussianReal_absolutelyContinuous', gaussianReal_add_const, gaussianReal_add_gaussianReal_of_indepFun, gaussianReal_apply, gaussianReal_apply_eq_integral, gaussianReal_const_add, gaussianReal_const_mul, gaussianReal_const_sub, gaussianReal_conv_gaussianReal, gaussianReal_div_const, gaussianReal_ext_iff, gaussianReal_map_add_const, gaussianReal_map_const_add, gaussianReal_map_const_mul, gaussianReal_map_const_sub, gaussianReal_map_continuousLinearMap, gaussianReal_map_div_const, gaussianReal_map_linearMap, gaussianReal_map_mul_const, gaussianReal_map_neg, gaussianReal_map_sub_const, gaussianReal_mul_const, gaussianReal_neg, gaussianReal_of_var_ne_zero, gaussianReal_sub_const, gaussianReal_zero_var, instIsProbabilityMeasureGaussianReal, integrableExpSet_fun_id_gaussianReal, integrableExpSet_id_gaussianReal, integrable_exp_mul_gaussianReal, integrable_gaussianPDFReal, integral_continuousLinearMap_gaussianReal, integral_gaussianPDFReal_eq_one, integral_gaussianReal_eq_integral_smul, integral_id_gaussianReal, integral_linearMap_gaussianReal, lintegral_gaussianPDFReal_eq_one, lintegral_gaussianPDF_eq_one, measurable_gaussianPDF, measurable_gaussianPDFReal, memLp_id_gaussianReal, memLp_id_gaussianReal', mgf_fun_id_gaussianReal, mgf_gaussianReal, mgf_id_gaussianReal, noAtoms_gaussianReal, rnDeriv_gaussianReal, stronglyMeasurable_gaussianPDFReal, support_gaussianPDF, toReal_gaussianPDF, variance_continuousLinearMap_gaussianReal, variance_fun_id_gaussianReal, variance_id_gaussianReal, variance_linearMap_gaussianReal	74
Total	77

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gaussianReal_comap_apply 📖	mathematical	MeasurableEmbedding Real Real.measurableSpace HasDerivAt DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal MeasurableSet	DFunLike.coe MeasureTheory.Measure Real Real.measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.comap ProbabilityTheory.gaussianReal ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Real.instMul abs Real.lattice Real.instAddGroup ProbabilityTheory.gaussianPDFReal	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ProbabilityTheory.gaussianReal_of_var_ne_zero ProbabilityTheory.gaussianPDF_def withDensity_ofReal_comap_apply_eq_integral_abs_deriv_mul' MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.gaussianPDFReal_nonneg ProbabilityTheory.integrable_gaussianPDFReal

MeasurableEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gaussianReal_map_symm_apply 📖	mathematical	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal DFunLike.coe MeasurableEquiv Real.measurableSpace EquivLike.toFunLike instEquivLike MeasurableSet	DFunLike.coe MeasureTheory.Measure Real Real.measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.map MeasurableEquiv EquivLike.toFunLike instEquivLike symm ProbabilityTheory.gaussianReal ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Real.instMul abs Real.lattice Real.instAddGroup ProbabilityTheory.gaussianPDFReal	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ProbabilityTheory.gaussianReal_of_var_ne_zero ProbabilityTheory.gaussianPDF_def withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul' MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass ProbabilityTheory.gaussianPDFReal_nonneg ProbabilityTheory.integrable_gaussianPDFReal

ProbabilityTheory

Definitions

Name	Category	Theorems
gaussianPDF 📖	CompOp	11 math math: lintegral_gaussianPDF_eq_one, rnDeriv_gaussianReal, support_gaussianPDF, gaussianReal_of_var_ne_zero, gaussianPDF_pos, measurable_gaussianPDF, gaussianReal_apply, gaussianPDF_zero_var, gaussianPDF_def, gaussianPDF_lt_top, toReal_gaussianPDF
gaussianPDFReal 📖	CompOp	19 math math: integral_gaussianReal_eq_integral_smul, integral_gaussianPDFReal_eq_one, gaussianPDFReal_def, gaussianPDFReal_sub, gaussianPDFReal_pos, MeasurableEmbedding.gaussianReal_comap_apply, gaussianPDFReal_inv_mul, gaussianPDFReal_zero_var, lintegral_gaussianPDFReal_eq_one, gaussianPDF_def, measurable_gaussianPDFReal, stronglyMeasurable_gaussianPDFReal, toReal_gaussianPDF, gaussianPDFReal_add, MeasurableEquiv.gaussianReal_map_symm_apply, gaussianPDFReal_mul, gaussianReal_apply_eq_integral, integrable_gaussianPDFReal, gaussianPDFReal_nonneg
gaussianReal 📖	CompOp	55 math math: gaussianReal_map_const_mul, gaussianReal_const_mul, variance_fun_id_gaussianReal, gaussianReal_map_neg, IsGaussian.map_eq_gaussianReal, rnDeriv_gaussianReal, integral_gaussianReal_eq_integral_smul, integral_continuousLinearMap_gaussianReal, gaussianReal_zero_var, gaussianReal_map_continuousLinearMap, gaussianReal_of_var_ne_zero, noAtoms_gaussianReal, gaussianReal_map_linearMap, gaussianReal_add_const, integrableExpSet_id_gaussianReal, map_pi_eq_stdGaussian, instIsProbabilityMeasureGaussianReal, integrableExpSet_fun_id_gaussianReal, memLp_id_gaussianReal', mgf_fun_id_gaussianReal, gaussianReal_apply, gaussianReal_neg, gaussianReal_conv_gaussianReal, isGaussian_gaussianReal, gaussianReal_mul_const, variance_continuousLinearMap_gaussianReal, gaussianReal_const_add, integral_linearMap_gaussianReal, gaussianReal_map_div_const, MeasurableEmbedding.gaussianReal_comap_apply, integrable_exp_mul_gaussianReal, gaussianReal_map_mul_const, gaussianReal_add_gaussianReal_of_indepFun, gaussianReal_ext_iff, gaussianReal_map_sub_const, memLp_id_gaussianReal, gaussianReal_const_sub, variance_id_gaussianReal, gaussianReal_sub_const, measurePreserving_eval_multivariateGaussian, gaussianReal_map_add_const, complexMGF_id_gaussianReal, integral_id_gaussianReal, stdGaussian_eq_map_pi_orthonormalBasis, gaussianReal_map_const_sub, gaussianReal_absolutelyContinuous', gaussianReal_map_const_add, variance_linearMap_gaussianReal, mgf_id_gaussianReal, MeasurableEquiv.gaussianReal_map_symm_apply, gaussianReal_div_const, gaussianReal_apply_eq_integral, charFun_gaussianReal, IsGaussian.eq_gaussianReal, gaussianReal_absolutelyContinuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cgf_gaussianReal 📖	mathematical	MeasureTheory.Measure.map Real Real.measurableSpace gaussianReal	cgf Real Real.instAdd Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid NNReal.toReal Monoid.toPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat cgf.eq_1 mgf_gaussianReal Real.log_exp
charFun_gaussianReal 📖	mathematical	—	MeasureTheory.charFun Real Real.measurableSpace InnerProductSpace.toInner Real.instRCLike NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField RCLike.toInnerProductSpaceReal gaussianReal Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid NNReal.toReal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat complexMGF_id_mul_I complexMGF_id_gaussianReal mul_pow Complex.I_sq mul_neg mul_one sub_eq_add_neg Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero
complexMGF_gaussianReal 📖	mathematical	MeasureTheory.Measure.map Real Real.measurableSpace gaussianReal	complexMGF Complex.exp Complex Complex.instAdd Complex.instMul Complex.ofReal DivInvMonoid.toDiv Complex.instDivInvMonoid NNReal.toReal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	aemeasurable_of_map_neZero MeasureTheory.IsProbabilityMeasure.neZero instIsProbabilityMeasureGaussianReal Nat.instAtLeastTwoHAddOfNat complexMGF_id_map complexMGF_id_gaussianReal
complexMGF_id_gaussianReal 📖	mathematical	—	complexMGF Real Real.measurableSpace gaussianReal Complex.exp Complex Complex.instAdd Complex.instMul Complex.ofReal DivInvMonoid.toDiv Complex.instDivInvMonoid NNReal.toReal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat gaussianReal_zero_var MeasureTheory.integral_dirac Complex.instCompleteSpace instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MulZeroClass.zero_mul zero_div add_zero integral_gaussianReal_eq_integral_smul Complex.ofReal_mul Complex.ofReal_inv Complex.ofReal_exp Complex.ofReal_div Complex.ofReal_neg Complex.ofReal_pow Complex.ofReal_sub mul_assoc MeasureTheory.integral_const_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow integral_cexp_quadratic mul_inv_rev Complex.inv_re Complex.normSq_ofReal div_self_mul_self' Complex.normSq_ofNat Complex.inv_im neg_zero MulZeroClass.mul_zero sub_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Real.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsOrderedRing Real.instNontrivial pos_iff_ne_zero Real.sqrt_eq_rpow one_div neg_neg div_inv_eq_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg le_of_lt mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.pi_pos Mathlib.Meta.Positivity.nnreal_coe_pos lt_of_le_of_ne' zero_le Mathlib.Meta.NormNum.isNNRat_eq_false RCLike.charZero_rclike Nat.cast_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass ne_of_gt Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Complex.ofReal_cpow Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.nnrat_rawCast mul_neg Mathlib.Tactic.FieldSimp.subst_sub neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Tactic.FieldSimp.zpow'_ofNat div_neg Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ sub_neg_eq_add Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
gaussianPDFReal_add 📖	mathematical	—	gaussianPDFReal Real Real.instAdd Real.instSub	—	sub_eq_add_neg gaussianPDFReal_sub neg_neg
gaussianPDFReal_def 📖	mathematical	—	gaussianPDFReal Real Real.instMul Real.instInv Real.sqrt instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi NNReal.toReal Real.exp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Monoid.toPow Real.instMonoid Real.instSub	—	—
gaussianPDFReal_inv_mul 📖	mathematical	—	gaussianPDFReal Real Real.instMul Real.instInv abs Real.lattice Real.instAddGroup NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Real.instLE Real.instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.semiring sq_nonneg Real.linearOrder AddGroup.existsAddOfLE Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedRing.toPosMulMono Real.partialOrder Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instPreorder Real.instIsOrderedAddMonoid	—	sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.sqrt_mul' mul_inv_rev mul_assoc Real.sqrt_mul le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.pi_pos lt_of_le_of_ne' Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Nat.instAtLeastTwoHAddOfNat even_two_mul pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg ne_of_gt Real.sqrt_pos_of_pos Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Real.sqrt_sq_eq_abs neg_div Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst mul_neg Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Nat.cast_zero Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat
gaussianPDFReal_mul 📖	mathematical	—	gaussianPDFReal Real Real.instMul abs Real.lattice Real.instAddGroup Real.instInv NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Real.instLE Real.instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.semiring Preorder.toLE PartialOrder.toPreorder Real.partialOrder MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Field.toSemifield Real.instField InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid inv_nonneg PosMulReflectLE.toPosMulReflectLT NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing PosMulStrictMono.toPosMulReflectLE MulZeroClass.toMul Real.linearOrder IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing sq_nonneg AddGroup.existsAddOfLE SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instPreorder Real.instIsOrderedAddMonoid	—	inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid inv_inv gaussianPDFReal_inv_mul inv_ne_zero inv_pow abs_inv
gaussianPDFReal_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero gaussianPDFReal	—	gaussianPDFReal.eq_1 mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing inv_nonneg_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.sqrt_nonneg le_of_lt Real.exp_pos
gaussianPDFReal_pos 📖	mathematical	—	Real Real.instLT Real.instZero gaussianPDFReal	—	gaussianPDFReal.eq_1 mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.sqrt_pos_of_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos Mathlib.Meta.Positivity.nnreal_coe_pos lt_of_le_of_ne' zero_le Real.exp_pos
gaussianPDFReal_sub 📖	mathematical	—	gaussianPDFReal Real Real.instSub Real.instAdd	—	sub_add_eq_sub_sub_swap
gaussianPDFReal_zero_var 📖	mathematical	—	gaussianPDFReal NNReal NNReal.instZero Pi.instZero Real Real.instZero	—	MulZeroClass.mul_zero Real.sqrt_zero inv_zero div_zero Real.exp_zero mul_one
gaussianPDF_def 📖	mathematical	—	gaussianPDF ENNReal.ofReal gaussianPDFReal	—	—
gaussianPDF_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder gaussianPDF Top.top instTopENNReal	—	—
gaussianPDF_ne_top 📖	—	—	—	—	—
gaussianPDF_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal gaussianPDF	—	gaussianPDF.eq_1 ENNReal.ofReal_pos gaussianPDFReal_pos
gaussianPDF_zero_var 📖	mathematical	—	gaussianPDF NNReal NNReal.instZero Pi.instZero Real ENNReal instZeroENNReal	—	gaussianPDFReal_zero_var ENNReal.ofReal_zero
gaussianReal_absolutelyContinuous 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous Real Real.measurableSpace gaussianReal MeasureTheory.MeasureSpace.volume Real.measureSpace	—	gaussianReal_of_var_ne_zero MeasureTheory.withDensity_absolutelyContinuous
gaussianReal_absolutelyContinuous' 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume gaussianReal	—	gaussianReal_of_var_ne_zero MeasureTheory.withDensity_absolutelyContinuous' Measurable.aemeasurable measurable_gaussianPDF MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass LT.lt.ne' gaussianPDF_pos
gaussianReal_add_const 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal	HasLaw Real Real.measurableSpace Real.instAdd gaussianReal	—	HasLaw.comp AEMeasurable.add_const ContinuousAdd.measurableAdd Real.borelSpace instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal aemeasurable_id gaussianReal_map_add_const
gaussianReal_add_gaussianReal_of_indepFun 📖	mathematical	IndepFun Real Real.measurableSpace MeasureTheory.Measure.map gaussianReal	MeasureTheory.Measure.map Real Real.measurableSpace Pi.instAdd Real.instAdd gaussianReal NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	IndepFun.map_add_eq_map_conv_map₀' ContinuousAdd.measurableMul₂ Real.borelSpace instSecondCountableTopologyReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal AEMeasurable.of_map_ne_zero MeasureTheory.IsProbabilityMeasure.neZero instIsProbabilityMeasureGaussianReal MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure gaussianReal_conv_gaussianReal
gaussianReal_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Real Real.measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike gaussianReal MeasureTheory.lintegral MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume gaussianPDF	—	gaussianReal_of_var_ne_zero MeasureTheory.withDensity_apply' MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal
gaussianReal_apply_eq_integral 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Real Real.measurableSpace Set ENNReal MeasureTheory.Measure.instFunLike gaussianReal ENNReal.ofReal MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume gaussianPDFReal	—	gaussianReal_apply MeasureTheory.ofReal_integral_eq_lintegral_ofReal MeasureTheory.Integrable.restrict integrable_gaussianPDFReal MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass gaussianPDFReal_nonneg
gaussianReal_const_add 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal	HasLaw Real Real.measurableSpace Real.instAdd gaussianReal	—	HasLaw.comp AEMeasurable.const_add ContinuousAdd.measurableAdd Real.borelSpace instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal aemeasurable_id gaussianReal_map_const_add
gaussianReal_const_mul 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal	HasLaw Real Real.measurableSpace Real.instMul gaussianReal NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Real.instLE Real.instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.semiring sq_nonneg Real.linearOrder AddGroup.existsAddOfLE Real.instAddGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedRing.toPosMulMono Real.partialOrder Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instPreorder Real.instIsOrderedAddMonoid	—	HasLaw.comp sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AEMeasurable.const_mul ContinuousMul.measurableMul Real.borelSpace IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal aemeasurable_id gaussianReal_map_const_mul
gaussianReal_const_sub 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal	HasLaw Real Real.measurableSpace Real.instSub gaussianReal	—	HasLaw.comp AEMeasurable.const_sub ContinuousSub.measurableSub Real.borelSpace IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal aemeasurable_id gaussianReal_map_const_sub
gaussianReal_conv_gaussianReal 📖	mathematical	—	MeasureTheory.Measure.conv Real Real.instAddMonoid Real.measurableSpace gaussianReal Real.instAdd NNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring	—	MeasureTheory.Measure.ext_of_charFun Real.borelSpace instSecondCountableTopologyReal Real.instCompleteSpace MeasureTheory.Measure.finite_of_finite_conv MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureGaussianReal MeasureTheory.charFun_conv Nat.instAtLeastTwoHAddOfNat charFun_gaussianReal Complex.exp_add Complex.ofReal_add Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.rat_rawCast_neg Mathlib.Tactic.RingNF.int_rawCast_neg add_zero
gaussianReal_div_const 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal	HasLaw Real Real.measurableSpace DivInvMonoid.toDiv Real.instDivInvMonoid gaussianReal NNReal NNReal.instDiv Real.instLE Real.instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.semiring sq_nonneg Real.linearOrder AddGroup.existsAddOfLE Real.instAddGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedRing.toPosMulMono Real.partialOrder Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instPreorder Real.instIsOrderedAddMonoid	—	HasLaw.comp sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AEMeasurable.div_const measurableDiv_of_mul_inv ContinuousMul.measurableMul Real.borelSpace IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal aemeasurable_id gaussianReal_map_div_const
gaussianReal_ext_iff 📖	mathematical	—	gaussianReal	—	integral_id_gaussianReal variance_id_gaussianReal
gaussianReal_map_add_const 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace Real.instAdd gaussianReal	—	gaussianReal_zero_var MeasureTheory.Measure.map_dirac instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring HasDerivAt.sub_const hasDerivAt_id MeasureTheory.Measure.ext MeasurableEquiv.gaussianReal_map_symm_apply abs_one Real.instIsOrderedRing one_mul gaussianReal_apply_eq_integral Equiv.addRight_symm gaussianPDFReal_sub
gaussianReal_map_const_add 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace Real.instAdd gaussianReal	—	add_comm gaussianReal_map_add_const
gaussianReal_map_const_mul 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace Real.instMul gaussianReal NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Real.instLE Real.instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.semiring sq_nonneg Real.linearOrder AddGroup.existsAddOfLE Real.instAddGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedRing.toPosMulMono Real.partialOrder Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instPreorder Real.instIsOrderedAddMonoid	—	sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid gaussianReal_zero_var MeasureTheory.Measure.map_dirac instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable Real.borelSpace instSecondCountableTopologyReal TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace MulZeroClass.mul_zero IsScalarTower.right MulZeroClass.zero_mul MeasureTheory.Measure.map_const MeasureTheory.IsProbabilityMeasure.measure_univ instIsProbabilityMeasureGaussianReal one_smul zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring HasDerivAt.const_mul hasDerivAt_id mul_one MeasureTheory.Measure.ext MeasurableEquiv.gaussianReal_map_symm_apply gaussianReal_apply_eq_integral isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Equiv.mulLeft₀_symm_apply gaussianPDFReal_inv_mul abs_inv Real.instIsStrictOrderedRing inv_mul_cancel₀ abs_eq_zero covariant_swap_add_of_covariant_add mul_assoc one_mul
gaussianReal_map_const_sub 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace Real.instSub gaussianReal	—	sub_eq_add_neg MeasureTheory.Measure.map_map Measurable.const_add ContinuousAdd.measurableAdd Real.borelSpace instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal measurable_id' Measurable.neg ContinuousNeg.measurableNeg IsSemitopologicalRing.toContinuousNeg gaussianReal_map_neg gaussianReal_map_const_add add_comm
gaussianReal_map_continuousLinearMap 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike gaussianReal NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instSemiring Real.toNNReal Monoid.toPow Real.instMonoid Real.instOne	—	gaussianReal_map_linearMap
gaussianReal_map_div_const 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace DivInvMonoid.toDiv Real.instDivInvMonoid gaussianReal NNReal NNReal.instDiv Real.instLE Real.instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.semiring sq_nonneg Real.linearOrder AddGroup.existsAddOfLE Real.instAddGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedRing.toPosMulMono Real.partialOrder Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instPreorder Real.instIsOrderedAddMonoid	—	sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_eq_mul_inv mul_comm NNReal.eq inv_pow gaussianReal_map_mul_const
gaussianReal_map_linearMap 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike gaussianReal NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring NNReal.instSemiring Real.toNNReal Monoid.toPow Real.instMonoid Real.instOne	—	Dual.apply_one_mul_eq sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid gaussianReal_map_const_mul mul_one Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing Real.instIsStrictOrderedRing Nat.instAtLeastTwoHAddOfNat even_two_mul
gaussianReal_map_mul_const 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace Real.instMul gaussianReal NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Real.instLE Real.instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.semiring sq_nonneg Real.linearOrder AddGroup.existsAddOfLE Real.instAddGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedRing.toPosMulMono Real.partialOrder Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instPreorder Real.instIsOrderedAddMonoid	—	sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_comm gaussianReal_map_const_mul
gaussianReal_map_neg 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace Real.instNeg gaussianReal	—	sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid neg_mul one_mul Real.instZeroLEOneClass Even.neg_pow Nat.instAtLeastTwoHAddOfNat one_pow gaussianReal_map_const_mul
gaussianReal_map_sub_const 📖	mathematical	—	MeasureTheory.Measure.map Real Real.measurableSpace Real.instSub gaussianReal	—	sub_eq_add_neg gaussianReal_map_add_const
gaussianReal_mul_const 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal	HasLaw Real Real.measurableSpace Real.instMul gaussianReal NNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NNReal.instSemiring Real.instLE Real.instZero Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Real.semiring sq_nonneg Real.linearOrder AddGroup.existsAddOfLE Real.instAddGroup Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsOrderedRing.toPosMulMono Real.partialOrder Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instAddCommMonoid Real.instPreorder Real.instIsOrderedAddMonoid	—	HasLaw.comp sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AEMeasurable.mul_const ContinuousMul.measurableMul Real.borelSpace IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal aemeasurable_id gaussianReal_map_mul_const
gaussianReal_neg 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal	HasLaw Real Real.measurableSpace Pi.instNeg Real.instNeg gaussianReal	—	Pi.neg_def HasLaw.comp AEMeasurable.neg ContinuousNeg.measurableNeg Real.borelSpace IsSemitopologicalRing.toContinuousNeg IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal aemeasurable_id gaussianReal_map_neg
gaussianReal_of_var_ne_zero 📖	mathematical	—	gaussianReal MeasureTheory.Measure.withDensity Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume gaussianPDF	—	—
gaussianReal_sub_const 📖	mathematical	HasLaw Real Real.measurableSpace gaussianReal	HasLaw Real Real.measurableSpace Real.instSub gaussianReal	—	HasLaw.comp AEMeasurable.sub_const ContinuousSub.measurableSub Real.borelSpace IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal aemeasurable_id gaussianReal_map_sub_const
gaussianReal_zero_var 📖	mathematical	—	gaussianReal NNReal NNReal.instZero MeasureTheory.Measure.dirac Real Real.measurableSpace	—	—
instIsProbabilityMeasureGaussianReal 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure Real Real.measurableSpace gaussianReal	—	gaussianReal_zero_var MeasureTheory.IsProbabilityMeasure.measure_univ MeasureTheory.Measure.dirac.isProbabilityMeasure gaussianReal_of_var_ne_zero MeasureTheory.withDensity_apply MeasureTheory.Measure.restrict_univ lintegral_gaussianPDF_eq_one
integrableExpSet_fun_id_gaussianReal 📖	mathematical	—	integrableExpSet Real Real.measurableSpace gaussianReal Set.univ	—	integrableExpSet_id_gaussianReal
integrableExpSet_id_gaussianReal 📖	mathematical	—	integrableExpSet Real Real.measurableSpace gaussianReal Set.univ	—	Set.ext integrable_exp_mul_gaussianReal
integrable_exp_mul_gaussianReal 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing Real.measurableSpace Real.exp Real.instMul gaussianReal	—	mgf_pos_iff MeasureTheory.IsProbabilityMeasure.neZero instIsProbabilityMeasureGaussianReal Nat.instAtLeastTwoHAddOfNat mgf_gaussianReal MeasureTheory.Measure.map_id' Real.exp_pos
integrable_gaussianPDFReal 📖	mathematical	—	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace gaussianPDFReal MeasureTheory.MeasureSpace.volume	—	Nat.instAtLeastTwoHAddOfNat gaussianPDFReal_def MulZeroClass.mul_zero Real.sqrt_zero inv_zero div_zero Real.exp_zero mul_one Real.sqrt_mul' mul_inv_rev neg_mul IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass mul_comm Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_zero ne_of_gt Mathlib.Meta.Positivity.nnreal_coe_pos lt_of_le_of_ne' zero_le one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero MeasureTheory.Integrable.const_mul integrable_exp_neg_mul_sq IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE lt_of_le_of_ne Real.instIsOrderedRing Real.instNontrivial MeasureTheory.Integrable.comp_sub_right ContinuousAdd.measurableAdd Real.borelSpace instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real
integral_continuousLinearMap_gaussianReal 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace gaussianReal DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ContinuousLinearMap.funLike	—	integral_linearMap_gaussianReal
integral_gaussianPDFReal_eq_one 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume gaussianPDFReal Real.instOne	—	lintegral_gaussianPDFReal_eq_one ENNReal.ofReal_eq_ofReal_iff MeasureTheory.integral_nonneg Real.instIsOrderedAddMonoid IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal gaussianPDFReal_nonneg zero_le_one Real.instZeroLEOneClass ENNReal.ofReal_one MeasureTheory.ofReal_integral_eq_lintegral_ofReal integrable_gaussianPDFReal MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass
integral_gaussianReal_eq_integral_smul 📖	mathematical	—	MeasureTheory.integral Real Real.measurableSpace gaussianReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField gaussianPDFReal	—	integral_withDensity_eq_integral_toReal_smul measurable_gaussianPDF MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass gaussianPDF_lt_top toReal_gaussianPDF
integral_id_gaussianReal 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace gaussianReal	—	deriv_mgf_zero integrableExpSet_fun_id_gaussianReal interior_univ Nat.instAtLeastTwoHAddOfNat mgf_fun_id_gaussianReal deriv_exp DifferentiableAt.fun_add DifferentiableAt.const_mul differentiableAt_id DifferentiableAt.div_const DifferentiableAt.fun_pow MulZeroClass.mul_zero zero_pow Nat.instCharZero zero_div add_zero Real.exp_zero one_mul deriv_fun_add deriv_fun_mul differentiableAt_const deriv_const' deriv_id'' mul_one zero_add deriv_div_const deriv_fun_pow pow_one
integral_linearMap_gaussianReal 📖	mathematical	—	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.measurableSpace gaussianReal DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing LinearMap.instFunLike	—	MeasureTheory.integral_map Continuous.aemeasurable BorelSpace.opensMeasurable Real.borelSpace IsModuleTopology.continuous_of_linearMap IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsModuleTopology.toContinuousSMul aestronglyMeasurable_id PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal gaussianReal_map_linearMap integral_id_gaussianReal
lintegral_gaussianPDFReal_eq_one 📖	mathematical	—	MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume ENNReal.ofReal gaussianPDFReal ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	ENNReal.toReal_eq_one_iff MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_gaussianPDFReal MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_of_all gaussianPDFReal_nonneg MeasureTheory.integral_eq_lintegral_of_nonneg_ae MeasureTheory.integral_const_mul Nat.instAtLeastTwoHAddOfNat MeasureTheory.integral_sub_right_eq_self ContinuousAdd.measurableAdd Real.borelSpace instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal MeasureTheory.IsAddLeftInvariant.isAddRightInvariant MeasureTheory.Measure.IsAddHaarMeasure.toIsAddLeftInvariant instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real div_eq_inv_mul mul_inv_rev mul_neg neg_mul integral_gaussian Real.sqrt_inv Real.sqrt_mul le_of_lt inv_pos_of_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos Mathlib.Meta.Positivity.nnreal_coe_pos lt_of_le_of_ne' zero_le IsStrictOrderedRing.toMulPosStrictMono Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_pos Real.instZeroLEOneClass zero_lt_one NeZero.one GroupWithZero.toNontrivial MulZeroClass.zero_mul NeZero.charZero_one RCLike.charZero_rclike Real.sqrt_mul' Real.sqrt_div' Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Real.sqrt_pos_of_pos Mathlib.Tactic.FieldSimp.NF.one_eq_eval one_ne_zero
lintegral_gaussianPDF_eq_one 📖	mathematical	—	MeasureTheory.lintegral Real MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.MeasureSpace.volume gaussianPDF ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	lintegral_gaussianPDFReal_eq_one
measurable_gaussianPDF 📖	mathematical	—	Measurable Real ENNReal Real.measurableSpace ENNReal.measurableSpace gaussianPDF	—	Measurable.ennreal_ofReal measurable_gaussianPDFReal
measurable_gaussianPDFReal 📖	mathematical	—	Measurable Real Real.measurableSpace gaussianPDFReal	—	Measurable.const_mul ContinuousMul.measurableMul Real.borelSpace IsSemitopologicalSemiring.toSeparatelyContinuousMul IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Measurable.exp Measurable.div_const measurableDiv_of_mul_inv ContinuousInv₀.measurableInv T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal Measurable.neg ContinuousNeg.measurableNeg IsSemitopologicalRing.toContinuousNeg Measurable.pow_const Monoid.measurablePow ContinuousMul.measurableMul₂ instSecondCountableTopologyReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring Measurable.add_const ContinuousAdd.measurableAdd instSeparatelyContinuousAddOfContinuousAdd IsSemitopologicalSemiring.toContinuousAdd measurable_id
memLp_id_gaussianReal 📖	mathematical	—	MeasureTheory.MemLp Real Real.measurableSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace ENNReal.ofNNReal gaussianReal	—	memLp_of_mem_interior_integrableExpSet integrableExpSet_id_gaussianReal interior_univ
memLp_id_gaussianReal' 📖	mathematical	—	MeasureTheory.MemLp Real Real.measurableSpace ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace gaussianReal	—	CanLift.prf ENNReal.canLift memLp_id_gaussianReal
mgf_fun_id_gaussianReal 📖	mathematical	—	mgf Real Real.measurableSpace gaussianReal Real.exp Real.instAdd Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid NNReal.toReal Monoid.toPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat mgf_gaussianReal MeasureTheory.Measure.map_id'
mgf_gaussianReal 📖	mathematical	MeasureTheory.Measure.map Real Real.measurableSpace gaussianReal	mgf Real.exp Real Real.instAdd Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid NNReal.toReal Monoid.toPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat aemeasurable_of_map_neZero MeasureTheory.IsProbabilityMeasure.neZero instIsProbabilityMeasureGaussianReal mgf_id_map complexMGF_ofReal complexMGF_id_gaussianReal mul_comm
mgf_id_gaussianReal 📖	mathematical	—	mgf Real Real.measurableSpace gaussianReal Real.exp Real.instAdd Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid NNReal.toReal Monoid.toPow Real.instMonoid instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	mgf_fun_id_gaussianReal
noAtoms_gaussianReal 📖	mathematical	—	MeasureTheory.NoAtoms Real Real.measurableSpace gaussianReal	—	gaussianReal_of_var_ne_zero MeasureTheory.noAtoms_withDensity Real.noAtoms_volume
rnDeriv_gaussianReal 📖	mathematical	—	Filter.EventuallyEq Real ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.MeasureSpace.volume MeasureTheory.Measure.rnDeriv Real.measurableSpace gaussianReal gaussianPDF	—	MeasureTheory.Measure.instOuterMeasureClass gaussianReal_zero_var gaussianPDF_zero_var Filter.EventuallyEq.symm MeasureTheory.Measure.eq_rnDeriv MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real Real.borelSpace SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instSecondCountableTopologyReal instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal measurable_zero MeasureTheory.mutuallySingular_dirac instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Real.noAtoms_volume MeasureTheory.withDensity_zero add_zero gaussianReal_of_var_ne_zero MeasureTheory.Measure.rnDeriv_withDensity measurable_gaussianPDF
stronglyMeasurable_gaussianPDFReal 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.measurableSpace gaussianPDFReal	—	Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_gaussianPDFReal
support_gaussianPDF 📖	mathematical	—	Function.support Real ENNReal instZeroENNReal gaussianPDF Set.univ	—	Set.ext LT.lt.ne' gaussianPDF_pos
toReal_gaussianPDF 📖	mathematical	—	ENNReal.toReal gaussianPDF gaussianPDFReal	—	gaussianPDF.eq_1 ENNReal.toReal_ofReal gaussianPDFReal_nonneg
variance_continuousLinearMap_gaussianReal 📖	mathematical	—	variance Real Real.measurableSpace DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike gaussianReal Real.instMul NNReal.toReal Real.toNNReal Monoid.toPow Real.instMonoid Real.instOne	—	variance_linearMap_gaussianReal
variance_fun_id_gaussianReal 📖	mathematical	—	variance Real Real.measurableSpace gaussianReal NNReal.toReal	—	variance_eq_integral Measurable.aemeasurable measurable_id' integral_id_gaussianReal MeasureTheory.integral_map AEMeasurable.sub_const ContinuousSub.measurableSub Real.borelSpace IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal aemeasurable_id Continuous.aestronglyMeasurable BorelSpace.opensMeasurable PseudoEMetricSpace.pseudoMetrizableSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Continuous.pow IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_id' gaussianReal_map_sub_const sub_self iteratedDeriv_mgf_zero integrableExpSet_fun_id_gaussianReal interior_univ Nat.instAtLeastTwoHAddOfNat mgf_fun_id_gaussianReal iteratedDeriv_succ iteratedDeriv_one MulZeroClass.zero_mul zero_add deriv_exp DifferentiableAt.div_const DifferentiableAt.const_mul DifferentiableAt.fun_pow differentiableAt_id deriv_div_const deriv_fun_mul deriv_const' deriv_fun_pow pow_one deriv_id'' mul_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz DifferentiableAt.exp differentiableAt_const MulZeroClass.mul_zero zero_pow Nat.instCharZero zero_div Real.exp_zero add_zero
variance_id_gaussianReal 📖	mathematical	—	variance Real Real.measurableSpace gaussianReal NNReal.toReal	—	variance_fun_id_gaussianReal
variance_linearMap_gaussianReal 📖	mathematical	—	variance Real Real.measurableSpace DFunLike.coe LinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal LinearMap.instFunLike gaussianReal Real.instMul NNReal.toReal Real.toNNReal Monoid.toPow Real.instMonoid Real.instOne	—	variance_id_map Continuous.aemeasurable BorelSpace.opensMeasurable Real.borelSpace IsModuleTopology.continuous_of_linearMap IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing IsModuleTopology.toContinuousSMul gaussianReal_map_linearMap variance_id_gaussianReal

---

← Back to Index