Bound

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

Statistics

Metric	Count
Definitions `evalBound`, `evalInitialBound`, `tacticSz_positivity`, `initialBound`, `stepBound`	5
Theorems `a_add_one_le_four_pow_parts_card`, `add_div_le_sum_sq_div_card`, `bound_pos`, `card_aux₁`, `card_aux₂`, `coe_m_add_one_pos`, `coe_stepBound`, `eps_pos`, `eps_pow_five_pos`, `hundred_div_ε_pow_five_le_m`, `hundred_le_m`, `hundred_lt_pow_initialBound_mul`, `initialBound_le_bound`, `initialBound_pos`, `le_bound`, `le_initialBound`, `le_stepBound`, `m_pos`, `mul_sq_le_sum_sq`, `one_le_m_coe`, `pow_mul_m_le_card_part`, `seven_le_initialBound`, `stepBound_mono`, `stepBound_pos`, `stepBound_pos_iff`	25
Total	30

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalBound` 📖	CompOp	—
`evalInitialBound` 📖	CompOp	—

SzemerediRegularity

Definitions

Name	Category	Theorems
`initialBound` 📖	CompOp	5 math math: `initialBound_le_bound`, `hundred_lt_pow_initialBound_mul`, `seven_le_initialBound`, `initialBound_pos`, `le_initialBound`
`stepBound` 📖	CompOp	18 math math: `stepBound_pos`, `a_add_one_le_four_pow_parts_card`, `m_le_card_of_mem_chunk_parts`, `card_increment`, `coe_stepBound`, `card_le_m_add_one_of_mem_chunk_parts`, `stepBound_pos_iff`, `m_pos`, `card_eq_of_mem_parts_chunk`, `hundred_div_ε_pow_five_le_m`, `le_stepBound`, `pow_mul_m_le_card_part`, `one_le_m_coe`, `coe_m_add_one_pos`, `card_aux₂`, `stepBound_mono`, `card_biUnion_star_le_m_add_one_card_star_mul`, `hundred_le_m`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`a_add_one_le_four_pow_parts_card` 📖	mathematical	—	`Fintype.card` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `stepBound` `Monoid.toNatPow` `Nat.instMonoid`	—	`one_le_pow₀` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instCharZero` `stepBound.eq_1` `add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `tsub_le_iff_left` `Nat.instOrderedSub`
`add_div_le_sum_sq_div_card` 📖	mathematical	`Finset` `Finset.instHasSubset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `abs` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Finset.card` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul`	—	`LE.le.eq_or_lt` `Nat.cast_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `zero_div` `MulZeroClass.zero_mul` `add_zero` `LE.le.trans` `sum_div_card_sq_le_sum_sq_div_card` `AddGroup.existsAddOfLE` `LT.lt.trans_le` `Nat.cast_le` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Finset.card_le_card` `sq_le_sq` `abs_of_nonneg` `Finset.sum_sub_distrib` `Finset.sum_const` `nsmul_eq_mul` `sub_div` `mul_div_cancel_left₀` `GroupWithZero.toMulDivCancelClass` `LT.lt.ne'` `le_refl` `le_imp_le_of_le_of_le` `add_le_add_left` `covariant_swap_add_of_covariant_add` `mul_div_right_comm` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `add_mul` `Distrib.rightDistribClass` `div_mul_cancel₀` `mul_sq_le_sum_sq` `add_le_add_right` `div_pow` `Finset.sum_congr` `sub_div'` `Nat.instAtLeastTwoHAddOfNat` `sub_sq` `mul_pow` `two_mul` `Finset.sum_add_distrib` `div_le_iff₀` `sq_pos_of_ne_zero` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.mul_pf_right` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf'` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Tactic.Ring.mul_one` `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_gt` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `mul_one`
`bound_pos` 📖	mathematical	—	`bound`	—	`LT.lt.trans_le` `initialBound_pos` `initialBound_le_bound`
`card_aux₁` 📖	—	`Finset.card` `Fintype.card` `stepBound` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `Monoid.toNatPow` `Nat.instMonoid`	—	—	`mul_add` `Distrib.leftDistribClass` `mul_one` `add_assoc` `add_mul` `Distrib.rightDistribClass` `LE.le.trans` `a_add_one_le_four_pow_parts_card` `mul_comm`
`card_aux₂` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	`Monoid.toNatPow` `Nat.instMonoid` `Finset.card` `Fintype.card` `stepBound`	—	`stepBound.eq_1` `Finpartition.IsEquipartition.card_parts_eq_average` `mul_add` `Distrib.leftDistribClass` `mul_one` `add_assoc` `add_mul` `Distrib.rightDistribClass` `a_add_one_le_four_pow_parts_card` `mul_comm` `Finset.card_univ`
`coe_m_add_one_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instAdd` `Real.instNatCast` `Fintype.card` `stepBound` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `Real.instOne`	—	`Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one`
`coe_stepBound` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `stepBound` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat`
`eps_pos` 📖	mathematical	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ`	`Real.instLT` `Real.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `Odd.pow_pos_iff` `Real.instIsStrictOrderedRing` `AddGroup.existsAddOfLE` `eps_pow_five_pos`
`eps_pow_five_pos` 📖	mathematical	`Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ`	`Real.instLT` `Real.instZero`	—	`Nat.instAtLeastTwoHAddOfNat` `pos_of_mul_pos_right` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.trans_le` `Real.instIsOrderedRing` `Real.instNontrivial` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo`
`hundred_div_ε_pow_five_le_m` 📖	mathematical	`Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Real.instMonoid`	`DivInvMonoid.toDiv` `Real.instDivInvMonoid` `stepBound`	—	`Nat.instAtLeastTwoHAddOfNat` `LE.le.trans` `div_le_of_le_mul₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `LT.lt.le` `eps_pow_five_pos` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `stepBound_pos` `Finset.Nonempty.card_pos` `Finpartition.parts_nonempty` `Finset.Nonempty.ne_empty` `Finset.univ_nonempty` `stepBound.eq_1` `mul_left_comm` `mul_pow`
`hundred_le_m` 📖	mathematical	`Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card` `Real` `Real.instLE` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Real.instMonoid` `Real.instOne`	`stepBound`	—	`Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `LE.le.trans'` `hundred_div_ε_pow_five_le_m` `le_div_self` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `pow_le_one₀` `IsOrderedRing.toPosMulMono` `le_of_lt`
`hundred_lt_pow_initialBound_mul` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `initialBound`	—	`Nat.instAtLeastTwoHAddOfNat` `Real.rpow_natCast` `div_lt_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instZeroLEOneClass` `Real.lt_rpow_iff_log_lt` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.instIsOrderedRing` `Real.instNontrivial` `zero_lt_four` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.log_pos` `initialBound.eq_1` `Nat.cast_max` `Nat.cast_add` `Nat.cast_one` `lt_max_of_lt_right` `Nat.lt_floor_add_one`
`initialBound_le_bound` 📖	mathematical	—	`initialBound` `bound`	—	`LE.le.trans` `Real.instIsStrictOrderedRing` `Function.id_le_iterate_of_id_le` `le_stepBound` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat`
`initialBound_pos` 📖	mathematical	—	`initialBound`	—	`LT.lt.trans_le` `Nat.succ_pos'` `seven_le_initialBound`
`le_bound` 📖	mathematical	—	`bound`	—	`LE.le.trans` `le_initialBound` `initialBound_le_bound`
`le_initialBound` 📖	mathematical	—	`initialBound`	—	`LE.le.trans` `Real.instIsStrictOrderedRing` `le_max_left` `le_max_right`
`le_stepBound` 📖	mathematical	—	`Pi.hasLe` `stepBound`	—	`pow_pos` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `Nat.instZeroLEOneClass` `Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial`
`m_pos` 📖	mathematical	`Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card`	`stepBound`	—	—
`mul_sq_le_sum_sq` 📖	mathematical	`Finset` `Finset.instHasSubset` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Finset.card`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	—	`mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `LE.le.trans` `sum_div_card_sq_le_sum_sq_div_card` `AddGroup.existsAddOfLE` `le_of_lt` `lt_of_le_of_ne'` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toZeroLEOneClass` `mul_div_cancel₀` `Finset.sum_le_sum_of_subset_of_nonneg` `Even.pow_nonneg` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul`
`one_le_m_coe` 📖	mathematical	`Finset.card` `Finset` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot` `Finset.univ` `Monoid.toNatPow` `Nat.instMonoid` `Fintype.card`	`Real` `Real.instLE` `Real.instOne` `Real.instNatCast` `stepBound`	—	`Nat.one_le_cast` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `m_pos`
`pow_mul_m_le_card_part` 📖	mathematical	`Finpartition.IsEquipartition` `Finset.univ` `Finset` `Finset.instMembership` `Finpartition.parts` `Finset.instLattice` `Finset.instOrderBot`	`Real` `Real.instLE` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `Finset.card` `Fintype.card` `stepBound`	—	`Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `stepBound.eq_1` `LE.le.trans` `Finpartition.IsEquipartition.average_le_card_part`
`seven_le_initialBound` 📖	mathematical	—	`initialBound`	—	`le_max_left` `Real.instIsStrictOrderedRing`
`stepBound_mono` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `stepBound`	—	`mul_le_mul'` `Nat.instMulLeftMono` `covariant_swap_mul_of_covariant_mul` `pow_le_pow_right'`
`stepBound_pos` 📖	mathematical	—	`stepBound`	—	`stepBound_pos_iff`
`stepBound_pos_iff` 📖	mathematical	—	`stepBound`	—	`mul_pos_iff_of_pos_right` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.instIsStrictOrderedRing` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat`

SzemerediRegularity.Positivity

Definitions

Name	Category	Theorems
`tacticSz_positivity` 📖	CompOp	—

---

← Back to Index