Documentation Verification Report

Fernique

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

Statistics

Metric	Count
Definitions	0
Theorems `charFunDual_eq_of_forall_strongDual_eq_zero`, `charFunDual_eq_of_integral_eq_zero`, `eq_dirac_of_variance_eq_zero`, `exists_integrable_exp_sq`, `integrable_exp_sq_of_conv_neg`, `integrable_fun_id`, `integrable_id`, `integral_dual`, `integral_dual_conv_map_neg_eq_zero`, `map_rotation_eq_self`, `map_rotation_eq_self_of_forall_strongDual_eq_zero`, `memLp_id`, `memLp_two_fun_id`, `memLp_two_id`, `noAtoms`	15
Total	15

ProbabilityTheory.IsGaussian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`charFunDual_eq_of_forall_strongDual_eq_zero` 📖	mathematical	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instZero`	`MeasureTheory.charFunDual` `Complex.exp` `Complex` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNeg` `Complex.ofReal` `ProbabilityTheory.variance` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `charFunDual_eq` `integral_complex_ofReal` `MulZeroClass.zero_mul` `zero_sub` `neg_div`
`charFunDual_eq_of_integral_eq_zero` 📖	mathematical	`MeasureTheory.integral` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`MeasureTheory.charFunDual` `Complex.exp` `Complex` `DivInvMonoid.toDiv` `Complex.instDivInvMonoid` `Complex.instNeg` `Complex.ofReal` `ProbabilityTheory.variance` `DFunLike.coe` `StrongDual` `Real` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `instOfNatAtLeastTwo` `Complex.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`charFunDual_eq_of_forall_strongDual_eq_zero` `integral_dual` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`eq_dirac_of_variance_eq_zero` 📖	mathematical	`ProbabilityTheory.variance` `DFunLike.coe` `StrongDual` `Real` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instZero`	`MeasureTheory.Measure.dirac` `MeasureTheory.integral`	—	`MeasureTheory.Measure.ext_of_charFunDual` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `toIsProbabilityMeasure` `MeasureTheory.Measure.dirac.instIsFiniteMeasure` `MeasureTheory.charFunDual_dirac` `BorelSpace.opensMeasurable` `Nat.instAtLeastTwoHAddOfNat` `charFunDual_eq` `integral_complex_ofReal` `integral_dual` `zero_div` `sub_zero`
`exists_integrable_exp_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` `Real.exp` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self` `MeasureTheory.Measure.finite_of_finite_conv` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `toIsProbabilityMeasure` `MeasureTheory.Measure.isFiniteMeasure_map` `map_rotation_eq_self_of_forall_strongDual_eq_zero` `ProbabilityTheory.isGaussian_conv` `ProbabilityTheory.isGaussian_map_equiv` `integral_dual_conv_map_neg_eq_zero` `Nat.instAtLeastTwoHAddOfNat` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `integrable_exp_sq_of_conv_neg`
`integrable_exp_sq_of_conv_neg` 📖	—	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Real.exp` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Norm.norm` `NormedAddCommGroup.toNorm` `MeasureTheory.Measure.conv` `ESeminormedAddMonoid.toAddMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.map` `DFunLike.coe` `ContinuousLinearEquiv` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.neg` `IsTopologicalAddGroup.toContinuousNeg` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Real.instLT` `Real.instZero`	—	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.integrable_conv_iff` `ContinuousAdd.measurableMul₂` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.Measure.instSFiniteMap` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `toIsProbabilityMeasure` `Continuous.comp_aestronglyMeasurable` `Continuous.rexp` `continuous_id'` `MeasureTheory.AEStronglyMeasurable.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.pow` `MeasureTheory.AEStronglyMeasurable.norm` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Filter.mp_mem` `Filter.univ_mem'` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `norm_sub_rev` `MeasureTheory.integrable_map_measure` `MeasureTheory.AEStronglyMeasurable.const_add` `MeasureTheory.StronglyMeasurable.aemeasurable` `MeasureTheory.StronglyMeasurable.neg` `stronglyMeasurable_id` `Filter.Eventually.exists` `MeasureTheory.Measure.ae.neBot` `MeasureTheory.IsProbabilityMeasure.neZero` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.exp_add` `Real.exp_monotone` `sub_add_cancel` `le_imp_le_of_le_of_le` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `norm_nonneg` `norm_add_le` `le_refl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `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.Meta.NormNum.IsNat.of_raw` `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.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Meta.NormNum.instAtLeastTwo` `add_assoc` `add_le_add_right` `two_mul_le_add_mul_sq` `Mathlib.Tactic.Ring.div_congr` `Mathlib.Tactic.Ring.sub_congr` `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.Tactic.Ring.neg_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` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Tactic.Ring.inv_congr` `Mathlib.Tactic.Ring.atom_pf'` `Nat.cast_one` `mul_le_mul_of_nonneg_left` `le_of_lt` `MeasureTheory.integrable_of_le_of_le` `MeasureTheory.ae_of_all` `Real.exp_pos` `MeasureTheory.integrable_const` `MeasureTheory.Integrable.const_mul`
`integrable_fun_id` 📖	mathematical	—	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`integrable_id`
`integrable_id` 📖	mathematical	—	`MeasureTheory.Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`MeasureTheory.memLp_one_iff_integrable` `memLp_id`
`integral_dual` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	—	`ContinuousLinearMap.integral_comp_comm` `Real.instCompleteSpace` `MeasureTheory.MemLp.integrable` `le_rfl` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `toIsProbabilityMeasure` `memLp_id`
`integral_dual_conv_map_neg_eq_zero` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `MeasureTheory.Measure.conv` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `MeasureTheory.Measure.map` `DFunLike.coe` `ContinuousLinearEquiv` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `EquivLike.toFunLike` `ContinuousLinearEquiv.equivLike` `ContinuousLinearEquiv.neg` `IsTopologicalAddGroup.toContinuousNeg` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `StrongDual` `Real.pseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ContinuousLinearMap.funLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instZero`	—	`RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousNeg` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `MeasureTheory.integral_conv` `ContinuousAdd.measurableMul₂` `IsTopologicalAddGroup.toContinuousAdd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `toIsProbabilityMeasure` `MeasureTheory.Measure.instSFiniteMap` `integrable_dual` `ProbabilityTheory.isGaussian_conv` `ProbabilityTheory.isGaussian_map_equiv` `map_add` `SemilinearMapClass.toAddHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `MeasureTheory.integral_add` `MeasureTheory.integrable_const` `MeasureTheory.Measure.isFiniteMeasure_map` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.probReal_univ` `one_mul` `MeasureTheory.integral_map` `Continuous.aemeasurable` `BorelSpace.opensMeasurable` `ContinuousMapClass.map_continuous` `ContinuousSemilinearMapClass.toContinuousMapClass` `ContinuousSemilinearEquivClass.continuousSemilinearMapClass` `ContinuousLinearEquiv.continuousSemilinearEquivClass` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `secondCountableTopologyEither_of_right` `instSecondCountableTopologyReal` `Continuous.clm_apply` `continuous_const` `continuous_id'` `ContinuousLinearEquiv.neg_apply` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `MeasureTheory.integral_neg` `add_neg_cancel`
`map_rotation_eq_self` 📖	mathematical	`MeasureTheory.integral` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`MeasureTheory.Measure.map` `Prod.instMeasurableSpace` `DFunLike.coe` `ContinuousLinearMap` `Real` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `ContinuousLinearMap.rotation` `MeasureTheory.Measure.prod`	—	`map_rotation_eq_self_of_forall_strongDual_eq_zero` `integral_dual` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass`
`map_rotation_eq_self_of_forall_strongDual_eq_zero` 📖	mathematical	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DFunLike.coe` `StrongDual` `Real.semiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instZero`	`MeasureTheory.Measure.map` `Prod.instMeasurableSpace` `ContinuousLinearMap` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `ContinuousLinearMap.rotation` `MeasureTheory.Measure.prod`	—	`MeasureTheory.Measure.ext_of_charFunDual` `Prod.borelSpace` `secondCountableTopologyEither_of_right` `TopologicalSpace.instSecondCountableTopologyProd` `CompleteSpace.prod` `MeasureTheory.Measure.isFiniteMeasure_map` `MeasureTheory.Measure.prod.instIsFiniteMeasure` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `toIsProbabilityMeasure` `RingHomCompTriple.ids` `MeasureTheory.charFunDual_map` `Prod.opensMeasurableSpace` `BorelSpace.opensMeasurable` `MeasureTheory.charFunDual_prod` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.sigmaFinite_of_locallyFinite` `MeasureTheory.IsFiniteMeasure.toIsLocallyFiniteMeasure` `Nat.instAtLeastTwoHAddOfNat` `charFunDual_eq_of_forall_strongDual_eq_zero` `add_div` `neg_add` `instIsTopologicalAddGroupReal` `Algebra.to_smulCommClass` `UniformContinuousConstSMul.to_continuousConstSMul` `Ring.uniformContinuousConstSMul` `instIsUniformAddGroupReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `ContinuousLinearMap.ext` `smul_zero` `add_zero` `ContinuousLinearMap.comp_inl_add_comp_inr` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `neg_mul` `RingHomIsometric.ids` `sub_eq_add_neg` `IsTopologicalSemiring.toContinuousAdd` `zero_add` `ProbabilityTheory.variance_sub` `MeasureTheory.MemLp.const_smul` `Real.isBoundedSMul` `memLp_dual` `ProbabilityTheory.variance_smul` `ProbabilityTheory.variance_add` `ProbabilityTheory.covariance_smul_left` `ProbabilityTheory.covariance_smul_right` `Real.cos_sq_add_sin_sq`
`memLp_id` 📖	mathematical	—	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Nat.instAtLeastTwoHAddOfNat` `CanLift.prf` `ENNReal.canLift` `ENNReal.coe_div` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing` `ProbabilityTheory.memLp_of_mem_interior_integrableExpSet` `exists_integrable_exp_sq` `MeasureTheory.integrable_of_le_of_le` `Continuous.comp_aestronglyMeasurable` `Continuous.rexp` `continuous_id'` `MeasureTheory.AEStronglyMeasurable.const_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.pow` `MeasureTheory.AEStronglyMeasurable.norm` `aestronglyMeasurable_id` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `MeasureTheory.ae_of_all` `MeasureTheory.Measure.instOuterMeasureClass` `le_of_lt` `Real.exp_pos` `Filter.univ_mem'` `neg_mul` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `even_two_mul` `MeasureTheory.integrable_const` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `toIsProbabilityMeasure` `IsOpen.subset_interior_iff` `isOpen_Ioo` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `ProbabilityTheory.integrable_exp_mul_of_le_of_le` `LT.lt.le` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `MeasureTheory.memLp_norm_rpow_iff` `ENNReal.instCharZero` `ENNReal.toReal_ofNat` `Real.rpow_ofNat`
`memLp_two_fun_id` 📖	mathematical	—	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`memLp_two_id`
`memLp_two_id` 📖	mathematical	—	`MeasureTheory.MemLp` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`memLp_id` `Nat.instAtLeastTwoHAddOfNat`
`noAtoms` 📖	mathematical	—	`MeasureTheory.NoAtoms`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `eq_dirac_of_variance_eq_zero` `map_eq_gaussianReal` `ProbabilityTheory.noAtoms_gaussianReal` `lt_of_le_of_ne` `ProbabilityTheory.variance_nonneg` `MeasureTheory.NoAtoms.measure_singleton` `MeasureTheory.measure_mono_null` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.map_apply` `ContinuousLinearMap.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`

---

← Back to Index