NetEntropy

📁 Source: Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean

Statistics

Metric	Count
Definitions IsDynNetIn, netEntropyEntourage, netEntropyInfEntourage, netMaxcard	4
Theorems card_le_card_of_isDynCoverOf, card_le_netMaxcard, of_entourage_subset, of_le, coverEntropyEntourage_le_netEntropyEntourage, coverEntropyInfEntourage_le_netEntropyInfEntourage, coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage, coverEntropyInf_eq_iSup_netEntropyInfEntourage, coverEntropy_eq_iSup_basis_netEntropyEntourage, coverEntropy_eq_iSup_netEntropyEntourage, coverMincard_le_netMaxcard, isDynNetIn_empty, isDynNetIn_singleton, netEntropyEntourage_antitone, netEntropyEntourage_empty, netEntropyEntourage_le_coverEntropy, netEntropyEntourage_le_coverEntropyEntourage, netEntropyEntourage_nonneg, netEntropyEntourage_univ, netEntropyInfEntourage_antitone, netEntropyInfEntourage_empty, netEntropyInfEntourage_le_coverEntropyInf, netEntropyInfEntourage_le_coverEntropyInfEntourage, netEntropyInfEntourage_le_netEntropyEntourage, netEntropyInfEntourage_nonneg, netEntropyInfEntourage_univ, netMaxcard_antitone, netMaxcard_empty, netMaxcard_eq_zero_iff, netMaxcard_finite_iff, netMaxcard_infinite_iff, netMaxcard_le_coverMincard, netMaxcard_monotone_time, netMaxcard_univ, netMaxcard_zero, one_le_netMaxcard_iff	36
Total	40

Dynamics

Definitions

