GaussianIntegral

📁 Source: Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

Statistics

Metric	Count
Definitions	0
Theorems `Gamma_one_half_eq`, `Gamma_nat_add_half`, `Gamma_nat_add_one_add_half`, `Gamma_one_half_eq`, `continuousAt_gaussian_integral`, `exp_neg_mul_rpow_isLittleO_exp_neg`, `exp_neg_mul_sq_isLittleO_exp_neg`, `integrableOn_Ioi_exp_neg_mul_sq_iff`, `integrableOn_rpow_mul_exp_neg_mul_rpow`, `integrableOn_rpow_mul_exp_neg_mul_sq`, `integrableOn_rpow_mul_exp_neg_rpow`, `integrable_cexp_neg_mul_sq`, `integrable_exp_neg_mul_sq`, `integrable_exp_neg_mul_sq_iff`, `integrable_mul_cexp_neg_mul_sq`, `integrable_mul_exp_neg_mul_sq`, `integrable_rpow_mul_exp_neg_mul_sq`, `integral_gaussian`, `integral_gaussian_Ioi`, `integral_gaussian_complex`, `integral_gaussian_complex_Ioi`, `integral_gaussian_sq_complex`, `integral_mul_cexp_neg_mul_sq`, `norm_cexp_neg_mul_sq`, `rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg`, `rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg`	26
Total	26

