Documentation Verification Report

Increment

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

Statistics

Metric	Count
Definitions `increment`	1
Theorems `card_increment`, `energy_increment`, `increment_isEquipartition`, `le_sum_distinctPairs_edgeDensity_sq`	4
Total	5

SzemerediRegularity

Definitions

Name	Category	Theorems
`increment` 📖	CompOp	3 math math: `energy_increment`, `card_increment`, `increment_isEquipartition`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_increment` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Finpartition.IsUniform` `Real` `Real.instField` `Real.linearOrder`	`increment` `stepBound`	—	`le_imp_le_of_le_of_le` `le_refl` `stepBound.eq_1` `mul_le_mul_right` `Nat.instMulLeftMono` `pow_le_pow_left'` `covariant_swap_mul_of_covariant_mul` `stepBound_pos` `Finset.Nonempty.card_pos` `Finpartition.nonempty_of_not_uniform` `increment.eq_1` `Finpartition.card_bind` `Real.instIsStrictOrderedRing` `card_aux₁` `card_aux₂` `Finset.sum_congr` `Finset.sum_dite` `Finset.sum_const_nat` `Finpartition.card_parts_equitabilise` `LT.lt.ne'` `Finset.univ_eq_attach` `Finset.card_attach` `a_add_one_le_four_pow_parts_card` `LE.le.trans` `add_mul` `Distrib.rightDistribClass` `Finset.card_filter_add_card_filter_not`
`energy_increment` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Nat.instMonoid` `Fintype.card` `Finpartition.IsUniform` `Real.instField` `Real.linearOrder` `Real.instZero` `Real.instOne`	`Real.instAdd` `Real.instRatCast` `Finpartition.energy` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `increment`	—	`Nat.instAtLeastTwoHAddOfNat` `Finpartition.coe_energy` `Real.instIsStrictOrderedRing` `add_div` `mul_div_cancel_left₀` `GroupWithZero.toMulDivCancelClass` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `add_le_add_right` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.div_congr` `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` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNNRat.of_raw` `Mathlib.Meta.NormNum.IsNNRat.den_nz` `Mathlib.Tactic.Ring.mul_one` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `mul_le_mul_of_nonneg_right` `mul_div_right_comm` `div_le_iff₀` `Real.instNontrivial` `Finset.offDiag_card` `tsub_mul` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `LE.total` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instIsOrderedAddMonoid` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `le_tsub_of_add_le_left` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `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.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_pow` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `Mathlib.Tactic.Linarith.natCast_nonneg` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Mathlib.Meta.NormNum.isRat_le_true` `Mathlib.Meta.NormNum.IsNNRat.to_isRat` `Mathlib.Meta.NormNum.isNNRat_div` `le_of_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `mul_nonneg` `Nat.cast_nonneg'` `Mathlib.Meta.NormNum.IsRat.to_raw_eq` `Mathlib.Meta.NormNum.isRat_mul` `Mathlib.Meta.NormNum.IsInt.to_isRat` `Mathlib.Meta.NormNum.IsRat.to_isNNRat` `Mathlib.Meta.NormNum.isRat_add` `Mathlib.Meta.NormNum.IsRat.of_raw` `Mathlib.Meta.NormNum.IsRat.den_nz` `sub_le_sub_right` `mul_one` `mul_tsub` `not_le` `Finpartition.IsUniform.eq_1` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `Even.pow_nonneg` `even_two_mul` `Finset.sum_add_distrib` `Finset.sum_sub_distrib` `Finset.sum_const` `nsmul_eq_mul` `Finset.sum_ite` `Finset.sum_const_zero` `zero_add` `Finpartition.nonUniforms.eq_1` `add_sub_assoc` `add_sub_right_comm` `Finset.sum_attach` `Finset.sum_le_sum` `le_sum_distinctPairs_edgeDensity_sq` `card_increment` `coe_stepBound` `mul_pow` `pow_right_comm` `div_mul_eq_div_div_swap` `Finset.sum_div` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `Finset.sum_biUnion` `Finset.sum_le_sum_of_subset_of_nonneg` `sq_nonneg`
`increment_isEquipartition` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ`	`increment`	—	`Finpartition.mem_bind` `increment.eq_1` `Finset.mem_coe` `card_eq_of_mem_parts_chunk`
`le_sum_distinctPairs_edgeDensity_sq` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Real` `Real.instLE` `Real.instOne` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Real.instMonoid`	`Real.instAdd` `Real.instRatCast` `SimpleGraph.edgeDensity` `Finset.instMembership` `Finset.offDiag` `Real.instSub` `SimpleGraph.IsUniform` `Real.instField` `Real.linearOrder` `SimpleGraph.IsUniform.instDecidableRel` `Real.instZero` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Finset.sum` `Real.instAddCommMonoid`	—	`Nat.instAtLeastTwoHAddOfNat` `add_sub_assoc` `add_sub_right_comm` `add_zero` `edgeDensity_chunk_uniform` `edgeDensity_chunk_not_uniform` `Finset.mem_offDiag`

---

← Back to Index