CharFun

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

Statistics

Metric	Count
Definitions	0
Theorems charFunDual_eq', charFun_eq', ext, ext_covarianceBilinDual, ext_iff, ext_iff_covarianceBilinDual, gaussian_charFunDual_congr, gaussian_charFun_congr, isGaussian_iff_gaussian_charFun, isGaussian_iff_gaussian_charFunDual	10
Total	10

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gaussian_charFunDual_congr 📖	mathematical	LinearMap.BilinForm.IsPosSemidef Real StrongDual Real.semiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField Semifield.toCommSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommGroup Real.instRing SeminormedAddCommGroup.toAddCommGroup Real.instAddCommGroup Semiring.toModule RingHom.id Semiring.toNonAssocSemiring instIsTopologicalAddGroupReal ContinuousLinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.instLE ContinuousLinearMap.toBilinForm ContinuousLinearMap.topologicalSpace MeasureTheory.charFunDual Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal DFunLike.coe ContinuousLinearMap.funLike Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid ContinuousLinearMap ContinuousLinearMap.addCommMonoid Real.instAddCommMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	MeasureTheory.integral covarianceBilinDual	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat isGaussian_iff_gaussian_charFunDual Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg 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_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.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.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.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt 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 Isometry.comp_continuous_iff Complex.isometry_intCast Continuous.comp' Continuous.div_const IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_id' Continuous.fun_add Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup Continuous.fun_mul continuous_const Complex.continuous_ofReal Continuous.clm_apply RingHomIsometric.ids ContinuousLinearMap.continuous Continuous.fst Continuous.snd Continuous.prodMk IsLocallyConstant.eq_const ConnectedSpace.toPreconnectedSpace PathConnectedSpace.connectedSpace NormedSpace.instPathConnectedSpace IsLocallyConstant.iff_continuous instDiscreteTopologyInt MulZeroClass.zero_mul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass zero_div sub_self add_zero Int.cast_zero NormedSpace.eq_iff_forall_dual_eq MulZeroClass.mul_zero Complex.div_ofNat_re zero_sub RCLike.charZero_rclike Complex.div_ofNat_im sub_zero SeminormedAddCommGroup.to_isUniformAddGroup LinearMap.BilinForm.ext_of_isSymm CharZero.NeZero.two LinearMap.BilinForm.IsPosSemidef.isSymm isPosSemidef_covarianceBilinDual covarianceBilinDual_self_eq_variance IsGaussian.memLp_two_id IsGaussian.charFunDual_eq'
gaussian_charFun_congr 📖	mathematical	LinearMap.BilinForm.IsPosSemidef Real Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup NormedAddCommGroup.toSeminormedAddCommGroup NormedSpace.toModule InnerProductSpace.toNormedSpace Real.instRCLike Real.instLE ContinuousLinearMap.toBilinForm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace MeasureTheory.charFun InnerProductSpace.toInner Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal Inner.inner Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	MeasureTheory.integral covarianceBilin	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat RingHomIsometric.ids RingHomCompTriple.right_ids SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.instStarRingEnd IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul InnerProductSpace.toDual_symm_apply LinearMap.BilinForm.IsSymm.eq LinearMap.BilinForm.IsPosSemidef.isSymm LinearMap.BilinForm.IsNonneg.nonneg LinearMap.BilinForm.IsPosSemidef.isNonneg gaussian_charFunDual_congr ContinuousLinearMap.ext ContinuousLinearMap.bilinearComp.congr_simp LinearIsometryEquiv.symm_apply_apply
isGaussian_iff_gaussian_charFun 📖	mathematical	—	IsGaussian UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike LinearMap.BilinForm.IsPosSemidef Semifield.toCommSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real.instLE ContinuousLinearMap.toBilinForm MeasureTheory.charFun InnerProductSpace.toInner Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal Inner.inner Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Real.pseudoMetricSpace Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat isGaussian_iff_gaussian_charFunDual RingHomIsometric.ids RingHomCompTriple.right_ids SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup LinearMap.BilinForm.IsSymm.eq LinearMap.BilinForm.IsPosSemidef.isSymm LinearMap.BilinForm.IsNonneg.nonneg LinearMap.BilinForm.IsPosSemidef.isNonneg IsTopologicalAddGroup.toContinuousAdd smulCommClass_self IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul MeasureTheory.charFun_eq_charFunDual_toDualMap RingHomInvPair.instStarRingEnd InnerProductSpace.toDual_symm_apply
isGaussian_iff_gaussian_charFunDual 📖	mathematical	—	IsGaussian UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real Real.normedField LinearMap.BilinForm.IsPosSemidef StrongDual Real.semiring Real.pseudoMetricSpace Semifield.toCommSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ContinuousLinearMap.addCommGroup Real.instRing SeminormedAddCommGroup.toAddCommGroup Real.instAddCommGroup Semiring.toModule RingHom.id Semiring.toNonAssocSemiring instIsTopologicalAddGroupReal ContinuousLinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.instLE ContinuousLinearMap.toBilinForm ContinuousLinearMap.topologicalSpace MeasureTheory.charFunDual Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal DFunLike.coe ContinuousLinearMap.funLike Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid ContinuousLinearMap ContinuousLinearMap.addCommMonoid Real.instAddCommMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat isPosSemidef_covarianceBilinDual IsGaussian.charFunDual_eq' isGaussian_of_map_eq_gaussianReal BorelSpace.opensMeasurable MeasureTheory.Measure.ext_of_charFun Real.borelSpace instSecondCountableTopologyReal Real.instCompleteSpace MeasureTheory.Measure.isFiniteMeasure_map MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureGaussianReal MeasureTheory.charFun_map_eq_charFunDual_smul charFun_gaussianReal map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Real.coe_toNNReal LinearMap.BilinForm.IsNonneg.nonneg LinearMap.BilinForm.IsPosSemidef.isNonneg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_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.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.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.Tactic.Ring.pow_congr 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

