Variance

📁 Source: Mathlib/Probability/Moments/Variance.lean

Statistics

Metric	Count
Definitions `evariance`, `variance`, `«termEVar[_;_]»`, `«termEVar[_]»`, `«termVar[_;_]»`, `«termVar[_]»`	6
Theorems `variance_fun_comp`, `evariance_lt_top`, `evariance_ne_top`, `ofReal_variance_eq`, `variance_add`, `variance_fun_add`, `variance_sum`, `covariance_self`, `evariance_congr`, `evariance_def'`, `evariance_eq_lintegral_ofReal`, `evariance_eq_top`, `evariance_eq_top_iff`, `evariance_eq_zero_iff`, `evariance_lt_top`, `evariance_lt_top_iff_memLp`, `evariance_mul`, `evariance_ne_top`, `evariance_zero`, `evariance_zero_measure`, `meas_ge_le_evariance_div_sq`, `meas_ge_le_variance_div_sq`, `ofReal_variance`, `variance_add`, `variance_add_const`, `variance_add_prod`, `variance_congr`, `variance_const_add`, `variance_const_mul`, `variance_const_sub`, `variance_dirac`, `variance_dual_prod`, `variance_dual_prod'`, `variance_eq_integral`, `variance_eq_sub`, `variance_fun_add`, `variance_fun_neg`, `variance_fun_sub`, `variance_fun_sum`, `variance_fun_sum'`, `variance_id_map`, `variance_le_expectation_sq`, `variance_le_sq_of_bounded`, `variance_le_sub_mul_sub`, `variance_map`, `variance_map_equiv`, `variance_mul`, `variance_mul_const`, `variance_neg`, `variance_nonneg`, `variance_of_integral_eq_zero`, `variance_of_not_memLp`, `variance_smul`, `variance_smul'`, `variance_sub`, `variance_sub_const`, `variance_sum`, `variance_sum'`, `variance_zero`, `variance_zero_measure`	60
Total	66

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`variance_fun_comp` 📖	mathematical	`MeasureTheory.MeasurePreserving` `AEMeasurable` `Real` `Real.measurableSpace`	`ProbabilityTheory.variance`	—	`map_eq` `ProbabilityTheory.variance_map` `aemeasurable`

MeasureTheory.MemLp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evariance_lt_top` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ProbabilityTheory.evariance` `Top.top` `instTopENNReal`	—	`ProbabilityTheory.evariance_lt_top`
`evariance_ne_top` 📖	—	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	—	`ProbabilityTheory.evariance_ne_top`
`ofReal_variance_eq` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`ENNReal.ofReal` `ProbabilityTheory.variance` `ProbabilityTheory.evariance`	—	`ProbabilityTheory.ofReal_variance`

ProbabilityTheory

Definitions

