Energy

📁 Source: Mathlib/Combinatorics/Additive/Energy.lean

Statistics

Metric	Count
Definitions `«termE[_,_]»`, `«termE[_]»`, `«termEₘ[_,_]»`, `«termEₘ[_]»`, `addEnergy`, `mulEnergy`	6
Theorems `addEnergy_comm`, `addEnergy_empty_left`, `addEnergy_empty_right`, `addEnergy_eq_card_filter`, `addEnergy_eq_sum_sq`, `addEnergy_eq_sum_sq'`, `addEnergy_eq_zero_iff`, `addEnergy_mono`, `addEnergy_mono_left`, `addEnergy_mono_right`, `addEnergy_pos`, `addEnergy_pos_iff`, `addEnergy_self_eq_zero_iff`, `addEnergy_self_pos`, `addEnergy_self_pos_iff`, `addEnergy_univ_left`, `addEnergy_univ_right`, `card_sq_le_card_mul_addEnergy`, `card_sq_le_card_mul_mulEnergy`, `le_addEnergy`, `le_addEnergy_self`, `le_card_add_mul_addEnergy`, `le_card_mul_mul_mulEnergy`, `le_mulEnergy`, `le_mulEnergy_self`, `mulEnergy_comm`, `mulEnergy_empty_left`, `mulEnergy_empty_right`, `mulEnergy_eq_card_filter`, `mulEnergy_eq_sum_sq`, `mulEnergy_eq_sum_sq'`, `mulEnergy_eq_zero_iff`, `mulEnergy_mono`, `mulEnergy_mono_left`, `mulEnergy_mono_right`, `mulEnergy_pos`, `mulEnergy_pos_iff`, `mulEnergy_self_eq_zero_iff`, `mulEnergy_self_pos`, `mulEnergy_self_pos_iff`, `mulEnergy_univ_left`, `mulEnergy_univ_right`	42
Total	48

Combinatorics.Additive

Definitions

Name	Category	Theorems
`«termE[_,_]»` 📖	CompOp	—
`«termE[_]»` 📖	CompOp	—
`«termEₘ[_,_]»` 📖	CompOp	—
`«termEₘ[_]»` 📖	CompOp	—

Finset

Definitions