ProbabilityTheory.IsGaussian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charFunDual_eq' 📖	mathematical	—	MeasureTheory.charFunDual Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal 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 MeasureTheory.integral Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid ContinuousLinearMap ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instAddCommMonoid ContinuousLinearMap.module NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousLinearMap.addCommGroup ProbabilityTheory.covarianceBilinDual instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat charFunDual_eq ProbabilityTheory.covarianceBilinDual_self_eq_variance MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure toIsProbabilityMeasure memLp_two_id integral_complex_ofReal ContinuousLinearMap.integral_comp_id_comm' Real.instCompleteSpace integrable_id
charFun_eq' 📖	mathematical	—	MeasureTheory.charFun InnerProductSpace.toInner Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal Inner.inner MeasureTheory.integral InnerProductSpace.toNormedSpace Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace SeminormedAddCommGroup.toAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ProbabilityTheory.covarianceBilin instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul Nat.instAtLeastTwoHAddOfNat charFun_eq ProbabilityTheory.covarianceBilin_self MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure toIsProbabilityMeasure memLp_two_id integral_complex_ofReal integral_inner integrable_id
ext 📖	—	MeasureTheory.integral InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup ProbabilityTheory.covarianceBilin	—	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul MeasureTheory.Measure.ext_of_charFun MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure toIsProbabilityMeasure Nat.instAtLeastTwoHAddOfNat charFun_eq'
ext_covarianceBilinDual 📖	—	MeasureTheory.integral ProbabilityTheory.covarianceBilinDual	—	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul MeasureTheory.Measure.ext_of_charFunDual MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure toIsProbabilityMeasure Nat.instAtLeastTwoHAddOfNat charFunDual_eq'
ext_iff 📖	mathematical	—	MeasureTheory.integral InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup ProbabilityTheory.covarianceBilin	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul ProbabilityTheory.covarianceBilin.congr_simp ext
ext_iff_covarianceBilinDual 📖	mathematical	—	MeasureTheory.integral ProbabilityTheory.covarianceBilinDual	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul ProbabilityTheory.covarianceBilinDual.congr_simp ext_covarianceBilinDual

---

← Back to Index