Name	Category	Theorems
`evariance` 📖	CompOp	16 math math: `MeasureTheory.MemLp.evariance_lt_top`, `evariance_congr`, `evariance_lt_top_iff_memLp`, `evariance_eq_top_iff`, `evariance_eq_lintegral_ofReal`, `evariance_zero`, `evariance_def'`, `evariance_eq_top`, `evariance_lt_top`, `MeasureTheory.MemLp.ofReal_variance_eq`, `meas_ge_le_evariance_div_sq`, `IdentDistrib.evariance_eq`, `evariance_eq_zero_iff`, `evariance_mul`, `evariance_zero_measure`, `ofReal_variance`
`variance` 📖	CompOp	73 math math: `variance_eq_integral`, `variance_fun_sum'`, `variance_fun_id_gaussianReal`, `hasGaussianLaw_iff_charFunDual_map_eq`, `IsGaussian.map_eq_gaussianReal`, `covarianceBilin_self`, `hasGaussianLaw_iff_charFun_map_eq`, `variance_const_sub`, `centralMoment_two_eq_variance`, `variance_fun_neg`, `variance_of_integral_eq_zero`, `covarianceBilin_apply_basisFun_self`, `variance_le_sub_mul_sub`, `IndepFun.variance_fun_add`, `variance_map_equiv`, `variance_add_const`, `variance_sub`, `IsGaussian.charFunDual_eq_of_forall_strongDual_eq_zero`, `integral_condVar_add_variance_condExp`, `variance_zero_measure`, `isGaussian_iff_charFun_eq`, `variance_eq_sub`, `variance_zero`, `meas_ge_le_variance_div_sq`, `variance_fun_sum`, `IsGaussian.charFunDual_eq`, `variance_continuousLinearMap_gaussianReal`, `variance_le_sq_of_bounded`, `covarianceBilinDual_self_eq_variance`, `variance_mul_const`, `covarianceBilin_real_self`, `variance_add_prod`, `variance_mul`, `HasGaussianLaw.charFun_map_eq`, `variance_nonneg`, `variance_fun_sub`, `variance_congr`, `IdentDistrib.variance_eq`, `variance_map`, `variance_le_expectation_sq`, `variance_add`, `variance_id_gaussianReal`, `IndepFun.variance_add`, `covarianceBilin_real`, `variance_of_not_memLp`, `variance_dual_prod'`, `isGaussian_iff_charFunDual_eq`, `MeasureTheory.MemLp.ofReal_variance_eq`, `HasLaw.variance_eq`, `variance_dirac`, `HasGaussianLaw.charFunDual_map_eq_fun`, `variance_neg`, `condVar_bot`, `variance_const_add`, `variance_sub_const`, `variance_linearMap_gaussianReal`, `IsGaussian.charFunDual_eq_of_integral_eq_zero`, `variance_dual_prod`, `IndepFun.variance_sum`, `IsGaussian.charFun_eq`, `variance_sum'`, `variance_id_map`, `variance_smul'`, `variance_tilted_mul`, `MeasureTheory.MeasurePreserving.variance_fun_comp`, `variance_fun_add`, `HasGaussianLaw.charFunDual_map_eq`, `variance_smul`, `variance_const_mul`, `IsGaussian.eq_gaussianReal`, `variance_sum`, `covariance_self`, `ofReal_variance`
`«termEVar[_;_]»` 📖	CompOp	—
`«termEVar[_]»` 📖	CompOp	—
`«termVar[_;_]»` 📖	CompOp	—
`«termVar[_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`covariance_self` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`covariance` `variance`	—	`covariance.eq_1` `variance_eq_integral` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_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.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_congr` `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.pow_zero`
`evariance_congr` 📖	mathematical	`Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`evariance`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.integral_congr_ae` `MeasureTheory.lintegral_congr_ae` `Filter.mp_mem` `Filter.univ_mem'`
`evariance_def'` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`evariance` `ENNReal` `ENNReal.instSub` `MeasureTheory.lintegral` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENorm.enorm` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `ENNReal.ofReal` `Real.instMonoid` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`Nat.instAtLeastTwoHAddOfNat` `ofReal_variance` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `variance_eq_sub` `ENNReal.ofReal_sub` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `MeasureTheory.lintegral_coe_eq_integral` `nnnorm_pow` `sq_abs` `MeasureTheory.MemLp.integrable_sq` `MeasureTheory.MemLp.abs` `instHasSolidNormReal` `evariance_eq_top` `ENNReal.sub_eq_top_iff` `ENNReal.rpow_natCast` `MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal` `two_ne_zero` `CharZero.NeZero.two` `ENNReal.instCharZero` `ENNReal.ofNat_ne_top` `ENNReal.toReal_ofNat` `one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `MeasureTheory.MemLp.eq_1` `zero_le_two` `ENNReal.ofReal_ne_top`
`evariance_eq_lintegral_ofReal` 📖	mathematical	—	`evariance` `MeasureTheory.lintegral` `ENNReal.ofReal` `Real` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`NormedDivisionRing.to_normOneClass` `NormedDivisionRing.toNormMulClass` `Real.enorm_of_nonneg` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`evariance_eq_top` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.MemLp` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`evariance` `Top.top` `instTopENNReal`	—	`Nat.instAtLeastTwoHAddOfNat` `Continuous.comp_aestronglyMeasurable` `Continuous.sub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `continuous_id'` `continuous_const` `MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal` `two_ne_zero` `CharZero.NeZero.two` `ENNReal.instCharZero` `ENNReal.ofNat_ne_top` `ENNReal.toReal_ofNat` `ENNReal.rpow_two` `ENNReal.rpow_lt_top_of_nonneg` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_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.mul_congr` `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.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `neg_neg_of_pos` `Real.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.instAtLeastTwo` `CancelDenoms.derive_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_sub` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_lt_true` `LT.lt.ne` `lt_top_iff_ne_top` `Pi.add_apply` `sub_add_cancel` `MeasureTheory.MemLp.add` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.memLp_const`
`evariance_eq_top_iff` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`evariance` `Top.top` `ENNReal` `instTopENNReal` `MeasureTheory.MemLp` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `evariance_lt_top_iff_memLp`
`evariance_eq_zero_iff` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`evariance` `ENNReal` `instZeroENNReal` `Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.lintegral_eq_zero_iff'` `AEMeasurable.pow_const` `Monoid.measurablePow` `ENNReal.instMeasurableMul₂` `AEMeasurable.enorm` `BorelSpace.opensMeasurable` `Real.borelSpace` `AEMeasurable.sub_const` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `isReduced_of_noZeroDivisors` `ENNReal.instNoZeroDivisors` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`evariance_lt_top` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `evariance` `Top.top` `instTopENNReal`	—	`Nat.instAtLeastTwoHAddOfNat` `ENNReal.pow_lt_top` `MeasureTheory.MemLp.sub` `MeasureTheory.memLp_const` `ENNReal.rpow_two` `ENNReal.rpow_one` `inv_mul_cancel₀` `two_ne_zero` `CharZero.NeZero.two` `RCLike.charZero_rclike` `ENNReal.rpow_mul` `ENNReal.toReal_ofNat` `one_div` `MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal` `ENNReal.instCharZero` `ENNReal.ofNat_ne_top`
`evariance_lt_top_iff_memLp` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `evariance` `Top.top` `instTopENNReal` `MeasureTheory.MemLp` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Contrapose.contrapose₁` `top_le_iff` `evariance_eq_top` `evariance_lt_top`
`evariance_mul` 📖	mathematical	—	`evariance` `Real` `Real.instMul` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofReal` `Monoid.toNatPow` `Real.instMonoid`	—	`evariance.eq_1` `MeasureTheory.lintegral_const_mul'` `LT.lt.ne` `ENNReal.ofReal_lt_top` `MeasureTheory.integral_const_mul` `mul_sub` `enorm_mul` `NormedDivisionRing.toNormMulClass` `mul_pow` `enorm_pow` `NormedDivisionRing.to_normOneClass` `Real.enorm_of_nonneg` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`evariance_ne_top` 📖	—	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	—	—	`Nat.instAtLeastTwoHAddOfNat` `LT.lt.ne` `evariance_lt_top`
`evariance_zero` 📖	mathematical	—	`evariance` `Pi.instZero` `Real` `Real.instZero` `ENNReal` `instZeroENNReal`	—	`MeasureTheory.integral_zero` `sub_self` `enorm_zero` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.lintegral_const` `MulZeroClass.zero_mul`
`evariance_zero_measure` 📖	mathematical	—	`evariance` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero` `ENNReal` `instZeroENNReal`	—	`MeasureTheory.integral_zero_measure` `sub_zero` `MeasureTheory.lintegral_zero_measure`
`meas_ge_le_evariance_div_sq` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `setOf` `Real.instLE` `NNReal.toReal` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `evariance` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.ofNNReal`	—	`ENNReal.coe_eq_zero` `MeasureTheory.aestronglyMeasurable_const` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal` `two_ne_zero` `CharZero.NeZero.two` `ENNReal.instCharZero` `ENNReal.ofNat_ne_top` `ENNReal.toReal_ofNat` `one_div` `div_eq_mul_inv` `ENNReal.inv_pow` `mul_comm` `ENNReal.rpow_two` `inv_mul_cancel₀` `RCLike.charZero_rclike` `ENNReal.rpow_one` `MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm` `MeasureTheory.AEStronglyMeasurable.sub` `instIsTopologicalAddGroupReal` `MeasureTheory.measure_empty` `MeasureTheory.Measure.instOuterMeasureClass`
`meas_ge_le_variance_div_sq` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Real.instLT` `Real.instZero`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `setOf` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `ENNReal.ofReal` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `variance` `Monoid.toNatPow` `Real.instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `ENNReal.ofReal_div_of_pos` `sq_pos_of_ne_zero` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `LT.lt.ne` `MeasureTheory.MemLp.ofReal_variance_eq` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `ENNReal.ofReal_pow` `LT.lt.le` `meas_ge_le_evariance_div_sq`
`ofReal_variance` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`ENNReal.ofReal` `variance` `evariance`	—	`Nat.instAtLeastTwoHAddOfNat` `variance.eq_1` `ENNReal.ofReal_toReal` `evariance_ne_top`
`variance_add` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Pi.instAdd` `Real.instAdd` `Real.instMul` `Real.instNatCast` `covariance`	—	`Nat.instAtLeastTwoHAddOfNat` `covariance_self` `AEMeasurable.add` `ContinuousAdd.measurableMul₂` `Real.borelSpace` `instSecondCountableTopologyReal` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.MemLp.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `covariance_add_left` `MeasureTheory.MemLp.add` `covariance_add_right` `covariance_comm` `Mathlib.Tactic.Ring.of_eq` `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.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_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`
`variance_add_const` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`variance` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.MemLp.integrable` `one_le_two` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `variance_eq_integral` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace` `MeasureTheory.AEStronglyMeasurable.add_const` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.integral_add` `MeasureTheory.integrable_const` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.probReal_univ` `one_mul` `add_sub_add_right_eq_sub` `variance_of_not_memLp` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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` `MeasureTheory.MemLp.sub` `MeasureTheory.memLp_const`
`variance_add_prod` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Prod.instMeasurableSpace` `Real.instAdd` `MeasureTheory.Measure.prod`	—	`Nat.instAtLeastTwoHAddOfNat` `IndepFun.variance_fun_add` `MeasureTheory.MemLp.comp_fst` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `MeasureTheory.MemLp.comp_snd` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `indepFun_prod₀` `MeasureTheory.MemLp.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace` `MeasureTheory.MeasurePreserving.variance_fun_comp` `MeasureTheory.measurePreserving_fst` `MeasureTheory.measurePreserving_snd`
`variance_congr` 📖	mathematical	`Filter.EventuallyEq` `Real` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`variance`	—	`MeasureTheory.Measure.instOuterMeasureClass` `evariance_congr`
`variance_const_add` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`variance` `Real.instAdd`	—	`add_comm` `variance_add_const`
`variance_const_mul` 📖	mathematical	—	`variance` `Real` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`variance.eq_1` `evariance_mul` `ENNReal.toReal_mul` `ENNReal.toReal_ofReal` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid`
`variance_const_sub` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`variance` `Real.instSub`	—	`sub_eq_add_neg` `variance_const_add` `Continuous.comp_aestronglyMeasurable` `Continuous.neg` `IsTopologicalRing.toContinuousNeg` `instIsTopologicalRingReal` `continuous_id'` `variance_fun_neg`
`variance_dirac` 📖	mathematical	—	`variance` `MeasureTheory.Measure.dirac` `Real` `Real.instZero`	—	`variance_eq_integral` `MeasureTheory.aemeasurable_dirac` `MeasureTheory.integral_dirac` `Real.instCompleteSpace` `sub_self` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`variance_dual_prod` 📖	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`	`variance` `Prod.instMeasurableSpace` `DFunLike.coe` `StrongDual` `Real` `Real.semiring` `Real.pseudoMetricSpace` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `Real.normedField` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `MeasureTheory.Measure.prod` `Real.instAdd` `ContinuousLinearMap` `ContinuousLinearMap.comp` `RingHomCompTriple.ids` `ContinuousLinearMap.inl` `ContinuousLinearMap.inr`	—	`Nat.instAtLeastTwoHAddOfNat` `variance_dual_prod'` `ContinuousLinearMap.comp_memLp'` `RingHomIsometric.ids` `RingHomCompTriple.ids`
`variance_dual_prod'` 📖	mathematical	`MeasureTheory.MemLp` `Real` `ContinuousENorm.toENorm` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `Real.pseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `Real.semiring` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NormedSpace.toModule` `Real.normedField` `Semiring.toModule` `ContinuousLinearMap.funLike` `ContinuousLinearMap.comp` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `RingHomCompTriple.ids` `ContinuousLinearMap.inl` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `ContinuousLinearMap.inr`	`variance` `Prod.instMeasurableSpace` `StrongDual` `MeasureTheory.Measure.prod` `Real.instAdd`	—	`RingHomCompTriple.ids` `Nat.instAtLeastTwoHAddOfNat` `ContinuousLinearMap.comp_inl_add_comp_inr` `variance_add_prod`
`variance_eq_integral` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`variance` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Monoid.toNatPow` `Real.instMonoid` `Real.instSub`	—	`MeasureTheory.integral_toReal` `AEMeasurable.pow_const` `Monoid.measurablePow` `ENNReal.instMeasurableMul₂` `AEMeasurable.enorm` `BorelSpace.opensMeasurable` `Real.borelSpace` `AEMeasurable.sub_const` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.pow_lt_top` `enorm_lt_top` `ENNReal.toReal_pow` `toReal_enorm` `sq_abs`
`variance_eq_sub` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Real.instSub` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Monoid.toNatPow` `Pi.monoid` `Real.instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `covariance_self` `MeasureTheory.MemLp.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace` `covariance_eq_sub` `pow_two`
`variance_fun_add` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Real.instAdd` `Real.instMul` `Real.instNatCast` `covariance`	—	`Nat.instAtLeastTwoHAddOfNat` `variance_add`
`variance_fun_neg` 📖	mathematical	—	`variance` `Real` `Real.instNeg`	—	`Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.atom_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.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `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` `Even.neg_pow` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `one_mul` `variance_const_mul`
`variance_fun_sub` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Real.instSub` `Real.instAdd` `Real.instMul` `Real.instNatCast` `covariance`	—	`Nat.instAtLeastTwoHAddOfNat` `variance_sub`
`variance_fun_sum` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Finset.sum` `Real.instAddCommMonoid` `Finset.univ` `covariance`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_apply` `variance_sum`
`variance_fun_sum'` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Finset.sum` `Real.instAddCommMonoid` `covariance`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_apply` `variance_sum'`
`variance_id_map` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace`	`variance` `MeasureTheory.Measure.map`	—	`variance_map` `Measurable.aemeasurable` `measurable_id` `CompTriple.comp_eq` `CompTriple.instId_comp` `CompTriple.instIsIdId`
`variance_le_expectation_sq` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`Real.instLE` `variance` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Monoid.toNatPow` `Pi.monoid` `Real.instMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `variance_eq_sub` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `variance.eq_1` `evariance_eq_lintegral_ofReal` `MeasureTheory.integral_eq_lintegral_of_nonneg_ae` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `sq_nonneg` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `AEMeasurable.pow_const` `Monoid.measurablePow` `ContinuousMul.measurableMul₂` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `AEMeasurable.sub_const` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `MeasureTheory.integral_undef` `MeasureTheory.memLp_two_iff_integrable_sq` `MeasureTheory.AEStronglyMeasurable.sub` `MeasureTheory.aestronglyMeasurable_const` `MeasureTheory.memLp_const` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `sub_add_cancel` `MeasureTheory.MemLp.add` `IsTopologicalSemiring.toContinuousAdd` `MeasureTheory.integral_nonneg` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `sub_zero` `le_rfl`
`variance_le_sq_of_bounded` 📖	mathematical	`Filter.Eventually` `Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `AEMeasurable` `Real.measurableSpace`	`Real.instLE` `variance` `Monoid.toNatPow` `Real.instMonoid` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instSub` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Nat.instAtLeastTwoHAddOfNat` `variance_le_sub_mul_sub` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_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.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.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.pow_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` `RCLike.charZero_rclike` `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.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.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Meta.NormNum.IsRat.to_isInt` `Mathlib.Meta.NormNum.isNNRat_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `sub_le_self` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sq_nonneg` `AddGroup.existsAddOfLE` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing`
`variance_le_sub_mul_sub` 📖	mathematical	`Filter.Eventually` `Real` `Set` `Set.instMembership` `Set.Icc` `Real.instPreorder` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `AEMeasurable` `Real.measurableSpace`	`Real.instLE` `variance` `Real.instMul` `Real.instSub` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.Eventually.mono` `MeasureTheory.Integrable.neg` `MeasureTheory.MemLp.integrable_sq` `MeasureTheory.memLp_of_bounded` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Integrable.const_mul` `MeasureTheory.Integrable.mono'` `MeasureTheory.integrable_const` `Filter.mp_mem` `Filter.univ_mem'` `abs_le_max_abs_abs` `Real.instIsOrderedAddMonoid` `MeasureTheory.integral_nonneg_of_ae` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `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.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` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_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_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `MeasureTheory.integral_congr_ae` `MeasureTheory.ae_of_all` `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.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `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` `MeasureTheory.integral_sub` `MeasureTheory.Integrable.add''` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `MeasureTheory.integral_const` `Real.instCompleteSpace` `MeasureTheory.probReal_univ` `one_mul` `MeasureTheory.integral_add` `variance_eq_sub`
`variance_map` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `MeasureTheory.Measure.map`	`variance`	—	`variance_eq_integral` `MeasureTheory.integral_map` `MeasureTheory.AEStronglyMeasurable.pow` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `AEMeasurable.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `AEMeasurable.sub_const` `ContinuousSub.measurableSub` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `AEMeasurable.comp_aemeasurable`
`variance_map_equiv` 📖	mathematical	—	`variance` `MeasureTheory.Measure.map` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `Real`	—	`MeasureTheory.lintegral_map_equiv` `MeasureTheory.integral_map_equiv`
`variance_mul` 📖	mathematical	—	`variance` `Real` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`variance_const_mul`
`variance_mul_const` 📖	mathematical	—	`variance` `Real` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`mul_comm` `variance_const_mul`
`variance_neg` 📖	mathematical	—	`variance` `Pi.instNeg` `Real` `Real.instNeg`	—	`variance_fun_neg`
`variance_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `variance`	—	`ENNReal.toReal_nonneg`
`variance_of_integral_eq_zero` 📖	mathematical	`AEMeasurable` `Real` `Real.measurableSpace` `MeasureTheory.integral` `Real.normedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `RCLike.toInnerProductSpaceReal` `Real.instZero`	`variance` `Monoid.toNatPow` `Real.instMonoid`	—	`variance_eq_integral` `sub_zero`
`variance_of_not_memLp` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MeasureTheory.MemLp` `ContinuousENorm.toENorm` `SeminormedAddGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `SeminormedAddGroup.toContinuousENorm` `ENNReal` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Real.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `evariance_eq_top_iff`
`variance_smul` 📖	mathematical	—	`variance` `Real` `Function.hasSMul` `Algebra.toSMul` `Real.instCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid`	—	`variance_const_mul`
`variance_smul'` 📖	mathematical	—	`variance` `Function.hasSMul` `Real` `Algebra.toSMul` `Real.semiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	—	`algebraMap_smul` `Pi.isScalarTower` `IsScalarTower.right` `Algebra.smul_def` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `variance_smul`
`variance_sub` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Pi.instSub` `Real.instSub` `Real.instAdd` `Real.instMul` `Real.instNatCast` `covariance`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_add_neg` `variance_add` `MeasureTheory.MemLp.neg` `variance_neg` `covariance_neg_right` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `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.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.sub_pf`
`variance_sub_const` 📖	mathematical	`MeasureTheory.AEStronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace`	`variance` `Real.instSub`	—	`sub_eq_add_neg` `variance_add_const`
`variance_sum` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `Finset.univ` `covariance`	—	`Nat.instAtLeastTwoHAddOfNat` `variance_sum'`
`variance_sum'` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat`	`variance` `Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid` `covariance`	—	`Nat.instAtLeastTwoHAddOfNat` `covariance_self` `MeasureTheory.MemLp.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace` `MeasureTheory.memLp_finset_sum'` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `covariance_sum_left'` `Finset.sum_congr` `covariance_sum_right'`
`variance_zero` 📖	mathematical	—	`variance` `Pi.instZero` `Real` `Real.instZero`	—	`evariance_zero`
`variance_zero_measure` 📖	mathematical	—	`variance` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero` `Real` `Real.instZero`	—	`evariance_zero_measure`

ProbabilityTheory.IndepFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`variance_add` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `ProbabilityTheory.IndepFun` `Real.measurableSpace`	`ProbabilityTheory.variance` `Pi.instAdd` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.variance_congr` `Filter.EventuallyEq.add_right` `zero_add` `ProbabilityTheory.variance_zero` `MeasureTheory.MemLp.isProbabilityMeasure_of_indepFun` `BorelSpace.opensMeasurable` `Real.borelSpace` `ENNReal.instCharZero` `ProbabilityTheory.variance_add` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `covariance_eq_zero` `MulZeroClass.mul_zero` `add_zero`
`variance_fun_add` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `ProbabilityTheory.IndepFun` `Real.measurableSpace`	`ProbabilityTheory.variance` `Real.instAdd`	—	`Nat.instAtLeastTwoHAddOfNat` `variance_add`
`variance_sum` 📖	mathematical	`MeasureTheory.MemLp` `Real` `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` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Nat.instAtLeastTwoHAddOfNat` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `ProbabilityTheory.IndepFun` `Real.measurableSpace`	`ProbabilityTheory.variance` `Finset.sum` `Pi.addCommMonoid` `Real.instAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.Measure.instOuterMeasureClass` `ProbabilityTheory.variance_congr` `Filter.mp_mem` `MeasureTheory.ae_all_iff` `Finite.to_countable` `Finite.of_fintype` `Filter.univ_mem'` `Finset.sum_apply` `Finset.sum_eq_zero` `ProbabilityTheory.variance_zero` `not_forall₂` `Finset.eq_singleton_or_nontrivial` `Finset.sum_singleton` `Finset.Nontrivial.exists_ne` `MeasureTheory.MemLp.isProbabilityMeasure_of_indepFun` `BorelSpace.opensMeasurable` `Real.borelSpace` `ENNReal.instCharZero` `ProbabilityTheory.variance_sum'` `MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure` `MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure` `Finset.sum_congr` `ProbabilityTheory.covariance_self` `MeasureTheory.MemLp.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Finset.sum_eq_single_of_mem` `covariance_eq_zero`

---

← Back to Index