Complex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Gamma_one_half_eq` 📖	mathematical	—	`Gamma` `Complex` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `instPow` `ofReal` `Real.pi`	—	`Nat.instAtLeastTwoHAddOfNat` `one_div` `ofReal_inv` `Gamma_ofReal` `Real.sqrt_eq_rpow` `ofReal_cpow` `LT.lt.le` `Real.pi_pos` `ofReal_div` `ofReal_ofNat` `ofReal_one` `Real.Gamma_one_half_eq`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Gamma_nat_add_half` 📖	mathematical	—	`Gamma` `Real` `instAdd` `instNatCast` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `instMul` `Nat.doubleFactorial` `sqrt` `pi` `Monoid.toNatPow` `instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_add` `Gamma_one_half_eq` `Nat.cast_one` `one_mul` `pow_zero` `div_one` `Nat.cast_add` `mul_add` `Distrib.leftDistribClass` `mul_one` `Gamma_nat_add_one_add_half`
`Gamma_nat_add_one_add_half` 📖	mathematical	—	`Gamma` `Real` `instAdd` `instNatCast` `instOne` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `instMul` `Nat.doubleFactorial` `sqrt` `pi` `Monoid.toNatPow` `instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_add` `add_comm` `Gamma_add_one` `NeZero.charZero_one` `Gamma_one_half_eq` `Nat.cast_one` `one_mul` `pow_one` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_left` `add_right_comm` `ne_of_gt` `add_pos'` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `Nat.cast_pos'` `instZeroLEOneClass` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Nat.instIsOrderedAddMonoid` `zero_le` `Nat.instCanonicallyOrderedAdd` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `instIsOrderedRing` `instNontrivial` `Nat.cast_add` `one_div` `Nat.cast_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.pow_prod_atom` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0`
`Gamma_one_half_eq` 📖	mathematical	—	`Gamma` `Real` `DivInvMonoid.toDiv` `instDivInvMonoid` `instOne` `instOfNatAtLeastTwo` `instNatCast` `Nat.instAtLeastTwoHAddOfNat` `sqrt` `pi`	—	`Nat.instAtLeastTwoHAddOfNat` `Gamma_eq_integral` `one_half_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `MeasureTheory.integral_comp_rpow_Ioi_of_pos` `zero_lt_two` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `MeasureTheory.integral_const_mul` `MeasureTheory.setIntegral_congr_fun` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `rpow_mul` `le_of_lt` `Mathlib.Meta.NormNum.IsInt.neg_to_eq` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `rpow_neg` `rpow_one` `smul_eq_mul` `rpow_ofNat` `neg_mul` `one_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.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `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.eval_cons_mul_eval_cons_neg` `ne_of_lt` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `exp_pos` `Mathlib.Meta.NormNum.isNat_eq_false` `Nat.cast_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_sub` `Mathlib.Meta.NormNum.IsNat.to_isInt` `mul_div_assoc` `mul_comm` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass` `two_ne_zero'` `CharZero.NeZero.two` `integral_gaussian_Ioi`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_gaussian_integral` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.re`	`ContinuousAt` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `MeasureTheory.integral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `Complex.exp` `Complex.instMul` `Complex.instNeg` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal`	—	`exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.eventually_of_mem` `IsOpen.mem_nhds` `Continuous.isOpen_preimage` `Complex.continuous_re` `isOpen_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `Filter.univ_mem'` `norm_cexp_neg_mul_sq` `Real.exp_monotone` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `neg_le_neg` `le_of_lt` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul` `MeasureTheory.continuousAt_of_dominated` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `Filter.Eventually.of_forall` `Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `continuous_id'` `MeasureTheory.AEStronglyMeasurable.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.pow` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `secondCountableTopologyEither_of_right` `secondCountable_of_proper` `Complex.instProperSpace` `Complex.continuous_ofReal` `integrable_exp_neg_mul_sq` `MeasureTheory.ae_of_all` `ContinuousAt.cexp` `ContinuousAt.fun_mul` `ContinuousAt.neg` `IsTopologicalRing.toContinuousNeg` `continuousAt_id'` `continuousAt_const`
`exp_neg_mul_rpow_isLittleO_exp_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instOne`	`Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.exp` `Real.instMul` `Real.instNeg` `Real.instPow`	—	`Real.isLittleO_exp_comp_exp_comp` `Filter.Tendsto.atTop_mul_atTop₀` `Real.instIsOrderedRing` `Filter.tendsto_id` `Filter.tendsto_atTop_add_const_right` `Real.instIsOrderedAddMonoid` `Filter.Tendsto.const_mul_atTop` `Real.instIsStrictOrderedRing` `tendsto_rpow_atTop` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Filter.Tendsto.congr'` `Filter.eventuallyEq_of_mem` `Filter.Ioi_mem_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instNontrivial` `Real.rpow_sub_one` `LT.lt.ne'` `Set.mem_Ioi` `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.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_add` `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.mul_eq_eval₁` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `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` `ne_of_gt` `mul_neg` `mul_one` `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` `Mathlib.Tactic.FieldSimp.subst_sub` `neg_mul` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `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.zero_mul` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Meta.NormNum.IsNat.to_raw_eq`
`exp_neg_mul_sq_isLittleO_exp_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.exp` `Real.instMul` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `exp_neg_mul_rpow_isLittleO_exp_neg` `one_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`integrableOn_Ioi_exp_neg_mul_sq_iff` 📖	mathematical	—	`MeasureTheory.IntegrableOn` `Real` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.exp` `Real.instMul` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Set.Ioi` `Real.instPreorder` `Real.instZero` `MeasureTheory.MeasureSpace.volume` `Real.instLT`	—	`MeasureTheory.lintegral_mono` `neg_mul` `Real.norm_of_nonneg` `LT.lt.le` `Real.exp_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_nonpos_of_nonpos_of_nonneg` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `MeasureTheory.lintegral_const` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `Real.volume_Ioi` `one_mul` `LE.le.trans_lt` `MeasureTheory.Integrable.integrableOn` `integrable_exp_neg_mul_sq`
`integrableOn_rpow_mul_exp_neg_mul_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `Real.instOne` `Real.instLE` `Real.instZero`	`MeasureTheory.IntegrableOn` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Real.instPow` `Real.exp` `Set.Ioi` `Real.instPreorder` `MeasureTheory.MeasureSpace.volume`	—	`Real.rpow_pos_of_pos` `MeasureTheory.Integrable.const_mul` `MeasureTheory.IntegrableOn.eq_1` `integrableOn_rpow_mul_exp_neg_rpow` `MulZeroClass.mul_zero` `MeasureTheory.integrableOn_Ioi_comp_mul_left_iff` `MeasureTheory.IntegrableOn.congr_fun` `mul_assoc` `Real.mul_rpow` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.add_pf_add_zero` `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_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.without_one_mul` `CancelDenoms.sub_subst` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Set.mem_Ioi` `Real.rpow_mul` `neg_mul` `inv_mul_cancel₀` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Linarith.lt_of_lt_of_eq` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `sub_eq_zero_of_eq` `Real.rpow_neg_one` `mul_inv_cancel_left₀` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal`
`integrableOn_rpow_mul_exp_neg_mul_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instNeg` `Real.instOne`	`MeasureTheory.IntegrableOn` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Real.instPow` `Real.exp` `Monoid.toNatPow` `Real.instMonoid` `Set.Ioi` `Real.instPreorder` `MeasureTheory.MeasureSpace.volume`	—	`Nat.instAtLeastTwoHAddOfNat` `integrableOn_rpow_mul_exp_neg_mul_rpow` `one_le_two` `Real.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`integrableOn_rpow_mul_exp_neg_rpow` 📖	mathematical	`Real` `Real.instLT` `Real.instNeg` `Real.instOne` `Real.instLE`	`MeasureTheory.IntegrableOn` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.instMul` `Real.instPow` `Real.exp` `Set.Ioi` `Real.instPreorder` `Real.instZero` `MeasureTheory.MeasureSpace.volume`	—	`le_iff_lt_or_eq` `ContinuousAt.rexp` `continuousAt_neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `Set.Ioc_union_Ioi_eq_Ioi` `zero_le_one` `Real.instZeroLEOneClass` `MeasureTheory.integrableOn_union` `PseudoEMetricSpace.pseudoMetrizableSpace` `integrableOn_Icc_iff_integrableOn_Ioc` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Real.noAtoms_volume` `enorm_ne_top` `MeasureTheory.IntegrableOn.mul_continuousOn` `secondCountableTopologyEither_of_right` `intervalIntegrable_iff_integrableOn_Icc_of_le` `intervalIntegral.intervalIntegrable_rpow'` `ContinuousAt.comp_continuousWithinAt` `ContinuousWithinAt.rpow_const` `continuousWithinAt_id` `le_of_lt` `lt_trans` `zero_lt_one` `NeZero.charZero_one` `RCLike.charZero_rclike` `CompactIccSpace.isCompact_Icc` `ConditionallyCompleteLinearOrder.toCompactIccSpace` `instOrderTopologyReal` `ne_of_gt` `lt_of_lt_of_le` `integrable_of_isBigO_exp_neg` `Nat.instAtLeastTwoHAddOfNat` `one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `ContinuousOn.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Asymptotics.IsLittleO.isBigO` `neg_mul` `one_mul` `rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg` `Real.rpow_one` `add_sub_cancel_right` `mul_comm` `Real.GammaIntegral_convergent` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.neg_add` `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.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Tactic.Linarith.sub_nonpos_of_le`
`integrable_cexp_neg_mul_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.re`	`MeasureTheory.Integrable` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Complex.exp` `Complex.instMul` `Complex.instNeg` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `MeasureTheory.MeasureSpace.volume`	—	`Continuous.comp_aestronglyMeasurable` `Continuous.cexp` `continuous_id'` `MeasureTheory.AEStronglyMeasurable.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.pow` `Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `secondCountable_of_proper` `Complex.instProperSpace` `Complex.continuous_ofReal` `MeasureTheory.hasFiniteIntegral_norm_iff` `norm_cexp_neg_mul_sq` `integrable_exp_neg_mul_sq`
`integrable_exp_neg_mul_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.Integrable` `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` `Real.exp` `Real.instMul` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `MeasureTheory.MeasureSpace.volume`	—	`neg_mul` `Real.rpow_zero` `one_mul` `integrable_rpow_mul_exp_neg_mul_sq` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`integrable_exp_neg_mul_sq_iff` 📖	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` `Real.exp` `Real.instMul` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `MeasureTheory.MeasureSpace.volume` `Real.instLT` `Real.instZero`	—	`integrableOn_Ioi_exp_neg_mul_sq_iff` `MeasureTheory.Integrable.integrableOn` `integrable_exp_neg_mul_sq`
`integrable_mul_cexp_neg_mul_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.re`	`MeasureTheory.Integrable` `Complex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `Complex.instMul` `Complex.ofReal` `Complex.exp` `Complex.instNeg` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `MeasureTheory.MeasureSpace.volume`	—	`Continuous.aestronglyMeasurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `secondCountable_of_proper` `Complex.instProperSpace` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Complex.continuous_ofReal` `Continuous.comp` `Complex.continuous_exp` `Continuous.comp'` `Continuous.fun_mul` `continuous_const` `continuous_id'` `Continuous.pow` `MeasureTheory.Integrable.hasFiniteIntegral` `integrable_mul_exp_neg_mul_sq` `MeasureTheory.hasFiniteIntegral_norm_iff` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_cexp_neg_mul_sq` `Complex.norm_real` `Real.norm_of_nonneg` `LT.lt.le` `Real.exp_pos`
`integrable_mul_exp_neg_mul_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`MeasureTheory.Integrable` `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` `Real.instMul` `Real.exp` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `MeasureTheory.MeasureSpace.volume`	—	`neg_mul` `Real.rpow_one` `integrable_rpow_mul_exp_neg_mul_sq` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike`
`integrable_rpow_mul_exp_neg_mul_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Real.instNeg` `Real.instOne`	`MeasureTheory.Integrable` `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` `Real.instMul` `Real.instPow` `Real.exp` `Monoid.toNatPow` `Real.instMonoid` `MeasureTheory.MeasureSpace.volume`	—	`MeasureTheory.integrableOn_univ` `Set.Iio_union_Ici` `MeasureTheory.integrableOn_union` `PseudoEMetricSpace.pseudoMetrizableSpace` `integrableOn_Ici_iff_integrableOn_Ioi` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Real.noAtoms_volume` `enorm_ne_top` `MeasureTheory.MeasurePreserving.integrableOn_comp_preimage` `MeasureTheory.Measure.measurePreserving_neg` `ContinuousNeg.measurableNeg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `MeasureTheory.Measure.IsAddHaarMeasure.isNegInvariant_of_innerRegular` `instIsTopologicalAddGroupReal` `instIsAddHaarMeasureVolume` `FiniteDimensional.rclike_to_real` `locallyCompact_of_proper` `instProperSpaceReal` `MeasureTheory.Measure.instInnerRegularOfPseudoMetrizableSpaceOfSigmaCompactSpaceOfBorelSpaceOfSigmaFinite` `SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `MeasureTheory.Measure.IsAddHaarMeasure.sigmaFinite` `Homeomorph.measurableEmbedding` `neg_sq` `Set.neg_Iio` `Real.instIsOrderedAddMonoid` `neg_zero` `MeasureTheory.Integrable.mono'` `integrableOn_rpow_mul_exp_neg_mul_sq` `Measurable.aestronglyMeasurable` `Measurable.mul` `ContinuousMul.measurableMul₂` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `Measurable.pow` `Real.hasMeasurablePow` `Measurable.neg` `measurable_id'` `measurable_const` `Measurable.exp` `Measurable.const_mul` `ContinuousMul.measurableMul` `Monoid.measurablePow` `measurableSet_Ioi` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_mem` `Filter.univ_mem'` `le_of_lt` `Real.norm_eq_abs` `abs_mul` `Real.instIsOrderedRing` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `LT.lt.le` `Real.exp_pos` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `abs_neg` `Real.abs_rpow_le_abs_rpow`
`integral_gaussian` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `Real.exp` `Real.instMul` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `Real.sqrt` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.pi`	—	`le_or_gt` `MeasureTheory.integral_undef` `Real.sqrt_eq_zero_of_nonpos` `div_nonpos_of_nonneg_of_nonpos` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `Real.pi_pos` `sq_eq_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `MeasureTheory.integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `le_of_lt` `Real.exp_pos` `Real.sqrt_pos_of_pos` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Complex.ofReal_pow` `Complex.coe_algebraMap` `RCLike.algebraMap_eq_ofReal` `integral_ofReal` `Real.sq_sqrt` `Complex.ofReal_div` `Complex.ofReal_exp` `Complex.ofReal_mul` `Complex.ofReal_neg` `integral_gaussian_sq_complex` `Complex.ofReal_re`
`integral_gaussian_Ioi` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Real.instZero` `Real.exp` `Real.instMul` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.sqrt` `Real.pi` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `le_or_gt` `MeasureTheory.integral_undef` `MeasureTheory.IntegrableOn.eq_1` `integrableOn_Ioi_exp_neg_mul_sq_iff` `not_lt` `Real.sqrt_eq_zero_of_nonpos` `div_nonpos_of_nonneg_of_nonpos` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `LT.lt.le` `Real.pi_pos` `zero_div` `integral_ofReal` `RCLike.algebraMap_eq_ofReal` `Complex.coe_algebraMap` `neg_mul` `Complex.ofReal_exp` `Complex.ofReal_neg` `Complex.ofReal_mul` `Complex.ofReal_pow` `Real.sqrt_eq_rpow` `Complex.ofReal_div` `Complex.ofReal_cpow` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `one_div` `Complex.ofReal_inv` `integral_gaussian_complex_Ioi` `Complex.ofReal_re`
`integral_gaussian_complex` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.re`	`MeasureTheory.integral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `Complex.exp` `Complex.instMul` `Complex.instNeg` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Complex.instPow` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Real.pi` `Complex.instOne` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `IsPreconnected.eq_of_sq_eq` `Nat.instAtLeastTwoHAddOfNat` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IsTopologicalDivisionRing.toContinuousInv₀` `NormedDivisionRing.to_isTopologicalDivisionRing` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `Convex.isPreconnected` `IsTopologicalSemiring.toContinuousAdd` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `convex_halfSpace_re_gt` `continuousOn_of_forall_continuousAt` `continuousAt_gaussian_integral` `ContinuousAt.comp` `continuousAt_cpow_const` `Complex.div_re` `Complex.ofReal_im` `Complex.ofReal_re` `MulZeroClass.zero_mul` `zero_div` `add_zero` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `Real.pi_pos` `Complex.normSq_pos` `ContinuousAt.div` `continuousAt_const` `continuousAt_id` `integral_gaussian_sq_complex` `sq` `Complex.cpow_one` `Complex.cpow_add` `div_ne_zero` `Complex.ofReal_ne_zero` `Real.pi_ne_zero` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.instAtLeastTwo` `Complex.cpow_eq_zero_iff` `not_and_or` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `neg_mul` `one_mul` `Complex.ofReal_exp` `Complex.ofReal_neg` `Complex.ofReal_pow` `integral_ofReal` `Complex.ofReal_one` `Complex.ofReal_div` `Complex.ofReal_ofNat` `Complex.ofReal_cpow` `div_one` `LT.lt.le` `Real.sqrt_eq_rpow` `integral_gaussian`
`integral_gaussian_complex_Ioi` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.re`	`MeasureTheory.integral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Complex.exp` `Complex.instMul` `Complex.instNeg` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instPow` `Real.pi` `Complex.instOne` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `integral_gaussian_complex` `measurableSet_Ioi` `BorelSpace.opensMeasurable` `Real.borelSpace` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `intervalIntegral.integral_comp_sub_left` `neg_mul` `zero_sub` `Complex.ofReal_neg` `Even.neg_pow` `sub_self` `MeasureTheory.intervalIntegral_tendsto_integral_Ioi` `instIsCountablyGenerated_atTop` `instOrderTopologyReal` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `instSecondCountableTopologyReal` `MeasureTheory.Integrable.integrableOn` `integrable_cexp_neg_mul_sq` `Filter.tendsto_id` `MeasureTheory.intervalIntegral_tendsto_integral_Iic` `Filter.tendsto_neg_atTop_atBot` `tendsto_nhds_unique` `Complex.instT2Space` `Filter.atTop_neBot` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `eq_div_iff` `two_ne_zero` `CharZero.NeZero.two` `Complex.instCharZero` `mul_two` `Set.compl_Ioi` `MeasureTheory.integral_add_compl`
`integral_gaussian_sq_complex` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.re`	`Complex` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `MeasureTheory.integral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.MeasureSpace.volume` `Complex.exp` `Complex.instMul` `Complex.instNeg` `Complex.ofReal` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Real.pi`	—	`pow_two` `MeasureTheory.integral_prod_mul` `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` `Complex.exp_add` `mul_add` `Distrib.leftDistribClass` `integral_comp_polarCoord_symm` `Complex.ofReal_mul` `Complex.ofReal_cos` `Complex.ofReal_sin` `MeasureTheory.setIntegral_prod_mul` `mul_one` `one_mul` `Complex.sin_sq_add_cos_sq` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_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.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.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Nat.instAtLeastTwoHAddOfNat` `integral_mul_cexp_neg_mul_sq` `MeasureTheory.integral_const` `Complex.instCompleteSpace` `MeasureTheory.measureReal_restrict_apply` `Set.univ_inter` `Real.volume_real_Ioo_of_le` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.neg_congr` `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.sub_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Real.pi_nonneg` `Mathlib.Meta.NormNum.isNat_lt_true` `RCLike.charZero_rclike` `mul_inv_rev` `sub_neg_eq_add` `Complex.ofReal_add` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNNRat.to_raw_eq` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.div_pf`
`integral_mul_cexp_neg_mul_sq` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Complex.re`	`MeasureTheory.integral` `Complex` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `MeasureTheory.MeasureSpace.toMeasurableSpace` `Real.measureSpace` `MeasureTheory.Measure.restrict` `MeasureTheory.MeasureSpace.volume` `Set.Ioi` `Real.instPreorder` `Complex.instMul` `Complex.ofReal` `Complex.exp` `Complex.instNeg` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.instInv` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Mathlib.Tactic.Contrapose.contrapose₃` `Complex.zero_re` `le_refl` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Nat.instAtLeastTwoHAddOfNat` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `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.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `Mathlib.Meta.NormNum.isNat_eq_false` `Complex.instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `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` `neg_mul` `mul_neg` `neg_mul_neg` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_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` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Meta.NormNum.isNat_natSub` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `HasDerivAt.const_mul` `HasDerivAt.cexp` `hasDerivAt_pow` `Filter.Tendsto.const_mul` `IsTopologicalSemiring.toContinuousMul` `tendsto_zero_iff_norm_tendsto_zero` `norm_cexp_neg_mul_sq` `Filter.Tendsto.comp` `Real.tendsto_exp_atBot` `Filter.Tendsto.const_mul_atTop_of_neg` `Real.instIsStrictOrderedRing` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Filter.tendsto_pow_atTop` `Real.instIsOrderedRing` `two_ne_zero` `MulZeroClass.mul_zero` `zero_pow` `Complex.exp_zero` `sub_neg_eq_add` `zero_add` `MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto'` `Complex.instCompleteSpace` `HasDerivAt.comp_ofReal` `MeasureTheory.Integrable.integrableOn` `integrable_mul_cexp_neg_mul_sq`
`norm_cexp_neg_mul_sq` 📖	mathematical	—	`Norm.norm` `Complex` `Complex.instNorm` `Complex.exp` `Complex.instMul` `Complex.instNeg` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Complex.instSemiring` `Complex.ofReal` `Real.exp` `Real` `Real.instMul` `Real.instNeg` `Complex.re` `Real.instMonoid`	—	`Complex.norm_exp` `Complex.ofReal_pow` `mul_comm` `Complex.re_ofReal_mul` `Complex.neg_re`
`rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instOne` `Real.instZero`	`Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.instMul` `Real.instPow` `Real.exp` `Real.instNeg` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Asymptotics.IsLittleO.trans` `Nat.instAtLeastTwoHAddOfNat` `Asymptotics.IsBigO.mul_isLittleO` `NormedDivisionRing.toNormMulClass` `Asymptotics.isBigO_refl` `exp_neg_mul_rpow_isLittleO_exp_neg` `mul_comm` `Real.Gamma_integrand_isLittleO`
`rpow_mul_exp_neg_mul_sq_isLittleO_exp_neg` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Asymptotics.IsLittleO` `Real.norm` `Filter.atTop` `Real.instPreorder` `Real.instMul` `Real.instPow` `Real.exp` `Real.instNeg` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg` `one_lt_two` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`

---

← Back to Index