Name	Category	Theorems
`addEnergy` 📖	CompOp	21 math math: `addEnergy_eq_sum_sq'`, `addEnergy_mono_left`, `addEnergy_comm`, `addEnergy_mono`, `addEnergy_univ_left`, `addEnergy_eq_sum_sq`, `addEnergy_self_pos`, `addEnergy_empty_left`, `le_addEnergy`, `le_card_add_mul_addEnergy`, `card_sq_le_card_mul_addEnergy`, `addEnergy_pos`, `addEnergy_self_eq_zero_iff`, `addEnergy_mono_right`, `addEnergy_empty_right`, `addEnergy_self_pos_iff`, `addEnergy_pos_iff`, `addEnergy_eq_card_filter`, `addEnergy_eq_zero_iff`, `addEnergy_univ_right`, `le_addEnergy_self`
`mulEnergy` 📖	CompOp	21 math math: `mulEnergy_self_eq_zero_iff`, `mulEnergy_mono_left`, `mulEnergy_univ_left`, `mulEnergy_univ_right`, `mulEnergy_eq_sum_sq'`, `mulEnergy_pos_iff`, `le_card_mul_mul_mulEnergy`, `mulEnergy_empty_right`, `mulEnergy_pos`, `card_sq_le_card_mul_mulEnergy`, `mulEnergy_self_pos_iff`, `mulEnergy_mono_right`, `le_mulEnergy`, `mulEnergy_eq_zero_iff`, `mulEnergy_eq_sum_sq`, `le_mulEnergy_self`, `mulEnergy_self_pos`, `mulEnergy_mono`, `mulEnergy_empty_left`, `mulEnergy_comm`, `mulEnergy_eq_card_filter`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addEnergy_comm` 📖	mathematical	—	`addEnergy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`addEnergy.eq_1` `card_map` `map_filter` `filter.congr_simp` `add_comm` `map_eq_image` `image_swap_product`
`addEnergy_empty_left` 📖	mathematical	—	`addEnergy` `Finset` `instEmptyCollection`	—	`filter.congr_simp` `product_empty` `filter_empty`
`addEnergy_empty_right` 📖	mathematical	—	`addEnergy` `Finset` `instEmptyCollection`	—	`filter.congr_simp` `product_empty` `filter_empty`
`addEnergy_eq_card_filter` 📖	mathematical	—	`addEnergy` `card` `filter` `SProd.sprod` `Finset` `instSProd`	—	`card_equiv` `mem_filter` `mem_product`
`addEnergy_eq_sum_sq` 📖	mathematical	—	`addEnergy` `sum` `Nat.instAddCommMonoid` `univ` `Monoid.toNatPow` `Nat.instMonoid` `card` `filter` `SProd.sprod` `Finset` `instSProd`	—	`addEnergy_eq_sum_sq'` `Fintype.sum_subset` `card_eq_zero` `filter_eq_empty_iff` `mem_product` `Nat.instAtLeastTwoHAddOfNat` `OfNat.ofNat_ne_zero` `Nat.instCharZero` `add_mem_add`
`addEnergy_eq_sum_sq'` 📖	mathematical	—	`addEnergy` `sum` `Nat.instAddCommMonoid` `Finset` `add` `Monoid.toNatPow` `Nat.instMonoid` `card` `filter` `SProd.sprod` `instSProd`	—	`addEnergy_eq_card_filter` `sum_congr` `sq` `card_product` `coe_add` `disjoint_left` `mem_product` `mem_filter` `card_disjiUnion` `disjiUnion_eq_biUnion` `ext` `mem_biUnion` `add_mem_add`
`addEnergy_eq_zero_iff` 📖	mathematical	—	`addEnergy` `Finset` `instEmptyCollection`	—	`LE.le.not_lt_iff_eq'` `addEnergy_pos_iff` `not_nonempty_iff_eq_empty` `imp_iff_or_not`
`addEnergy_mono` 📖	mathematical	`Finset` `instHasSubset`	`addEnergy`	—	`card_le_card` `filter_subset_filter` `product_subset_product`
`addEnergy_mono_left` 📖	mathematical	`Finset` `instHasSubset`	`addEnergy`	—	`addEnergy_mono` `Subset.rfl`
`addEnergy_mono_right` 📖	mathematical	`Finset` `instHasSubset`	`addEnergy`	—	`addEnergy_mono` `Subset.rfl`
`addEnergy_pos` 📖	mathematical	`Nonempty`	`addEnergy`	—	`LT.lt.trans_le` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nonempty.card_pos` `le_addEnergy`
`addEnergy_pos_iff` 📖	mathematical	—	`addEnergy` `Nonempty`	—	`Mathlib.Tactic.Push.not_and_or_eq` `not_nonempty_iff_eq_empty` `addEnergy_empty_left` `lt_self_iff_false` `addEnergy_empty_right` `addEnergy_pos`
`addEnergy_self_eq_zero_iff` 📖	mathematical	—	`addEnergy` `Finset` `instEmptyCollection`	—	`addEnergy_eq_zero_iff`
`addEnergy_self_pos` 📖	mathematical	`Nonempty`	`addEnergy`	—	`addEnergy_pos`
`addEnergy_self_pos_iff` 📖	mathematical	—	`addEnergy` `Nonempty`	—	`addEnergy_pos_iff`
`addEnergy_univ_left` 📖	mathematical	—	`addEnergy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `univ` `Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `card`	—	`sq` `card_product` `add_right_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd` `card_image_of_injOn` `ext` `mem_filter` `mem_product` `mem_univ` `mem_image` `add_right_comm` `add_neg_cancel_right`
`addEnergy_univ_right` 📖	mathematical	—	`addEnergy` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `univ` `Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `card`	—	`addEnergy_comm` `addEnergy_univ_left`
`card_sq_le_card_mul_addEnergy` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `card` `filter` `Finset` `instMembership` `decidableMem` `SProd.sprod` `instSProd` `addEnergy`	—	`sum_card_fiberwise_eq_card_filter` `sum_congr` `one_mul` `one_pow` `sum_const` `nsmul_eq_mul` `mul_one` `sum_mul_sq_le_sq_mul_sq` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `mul_le_mul_right` `Nat.instMulLeftMono` `sum_le_sum_of_ne_zero` `card_eq_zero` `filter_eq_empty_iff` `mem_product` `Nat.instAtLeastTwoHAddOfNat` `OfNat.ofNat_ne_zero` `Nat.instCharZero` `add_mem_add` `addEnergy_eq_sum_sq'`
`card_sq_le_card_mul_mulEnergy` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `card` `filter` `Finset` `instMembership` `decidableMem` `SProd.sprod` `instSProd` `mulEnergy`	—	`sum_card_fiberwise_eq_card_filter` `sum_congr` `one_mul` `one_pow` `sum_const` `nsmul_eq_mul` `mul_one` `sum_mul_sq_le_sq_mul_sq` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `mul_le_mul_right` `Nat.instMulLeftMono` `sum_le_sum_of_ne_zero` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `mul_mem_mul` `mulEnergy_eq_sum_sq'`
`le_addEnergy` 📖	mathematical	—	`card` `addEnergy`	—	`card_product` `card_le_card_of_injOn` `coe_product` `Set.mem_prod` `SetLike.mem_coe` `coe_filter` `mem_product` `Set.injOn_of_eq_iff_eq`
`le_addEnergy_self` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `card` `addEnergy`	—	`le_addEnergy` `sq`
`le_card_add_mul_addEnergy` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `card` `Finset` `add` `addEnergy`	—	`filter_eq_self` `add_mem_add` `mem_product` `card_product` `mul_pow` `card_sq_le_card_mul_addEnergy`
`le_card_mul_mul_mulEnergy` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `card` `Finset` `mul` `mulEnergy`	—	`filter_eq_self` `mul_mem_mul` `card_product` `mul_pow` `card_sq_le_card_mul_mulEnergy`
`le_mulEnergy` 📖	mathematical	—	`card` `mulEnergy`	—	`card_product` `card_le_card_of_injOn` `coe_product` `coe_filter`
`le_mulEnergy_self` 📖	mathematical	—	`Monoid.toNatPow` `Nat.instMonoid` `card` `mulEnergy`	—	`le_mulEnergy` `sq`
`mulEnergy_comm` 📖	mathematical	—	`mulEnergy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid`	—	`mulEnergy.eq_1` `card_map` `map_filter` `filter.congr_simp` `mul_comm` `map_eq_image` `image_swap_product`
`mulEnergy_empty_left` 📖	mathematical	—	`mulEnergy` `Finset` `instEmptyCollection`	—	`filter.congr_simp` `product_empty` `filter_empty`
`mulEnergy_empty_right` 📖	mathematical	—	`mulEnergy` `Finset` `instEmptyCollection`	—	`filter.congr_simp` `product_empty` `filter_empty`
`mulEnergy_eq_card_filter` 📖	mathematical	—	`mulEnergy` `card` `filter` `SProd.sprod` `Finset` `instSProd`	—	`card_equiv`
`mulEnergy_eq_sum_sq` 📖	mathematical	—	`mulEnergy` `sum` `Nat.instAddCommMonoid` `univ` `Monoid.toNatPow` `Nat.instMonoid` `card` `filter` `SProd.sprod` `Finset` `instSProd`	—	`mulEnergy_eq_sum_sq'` `Fintype.sum_subset` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat`
`mulEnergy_eq_sum_sq'` 📖	mathematical	—	`mulEnergy` `sum` `Nat.instAddCommMonoid` `Finset` `mul` `Monoid.toNatPow` `Nat.instMonoid` `card` `filter` `SProd.sprod` `instSProd`	—	`mulEnergy_eq_card_filter` `sum_congr` `sq` `coe_mul` `card_disjiUnion` `disjiUnion_eq_biUnion` `ext` `mul_mem_mul`
`mulEnergy_eq_zero_iff` 📖	mathematical	—	`mulEnergy` `Finset` `instEmptyCollection`	—	`LE.le.not_lt_iff_eq'`
`mulEnergy_mono` 📖	mathematical	`Finset` `instHasSubset`	`mulEnergy`	—	`card_le_card` `filter_subset_filter` `product_subset_product`
`mulEnergy_mono_left` 📖	mathematical	`Finset` `instHasSubset`	`mulEnergy`	—	`mulEnergy_mono` `Subset.rfl`
`mulEnergy_mono_right` 📖	mathematical	`Finset` `instHasSubset`	`mulEnergy`	—	`mulEnergy_mono` `Subset.rfl`
`mulEnergy_pos` 📖	mathematical	`Nonempty`	`mulEnergy`	—	`LT.lt.trans_le` `mul_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nonempty.card_pos` `le_mulEnergy`
`mulEnergy_pos_iff` 📖	mathematical	—	`mulEnergy` `Nonempty`	—	`Mathlib.Tactic.Push.not_and_or_eq` `mulEnergy_empty_left` `mulEnergy_empty_right` `mulEnergy_pos`
`mulEnergy_self_eq_zero_iff` 📖	mathematical	—	`mulEnergy` `Finset` `instEmptyCollection`	—	`mulEnergy_eq_zero_iff`
`mulEnergy_self_pos` 📖	mathematical	`Nonempty`	`mulEnergy`	—	`mulEnergy_pos`
`mulEnergy_self_pos_iff` 📖	mathematical	—	`mulEnergy` `Nonempty`	—	`mulEnergy_pos_iff`
`mulEnergy_univ_left` 📖	mathematical	—	`mulEnergy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `univ` `Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `card`	—	`sq` `mul_right_cancel` `RightCancelSemigroup.toIsRightCancelMul` `card_image_of_injOn` `ext` `mul_right_comm` `mul_inv_cancel_right`
`mulEnergy_univ_right` 📖	mathematical	—	`mulEnergy` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `CommGroup.toGroup` `univ` `Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `card`	—	`mulEnergy_comm` `mulEnergy_univ_left`

---

← Back to Index