Documentation Verification Report

Chunk

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

Statistics

Metric	Count
Definitions `chunk`	1
Theorems `biUnion_star_subset_nonuniformWitness`, `card_biUnion_star_le_m_add_one_card_star_mul`, `card_chunk`, `card_eq_of_mem_parts_chunk`, `card_le_m_add_one_of_mem_chunk_parts`, `edgeDensity_chunk_not_uniform`, `edgeDensity_chunk_uniform`, `m_le_card_of_mem_chunk_parts`, `star_subset_chunk`	9
Total	10

SzemerediRegularity

Definitions

Name	Category	Theorems
`chunk` 📖	CompOp	4 math math: `card_chunk`, `star_subset_chunk`, `edgeDensity_chunk_uniform`, `edgeDensity_chunk_not_uniform`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`biUnion_star_subset_nonuniformWitness` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	`Finset.instHasSubset` `Finset.biUnion` `star` `SimpleGraph.nonuniformWitness` `Real` `Real.instField` `Real.linearOrder` `Real.instIsStrictOrderedRing`	—	`Real.instIsStrictOrderedRing` `Finset.biUnion_subset_iff_forall_subset` `Finset.mem_filter`
`card_biUnion_star_le_m_add_one_card_star_mul` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	`Real` `Real.instLE` `Real.instNatCast` `Finset.card` `Finset.biUnion` `star` `Real.instMul` `Real.instAdd` `Fintype.card` `stepBound` `Real.instOne`	—	`Nat.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Finset.card_biUnion_le_card_mul` `card_le_m_add_one_of_mem_chunk_parts` `star_subset_chunk`
`card_chunk` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	`Finset.card` `chunk` `Monoid.toNatPow` `Nat.instMonoid`	—	`Real.instIsStrictOrderedRing` `card_aux₁` `card_aux₂` `Finpartition.card_parts_equitabilise` `tsub_add_cancel_of_le` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `le_of_lt` `a_add_one_le_four_pow_parts_card`
`card_eq_of_mem_parts_chunk` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `chunk`	`Finset.card` `Fintype.card` `stepBound`	—	`Finpartition.card_eq_of_mem_parts_equitabilise` `Real.instIsStrictOrderedRing` `card_aux₁` `card_aux₂`
`card_le_m_add_one_of_mem_chunk_parts` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `chunk`	`Finset.card` `Fintype.card` `stepBound`	—	`card_eq_of_mem_parts_chunk` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Eq.le`
`edgeDensity_chunk_not_uniform` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Real.instMonoid` `Real.instOne` `Finset.instMembership` `SimpleGraph.IsUniform` `Real.instField` `Real.linearOrder`	`Real.instAdd` `Real.instSub` `Real.instRatCast` `SimpleGraph.edgeDensity` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Finset.sum` `Real.instAddCommMonoid` `Finset.product` `chunk`	—	`Nat.instAtLeastTwoHAddOfNat` `add_le_add_right` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `SimpleGraph.IsUniform.symm` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Meta.NormNum.isNat_pow` `Mathlib.Meta.NormNum.IsNatPowT.run` `Mathlib.Meta.NormNum.IsNatPowT.bit0` `pow_right_comm` `sq` `div_mul_div_comm` `mul_assoc` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `le_of_lt` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `div_nonneg` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `le_trans` `Mathlib.Meta.NormNum.IsNNRat.to_eq` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `RCLike.charZero_rclike` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Tactic.Ring.sub_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `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.atom_pf` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_pf_left` `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.Tactic.Ring.neg_zero` `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_zero_add` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.mul_neg` `CancelDenoms.derive_trans` `CancelDenoms.sub_subst` `CancelDenoms.mul_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `CancelDenoms.pow_subst` `Mathlib.Meta.NormNum.one_natPow` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `mul_self_nonneg` `mul_le_mul_of_nonneg_right` `Mathlib.Meta.NormNum.isNNRat_lt_true` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `Finset.product_subset_product` `star_subset_chunk` `add_div_le_sum_sq_div_card` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.mul_nonpos` `Finset.sum_congr` `Finset.card_product` `card_chunk` `LT.lt.ne'` `m_pos` `Nat.cast_mul` `Mathlib.Meta.NormNum.IsNat.to_eq` `Nat.cast_pow` `Mathlib.Meta.NormNum.isNat_natCast` `LE.le.trans` `mul_pow` `div_pow`
`edgeDensity_chunk_uniform` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Real.instMonoid` `Finset.instMembership`	`Real.instSub` `Real.instRatCast` `SimpleGraph.edgeDensity` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Finset.sum` `Real.instAddCommMonoid` `Finset.product` `chunk`	—	`Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `Finset.card_product` `Nat.cast_mul` `card_chunk` `LT.lt.ne'` `m_pos` `mul_pow` `RCLike.charZero_rclike` `sum_div_card_sq_le_sum_sq_div_card` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE`
`m_le_card_of_mem_chunk_parts` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `chunk`	`Fintype.card` `stepBound` `Finset.card`	—	`card_eq_of_mem_parts_chunk` `ge_of_eq` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd`
`star_subset_chunk` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	`Finset.instHasSubset` `star` `chunk`	—	`Finset.filter_subset` `Real.instIsStrictOrderedRing`

---

← Back to Index