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 NormedAddCommGroup.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 SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal IsSemitopologicalSemiring.toContinuousAdd 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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_add Continuous.prodMk Continuous.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuous_mul_const Complex.continuous_ofReal Continuous.clm_apply continuous_const RingHomIsometric.ids ContinuousLinearMap.continuous Continuous.fst Continuous.snd 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 SeparatingDual.eq_iff_forall_dual_eq instSeparatingDualRealOfIsTopologicalAddGroupOfContinuousSMulOfLocallyConvexSpaceOfT1Space IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul NormedSpace.toLocallyConvexSpace T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace MulZeroClass.mul_zero Complex.div_ofNat_re zero_sub RCLike.charZero_rclike Complex.div_ofNat_im sub_zero 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 NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup 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 Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	MeasureTheory.integral InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup covarianceBilin	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Nat.instAtLeastTwoHAddOfNat RingHomIsometric.ids RingHomCompTriple.right_ids IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup RingHomInvPair.instStarRingEnd IsTopologicalAddGroup.toContinuousAdd smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul 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 ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring Real.pseudoMetricSpace Real.instAddCommMonoid NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing RCLike.toInnerProductSpaceReal ContinuousLinearMap.topologicalSpace NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul LinearMap.BilinForm.IsPosSemidef Semifield.toCommSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid 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.funLike instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Nat.instAtLeastTwoHAddOfNat isGaussian_iff_gaussian_charFunDual RingHomIsometric.ids RingHomCompTriple.right_ids 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 UniformContinuousConstSMul.to_continuousConstSMul 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 ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring StrongDual Real.pseudoMetricSpace ContinuousLinearMap.topologicalSpace NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup Semiring.toModule instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousLinearMap.addCommGroup Real.instRing LinearMap.BilinForm.IsPosSemidef Semifield.toCommSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid Real.instLE ContinuousLinearMap.toBilinForm MeasureTheory.charFunDual Complex.exp Complex Complex.instSub Complex.instMul Complex.ofReal DFunLike.coe ContinuousLinearMap.funLike Complex.I DivInvMonoid.toDiv Complex.instDivInvMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing 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 SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ContinuousLinearMap.addCommGroup Real.instRing ProbabilityTheory.covarianceBilinDual instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ProbabilityTheory.covarianceBilin instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul MeasureTheory.Measure.ext_of_charFun MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure toIsProbabilityMeasure Nat.instAtLeastTwoHAddOfNat charFun_eq'
ext_covarianceBilinDual 📖	—	MeasureTheory.integral ProbabilityTheory.covarianceBilinDual	—	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul 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 IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ProbabilityTheory.covarianceBilin.congr_simp ext
ext_iff_covarianceBilinDual 📖	mathematical	—	MeasureTheory.integral ProbabilityTheory.covarianceBilinDual	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul ProbabilityTheory.covarianceBilinDual.congr_simp ext_covarianceBilinDual

---

← Back to Index