Documentation Verification Report

Energy

📁 Source: Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean

Statistics

Metric	Count
Definitions `energy`	1
Theorems `coe_energy`, `energy_le_one`, `energy_nonneg`	3
Total	4

Finpartition

Definitions

Name	Category	Theorems
`energy` 📖	CompOp	4 math math: `SzemerediRegularity.energy_increment`, `energy_le_one`, `coe_energy`, `energy_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_energy` 📖	mathematical	—	`DivisionRing.toRatCast` `Field.toDivisionRing` `energy` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Finset.sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.offDiag` `parts` `Finset.instLattice` `Finset.instOrderBot` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SimpleGraph.edgeDensity` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Finset.card`	—	`energy.eq_1` `Finset.sum_congr` `IsStrictOrderedRing.toCharZero` `Nat.cast_pow` `Rat.cast_pow` `Rat.cast_natCast`
`energy_le_one` 📖	mathematical	—	`energy`	—	`div_le_of_le_mul₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Rat.instIsStrictOrderedRing` `sq_nonneg` `AddGroup.existsAddOfLE` `Rat.instPosMulMono` `Rat.instAddLeftMono` `zero_le_one` `Rat.instZeroLEOneClass` `Finset.sum_le_card_nsmul` `sq_le_one_iff₀` `IsStrictOrderedRing.toPosMulStrictMono` `SimpleGraph.edgeDensity_nonneg` `SimpleGraph.edgeDensity_le_one` `Nat.smul_one_eq_cast` `Finset.offDiag_card` `one_mul` `Rat.instCharZero` `sq` `tsub_le_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub`
`energy_nonneg` 📖	mathematical	—	`energy`	—	`div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Rat.instIsStrictOrderedRing` `Finset.sum_nonneg` `Rat.instAddLeftMono` `sq_nonneg` `AddGroup.existsAddOfLE` `Rat.instPosMulMono`

---

← Back to Index