KLFun

📁 Source: Mathlib/InformationTheory/KullbackLeibler/KLFun.lean

Statistics

Metric	Count
Definitions klFun	1
Theorems continuous_klFun, convexOn_Ioi_klFun, convexOn_klFun, deriv_klFun, hasDerivAt_klFun, integrable_klFun_rnDeriv_iff, integral_klFun_rnDeriv, isMinOn_klFun, klFun_apply, klFun_eq_zero_iff, klFun_nonneg, klFun_one, klFun_zero, leftDeriv_klFun, leftDeriv_klFun_one, measurable_klFun, not_differentiableAt_klFun_zero, not_differentiableWithinAt_klFun_Iio_zero, not_differentiableWithinAt_klFun_Ioi_zero, rightDeriv_klFun, rightDeriv_klFun_one, strictConvexOn_klFun, stronglyMeasurable_klFun, tendsto_klFun_atTop, tendsto_rightDeriv_klFun_atTop	25
Total	26

InformationTheory

Definitions

Name	Category	Theorems
klFun 📖	CompOp	29 math math: integrable_klFun_rnDeriv_iff, klFun_eq_zero_iff, tendsto_klFun_atTop, klFun_apply, leftDeriv_klFun_one, not_differentiableWithinAt_klFun_Iio_zero, toReal_klDiv_eq_integral_klFun, measurable_klFun, tendsto_rightDeriv_klFun_atTop, hasDerivAt_klFun, leftDeriv_klFun, integral_klFun_rnDeriv, klDiv_eq_lintegral_klFun, klDiv_eq_integral_klFun, convexOn_klFun, klFun_zero, klFun_nonneg, isMinOn_klFun, rightDeriv_klFun_one, rightDeriv_klFun, klFun_one, strictConvexOn_klFun, continuous_klFun, stronglyMeasurable_klFun, not_differentiableWithinAt_klFun_Ioi_zero, convexOn_Ioi_klFun, not_differentiableAt_klFun_zero, deriv_klFun, mul_klFun_le_toReal_klDiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_klFun 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun	—	Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Continuous.fun_add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.continuous_mul_log continuous_const continuous_id'
convexOn_Ioi_klFun 📖	mathematical	—	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ioi Real.instPreorder Real.instZero klFun	—	ConvexOn.subset convexOn_klFun Set.Ioi_subset_Ici le_rfl convex_Ioi Real.instIsOrderedCancelAddMonoid IsStrictOrderedModule.toPosSMulStrictMono IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing
convexOn_klFun 📖	mathematical	—	ConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instZero klFun	—	StrictConvexOn.convexOn strictConvexOn_klFun
deriv_klFun 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Real.log	—	Real.log_zero deriv_zero_of_not_differentiableAt not_differentiableAt_klFun_zero HasDerivAt.deriv hasDerivAt_klFun
hasDerivAt_klFun 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal klFun Real.log	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.sub_pf 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.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add HasDerivAt.sub HasDerivAt.add Real.hasDerivAt_mul_log hasDerivAt_const hasDerivAt_id
integrable_klFun_rnDeriv_iff 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing klFun ENNReal.toReal MeasureTheory.Measure.rnDeriv MeasureTheory.llr	—	MeasureTheory.integrable_add_iff_integrable_left' MeasureTheory.Integrable.sub' MeasureTheory.integrable_const MeasureTheory.Measure.integrable_toReal_rnDeriv MeasureTheory.integrable_rnDeriv_mul_log_iff MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite klFun.eq_1 add_sub_assoc
integral_klFun_rnDeriv 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.llr	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal klFun ENNReal.toReal MeasureTheory.Measure.rnDeriv Real.instSub Real.instAdd MeasureTheory.Measure.real Set.univ	—	MeasureTheory.integral_sub MeasureTheory.Integrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.integrable_rnDeriv_mul_log_iff MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.integrable_const MeasureTheory.Measure.integrable_toReal_rnDeriv MeasureTheory.integral_add MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.Measure.integral_toReal_rnDeriv smul_eq_mul mul_one MeasureTheory.integral_rnDeriv_smul
isMinOn_klFun 📖	mathematical	—	IsMinOn Real Real.instPreorder klFun Set.Ici Real.instZero Real.instOne	—	ConvexOn.isMinOn_of_rightDeriv_eq_zero convexOn_klFun interior_Ici' instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike rightDeriv_klFun Real.log_one
klFun_apply 📖	mathematical	—	klFun Real Real.instSub Real.instAdd Real.instMul Real.log Real.instOne	—	—
klFun_eq_zero_iff 📖	mathematical	Real Real.instLE Real.instZero	klFun Real.instOne	—	StrictConvexOn.eq_of_isMinOn Real.instIsStrictOrderedRing Real.instIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule strictConvexOn_klFun isMinOn_iff klFun_nonneg isMinOn_klFun zero_le_one' Real.instZeroLEOneClass Real.log_one MulZeroClass.mul_zero zero_add sub_self
klFun_nonneg 📖	mathematical	Real Real.instLE Real.instZero	klFun	—	isMinOn_klFun klFun_one
klFun_one 📖	mathematical	—	klFun Real Real.instOne Real.instZero	—	Real.log_one MulZeroClass.mul_zero zero_add sub_self
klFun_zero 📖	mathematical	—	klFun Real Real.instZero Real.instOne	—	Real.log_zero MulZeroClass.mul_zero zero_add sub_zero
leftDeriv_klFun 📖	mathematical	—	derivWithin Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Set.Iio Real.instPreorder Real.log	—	Real.log_zero derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Iio_zero HasDerivWithinAt.derivWithin HasDerivAt.hasDerivWithinAt hasDerivAt_klFun uniqueDiffWithinAt_Iio
leftDeriv_klFun_one 📖	mathematical	—	derivWithin Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Set.Iio Real.instPreorder Real.instOne Real.instZero	—	leftDeriv_klFun Real.log_one
measurable_klFun 📖	mathematical	—	Measurable Real Real.measurableSpace klFun	—	Continuous.measurable BorelSpace.opensMeasurable Real.borelSpace continuous_klFun
not_differentiableAt_klFun_zero 📖	mathematical	—	DifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Real.instZero	—	Real.not_DifferentiableAt_log_mul_zero
not_differentiableWithinAt_klFun_Iio_zero 📖	mathematical	—	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Set.Iio Real.instPreorder Real.instZero	—	not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio deriv_klFun Real.tendsto_log_nhdsLT_zero
not_differentiableWithinAt_klFun_Ioi_zero 📖	mathematical	—	DifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Set.Ioi Real.instPreorder Real.instZero	—	not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi deriv_klFun Real.tendsto_log_nhdsGT_zero
rightDeriv_klFun 📖	mathematical	—	derivWithin Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Set.Ioi Real.instPreorder Real.log	—	Real.log_zero derivWithin_zero_of_not_differentiableWithinAt not_differentiableWithinAt_klFun_Ioi_zero HasDerivWithinAt.derivWithin HasDerivAt.hasDerivWithinAt hasDerivAt_klFun uniqueDiffWithinAt_Ioi
rightDeriv_klFun_one 📖	mathematical	—	derivWithin Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Set.Ioi Real.instPreorder Real.instOne Real.instZero	—	rightDeriv_klFun Real.log_one
strictConvexOn_klFun 📖	mathematical	—	StrictConvexOn Real Real.semiring Real.partialOrder Real.instAddCommMonoid Algebra.toSMul Real.instCommSemiring CommSemiring.toSemiring Algebra.id Set.Ici Real.instPreorder Real.instZero klFun	—	StrictConvexOn.sub_concaveOn Real.instIsOrderedAddMonoid StrictConvexOn.add_convexOn Real.instIsOrderedCancelAddMonoid Real.strictConvexOn_mul_log convexOn_const convex_Ici IsOrderedModule.toPosSMulMono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing concaveOn_id
stronglyMeasurable_klFun 📖	mathematical	—	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.measurableSpace klFun	—	Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_klFun
tendsto_klFun_atTop 📖	mathematical	—	Filter.Tendsto Real klFun Filter.atTop Real.instPreorder	—	Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt 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 Filter.Tendsto.atTop_add Real.instIsOrderedAddMonoid instOrderTopologyReal Filter.Tendsto.atTop_mul_atTop₀ Real.instIsOrderedRing Filter.tendsto_id Real.tendsto_log_atTop tendsto_const_nhds
tendsto_rightDeriv_klFun_atTop 📖	mathematical	—	Filter.Tendsto Real derivWithin DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace klFun Set.Ioi Real.instPreorder Filter.atTop	—	rightDeriv_klFun Real.tendsto_log_atTop

---

← Back to Index