Name	Category	Theorems
IsDynNetIn 📖	MathDef	4 math math: netMaxcard_infinite_iff, isDynNetIn_singleton, netMaxcard_finite_iff, isDynNetIn_empty
netEntropyEntourage 📖	CompOp	11 math math: netEntropyEntourage_monotone, netEntropyEntourage_le_coverEntropyEntourage, netEntropyEntourage_antitone, coverEntropyEntourage_le_netEntropyEntourage, netEntropyEntourage_empty, netEntropyInfEntourage_le_netEntropyEntourage, coverEntropy_eq_iSup_basis_netEntropyEntourage, coverEntropy_eq_iSup_netEntropyEntourage, netEntropyEntourage_nonneg, netEntropyEntourage_le_coverEntropy, netEntropyEntourage_univ
netEntropyInfEntourage 📖	CompOp	11 math math: coverEntropyInfEntourage_le_netEntropyInfEntourage, netEntropyInfEntourage_univ, coverEntropyInf_eq_iSup_netEntropyInfEntourage, netEntropyInfEntourage_nonneg, netEntropyInfEntourage_le_netEntropyEntourage, netEntropyInfEntourage_monotone, coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage, netEntropyInfEntourage_le_coverEntropyInfEntourage, netEntropyInfEntourage_le_coverEntropyInf, netEntropyInfEntourage_empty, netEntropyInfEntourage_antitone
netMaxcard 📖	CompOp	13 math math: netMaxcard_monotone_subset, netMaxcard_le_coverMincard, IsDynNetIn.card_le_netMaxcard, netMaxcard_infinite_iff, netMaxcard_zero, netMaxcard_empty, netMaxcard_antitone, netMaxcard_monotone_time, netMaxcard_finite_iff, coverMincard_le_netMaxcard, netMaxcard_univ, netMaxcard_eq_zero_iff, one_le_netMaxcard_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coverEntropyEntourage_le_netEntropyEntourage 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal coverEntropyEntourage SetRel.comp netEntropyEntourage	—	ExpGrowth.expGrowthSup_monotone ENat.toENNReal_mono coverMincard_le_netMaxcard
coverEntropyInfEntourage_le_netEntropyInfEntourage 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal coverEntropyInfEntourage SetRel.comp netEntropyInfEntourage	—	ExpGrowth.expGrowthInf_monotone ENat.toENNReal_mono coverMincard_le_netMaxcard
coverEntropyInf_eq_iSup_basis_netEntropyInfEntourage 📖	mathematical	Filter.HasBasis uniformity	coverEntropyInf iSup EReal instSupSetEReal netEntropyInfEntourage	—	coverEntropyInf_eq_iSup_netEntropyInfEntourage LE.le.antisymm' iSup₂_mono' Filter.HasBasis.mem_of_mem le_refl iSup₂_le Filter.HasBasis.mem_iff LE.le.trans netEntropyInfEntourage_antitone le_iSup₂
coverEntropyInf_eq_iSup_netEntropyInfEntourage 📖	mathematical	—	coverEntropyInf iSup EReal Set instSupSetEReal Filter Filter.instMembership uniformity netEntropyInfEntourage	—	le_antisymm iSup₂_le comp_symm_mem_uniformity_sets isRefl_of_mem_uniformity LE.le.trans coverEntropyInfEntourage_antitone le_iSup₂_of_le coverEntropyInfEntourage_le_netEntropyInfEntourage netEntropyInfEntourage_antitone SetRel.symmetrize_subset_self LE.le.trans' le_iSup₂ symmetrize_mem_uniformity netEntropyInfEntourage_le_coverEntropyInfEntourage
coverEntropy_eq_iSup_basis_netEntropyEntourage 📖	mathematical	Filter.HasBasis uniformity	coverEntropy iSup EReal instSupSetEReal netEntropyEntourage	—	coverEntropy_eq_iSup_netEntropyEntourage LE.le.antisymm' iSup₂_mono' Filter.HasBasis.mem_of_mem le_refl iSup₂_le Filter.HasBasis.mem_iff LE.le.trans netEntropyEntourage_antitone le_iSup₂
coverEntropy_eq_iSup_netEntropyEntourage 📖	mathematical	—	coverEntropy iSup EReal Set instSupSetEReal Filter Filter.instMembership uniformity netEntropyEntourage	—	le_antisymm iSup₂_le comp_symm_mem_uniformity_sets LE.le.trans coverEntropyEntourage_antitone le_iSup₂_of_le isRefl_of_mem_uniformity coverEntropyEntourage_le_netEntropyEntourage netEntropyEntourage_antitone SetRel.symmetrize_subset_self LE.le.trans' le_iSup₂ symmetrize_mem_uniformity netEntropyEntourage_le_coverEntropyEntourage
coverMincard_le_netMaxcard 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat coverMincard SetRel.comp netMaxcard	—	eq_top_or_lt_top le_top netMaxcard_finite_iff IsDynCoverOf.coverMincard_le_card IsDynCoverOf.eq_1 UniformSpace.isCover_iff_subset_iUnion_ball isSymm_dynEntourage SetRel.isSymm_comp_self Set.not_subset Set.insert_subset Set.pairwiseDisjoint_insert Set.disjoint_left Set.iUnion_congr_Prop mem_ball_dynEntourage_comp Set.nonempty_of_mem LE.le.not_gt IsDynNetIn.card_le_netMaxcard Finset.coe_insert Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass LT.lt.trans_eq lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instIsOrderedAddMonoid Finset.card_insert_of_notMem UniformSpace.ball_mono dynEntourage_monotone SetRel.left_subset_comp SetRel.rfl isRefl_dynEntourage
isDynNetIn_empty 📖	mathematical	—	IsDynNetIn Set Set.instEmptyCollection	—	Set.empty_subset Set.pairwise_empty
isDynNetIn_singleton 📖	mathematical	Set Set.instMembership	IsDynNetIn Set.instSingletonSet	—	Set.singleton_subset_iff Set.pairwise_singleton
netEntropyEntourage_antitone 📖	mathematical	—	Antitone SetRel EReal PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrderEReal netEntropyEntourage	—	ExpGrowth.expGrowthSup_monotone ENat.toENNReal_mono netMaxcard_antitone
netEntropyEntourage_empty 📖	mathematical	—	netEntropyEntourage Set Set.instEmptyCollection Bot.bot EReal instBotEReal	—	netEntropyEntourage.eq_1 ExpGrowth.expGrowthSup_zero netMaxcard_empty ENat.toENNReal_zero
netEntropyEntourage_le_coverEntropy 📖	mathematical	SetRel Filter Filter.instMembership uniformity	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal netEntropyEntourage coverEntropy	—	le_iSup₂ coverEntropy_eq_iSup_netEntropyEntourage
netEntropyEntourage_le_coverEntropyEntourage 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal netEntropyEntourage coverEntropyEntourage	—	ExpGrowth.expGrowthSup_monotone ENat.toENNReal_mono netMaxcard_le_coverMincard
netEntropyEntourage_nonneg 📖	mathematical	Set.Nonempty	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal netEntropyEntourage	—	LE.le.trans netEntropyInfEntourage_nonneg netEntropyInfEntourage_le_netEntropyEntourage
netEntropyEntourage_univ 📖	mathematical	Set.Nonempty	netEntropyEntourage Set.univ EReal instZeroEReal	—	ExpGrowth.expGrowthSup_const one_ne_zero NeZero.charZero_one ENNReal.instCharZero ENNReal.one_ne_top netEntropyEntourage.eq_1 netMaxcard_univ ENat.toENNReal_one
netEntropyInfEntourage_antitone 📖	mathematical	—	Antitone SetRel EReal PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrderEReal netEntropyInfEntourage	—	ExpGrowth.expGrowthInf_monotone ENat.toENNReal_mono netMaxcard_antitone
netEntropyInfEntourage_empty 📖	mathematical	—	netEntropyInfEntourage Set Set.instEmptyCollection Bot.bot EReal instBotEReal	—	eq_bot_mono netEntropyInfEntourage_le_netEntropyEntourage netEntropyEntourage_empty
netEntropyInfEntourage_le_coverEntropyInf 📖	mathematical	SetRel Filter Filter.instMembership uniformity	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal netEntropyInfEntourage coverEntropyInf	—	le_iSup₂ coverEntropyInf_eq_iSup_netEntropyInfEntourage
netEntropyInfEntourage_le_coverEntropyInfEntourage 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal netEntropyInfEntourage coverEntropyInfEntourage	—	ExpGrowth.expGrowthInf_monotone ENat.toENNReal_mono netMaxcard_le_coverMincard
netEntropyInfEntourage_le_netEntropyEntourage 📖	mathematical	—	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal netEntropyInfEntourage netEntropyEntourage	—	ExpGrowth.expGrowthInf_le_expGrowthSup
netEntropyInfEntourage_nonneg 📖	mathematical	Set.Nonempty	EReal Preorder.toLE PartialOrder.toPreorder instPartialOrderEReal instZeroEReal netEntropyInfEntourage	—	Monotone.expGrowthInf_nonneg ENat.toENNReal_mono netMaxcard_monotone_time Iff.not netMaxcard_zero Pi.zero_apply ENat.toENNReal_one one_ne_zero NeZero.charZero_one ENNReal.instCharZero
netEntropyInfEntourage_univ 📖	mathematical	Set.Nonempty	netEntropyInfEntourage Set.univ EReal instZeroEReal	—	ExpGrowth.expGrowthInf_const one_ne_zero NeZero.charZero_one ENNReal.instCharZero ENNReal.one_ne_top netEntropyInfEntourage.eq_1 netMaxcard_univ ENat.toENNReal_one
netMaxcard_antitone 📖	mathematical	—	Antitone SetRel ENat PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat netMaxcard	—	biSup_mono IsDynNetIn.of_entourage_subset
netMaxcard_empty 📖	mathematical	—	netMaxcard Set Set.instEmptyCollection ENat instZeroENat	—	netMaxcard.eq_1 bot_eq_zero iSup₂_eq_bot Set.subset_empty_iff Finset.card_empty CharP.cast_eq_zero CharP.ofCharZero bot_eq_zero'
netMaxcard_eq_zero_iff 📖	mathematical	—	netMaxcard ENat instZeroENat Set Set.instEmptyCollection	—	Set.eq_empty_iff_forall_notMem isDynNetIn_singleton IsDynNetIn.card_le_netMaxcard Finset.coe_singleton LE.le.not_gt Nat.cast_one Finset.card_singleton zero_lt_one IsOrderedRing.toZeroLEOneClass NeZero.charZero_one netMaxcard_empty
netMaxcard_finite_iff 📖	mathematical	—	ENat Preorder.toLT PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat netMaxcard Top.top instTopENat IsDynNetIn SetLike.coe Finset Finset.instSetLike ENat.instNatCast Finset.card	—	WithTop.ne_top_iff_exists LT.lt.ne netMaxcard.eq_1 Set.image_comp sSup_image iSup_congr_Prop mem_upperBounds WithTop.coe_le_coe le_sSup Set.image_congr WithTop.charZero Nat.instCharZero Filter.frequently_principal Finset.coe_empty isDynNetIn_empty Nat.sSup_mem Set.mem_image ENat.some_eq_coe WithTop.coe_sSup' WithTop.coe_lt_top
netMaxcard_infinite_iff 📖	mathematical	—	netMaxcard Top.top ENat instTopENat IsDynNetIn SetLike.coe Finset Finset.instSetLike Finset.card	—	IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass iSup_eq_top iSup_subtype' netMaxcard.eq_1 ENat.coe_lt_top LT.lt.le WithTop.eq_top_iff_forall_gt LE.le.trans_lt' IsDynNetIn.card_le_netMaxcard ENat.some_eq_coe Nat.cast_lt LT.lt.trans_le lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Nat.instIsOrderedAddMonoid
netMaxcard_le_coverMincard 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat netMaxcard coverMincard	—	eq_top_or_lt_top le_top coverMincard_finite_iff iSup₂_le Nat.cast_le IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass IsDynNetIn.card_le_card_of_isDynCoverOf
netMaxcard_monotone_time 📖	mathematical	—	Monotone ENat Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat netMaxcard	—	biSup_mono IsDynNetIn.of_le
netMaxcard_univ 📖	mathematical	Set.Nonempty	netMaxcard Set.univ ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	LE.le.antisymm iSup₂_le Nat.cast_one IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass Finset.card_le_one Set.PairwiseDisjoint.elim_set dynEntourage_univ Set.mem_univ one_le_netMaxcard_iff
netMaxcard_zero 📖	mathematical	Set.Nonempty	netMaxcard ENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	LE.le.antisymm iSup₂_le Nat.cast_one IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass Finset.card_le_one Set.PairwiseDisjoint.elim_set dynEntourage_zero Set.mem_univ one_le_netMaxcard_iff
one_le_netMaxcard_iff 📖	mathematical	—	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat netMaxcard Set.Nonempty	—	ENat.one_le_iff_ne_zero Set.nonempty_iff_ne_empty not_iff_not netMaxcard_eq_zero_iff

Dynamics.IsDynNetIn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_le_card_of_isDynCoverOf 📖	mathematical	Dynamics.IsDynNetIn SetLike.coe Finset Finset.instSetLike Dynamics.IsDynCoverOf	Finset.card	—	Finset.card_le_card_of_injOn Set.PairwiseDisjoint.elim_set Function.sometimes_spec
card_le_netMaxcard 📖	mathematical	Dynamics.IsDynNetIn SetLike.coe Finset Finset.instSetLike	ENat Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat ENat.instNatCast Finset.card Dynamics.netMaxcard	—	le_iSup₂
of_entourage_subset 📖	—	SetRel Set.instHasSubset Dynamics.IsDynNetIn	—	—	Set.PairwiseDisjoint.mono UniformSpace.ball_mono Dynamics.dynEntourage_monotone
of_le 📖	—	Dynamics.IsDynNetIn	—	—	Set.PairwiseDisjoint.mono UniformSpace.ball_mono Dynamics.dynEntourage_antitone

---

← Back to Index