Documentation Verification Report

RuzsaSzemeredi

📁 Source: Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean

Statistics

Metric	Count
Definitions `ruzsaSzemerediNumber`, `ruzsaSzemerediNumberNat`	2
Theorems `le_ruzsaSzemerediNumber`, `addRothNumber_le_ruzsaSzemerediNumber`, `rothNumberNat_le_ruzsaSzemerediNumberNat`, `rothNumberNat_le_ruzsaSzemerediNumberNat'`, `ruzsaSzemerediNumberNat_asymptotic_lower_bound`, `ruzsaSzemerediNumberNat_card`, `ruzsaSzemerediNumberNat_le`, `ruzsaSzemerediNumberNat_lower_bound`, `ruzsaSzemerediNumberNat_mono`, `ruzsaSzemerediNumberNat_one`, `ruzsaSzemerediNumberNat_two`, `ruzsaSzemerediNumberNat_zero`, `ruzsaSzemerediNumber_congr`, `ruzsaSzemerediNumber_le`, `ruzsaSzemerediNumber_mono`, `ruzsaSzemerediNumber_spec`	16
Total	18

SimpleGraph.LocallyLinear

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_ruzsaSzemerediNumber` 📖	mathematical	`SimpleGraph.LocallyLinear`	`Finset.card` `Finset` `SimpleGraph.cliqueFinset` `ruzsaSzemerediNumber`	—	`Nat.le_findGreatest` `SimpleGraph.card_cliqueFinset_le`

(root)

Definitions

Name	Category	Theorems
`ruzsaSzemerediNumber` 📖	CompOp	7 math math: `ruzsaSzemerediNumber_congr`, `ruzsaSzemerediNumber_spec`, `addRothNumber_le_ruzsaSzemerediNumber`, `ruzsaSzemerediNumber_le`, `ruzsaSzemerediNumber_mono`, `SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumber`, `ruzsaSzemerediNumberNat_card`
`ruzsaSzemerediNumberNat` 📖	CompOp	10 math math: `ruzsaSzemerediNumberNat_le`, `ruzsaSzemerediNumberNat_two`, `rothNumberNat_le_ruzsaSzemerediNumberNat`, `ruzsaSzemerediNumberNat_zero`, `ruzsaSzemerediNumberNat_card`, `ruzsaSzemerediNumberNat_one`, `ruzsaSzemerediNumberNat_lower_bound`, `rothNumberNat_le_ruzsaSzemerediNumberNat'`, `ruzsaSzemerediNumberNat_asymptotic_lower_bound`, `ruzsaSzemerediNumberNat_mono`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addRothNumber_le_ruzsaSzemerediNumber` 📖	mathematical	—	`Fintype.card` `DFunLike.coe` `OrderHom` `Finset` `PartialOrder.toPreorder` `Finset.partialOrder` `Nat.instPreorder` `OrderHom.instFunLike` `addRothNumber` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Finset.univ` `ruzsaSzemerediNumber` `instFintypeSum`	—	`Nat.instAtLeastTwoHAddOfNat` `addRothNumber_spec` `SimpleGraph.TripartiteFromTriangles.card_triangles` `SimpleGraph.LocallyLinear.le_ruzsaSzemerediNumber`
`rothNumberNat_le_ruzsaSzemerediNumberNat` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `rothNumberNat` `ruzsaSzemerediNumberNat`	—	`Fin.addRothNumber_eq_rothNumberNat` `le_rfl` `Fintype.card_fin` `mul_le_mul_right` `Nat.instMulLeftMono` `OrderHomClass.mono` `OrderHom.instOrderHomClass` `Finset.subset_univ` `addRothNumber_le_ruzsaSzemerediNumber` `Units.isUnit` `Fintype.card_sum` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.RingNF.nat_rawCast_1` `pow_one` `add_zero`
`rothNumberNat_le_ruzsaSzemerediNumberNat'` 📖	mathematical	—	`Real` `Real.instLE` `Real.instMul` `Real.instSub` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderHom.instFunLike` `rothNumberNat` `ruzsaSzemerediNumberNat`	—	`Nat.instAtLeastTwoHAddOfNat` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `zero_div` `zero_sub` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `MulZeroClass.mul_zero` `ruzsaSzemerediNumberNat_zero` `Nat.cast_one` `one_div` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `ruzsaSzemerediNumberNat_one` `ruzsaSzemerediNumberNat_two` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_add` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_natCast` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_mul` `AddGroup.toOrderedSub` `covariant_swap_add_of_covariant_add` `Real.instIsOrderedAddMonoid` `div_add_one` `three_ne_zero'` `ZeroLEOneClass.neZero.three` `Real.instZeroLEOneClass` `NeZero.charZero_one` `le_sub_iff_add_le` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `zero_lt_three'` `add_assoc` `add_sub_assoc` `add_mul` `Distrib.rightDistribClass` `mul_right_comm` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_sub` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_add` `LT.lt.le` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Nat.cast_nonneg` `rothNumberNat_le_ruzsaSzemerediNumberNat` `le_imp_le_of_le_of_le` `Nat.mono_cast` `ruzsaSzemerediNumberNat_mono` `add_le_add_left` `le_refl`
`ruzsaSzemerediNumberNat_asymptotic_lower_bound` 📖	mathematical	—	`Asymptotics.IsBigO` `Real` `Real.norm` `Filter.atTop` `Nat.instPreorder` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast` `Real.exp` `Real.instNeg` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.sqrt` `Real.log` `ruzsaSzemerediNumberNat`	—	`Asymptotics.IsBigO.trans` `Nat.instAtLeastTwoHAddOfNat` `sq` `Asymptotics.IsBigO.mul` `NormedDivisionRing.toNormMulClass` `div_eq_inv_mul` `Asymptotics.IsBigO.const_mul_right` `RCLike.charZero_rclike` `Asymptotics.isBigO_refl` `Asymptotics.IsLittleO.right_isBigO_sub` `norm_mul` `norm_inv` `Real.norm_ofNat` `RCLike.norm_natCast` `Filter.Tendsto.atTop_of_const_mul₀` `Real.instIsStrictOrderedRing` `zero_lt_three` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_inv_cancel_left₀` `Real.instIsOrderedRing` `Real.instArchimedean` `Asymptotics.IsBigO_def` `Asymptotics.IsBigOWith_def` `Real.norm_natCast` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Real.isBigO_exp_comp_exp_comp` `neg_mul` `sub_neg_eq_add` `add_zero` `IsOrderedRing.toPosMulMono` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instNontrivial` `Real.sqrt_monotone` `Real.log_le_log` `Nat.instNontrivial` `Nat.mono_cast` `Asymptotics.IsBigO.of_norm_eventuallyLE` `Filter.mp_mem` `Filter.eventually_ge_atTop` `Filter.univ_mem'` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.atom_pf` `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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_congr` `Nat.cast_one` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Int.cast_ofNat` `Int.cast_natCast` `Rat.cast_natCast` `CancelDenoms.sub_subst` `CancelDenoms.div_subst` `Mathlib.Meta.NormNum.isNat_eq_true` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_div` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.isNNRat_mul` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Mathlib.Tactic.Linarith.mul_neg` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Mathlib.Meta.NormNum.isNat_lt_true` `abs_of_nonneg` `Real.abs_exp` `ruzsaSzemerediNumberNat_lower_bound`
`ruzsaSzemerediNumberNat_card` 📖	mathematical	—	`ruzsaSzemerediNumberNat` `Fintype.card` `ruzsaSzemerediNumber`	—	`ruzsaSzemerediNumber_congr`
`ruzsaSzemerediNumberNat_le` 📖	mathematical	—	`ruzsaSzemerediNumberNat` `Nat.choose`	—	`LE.le.trans_eq` `ruzsaSzemerediNumber_le` `Fintype.card_fin`
`ruzsaSzemerediNumberNat_lower_bound` 📖	mathematical	—	`Real` `Real.instLE` `Real.instMul` `Real.instSub` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat` `Real.exp` `Real.instNeg` `Real.sqrt` `Real.log` `ruzsaSzemerediNumberNat`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_assoc` `le_total` `LE.le.trans` `mul_nonpos_of_nonpos_of_nonneg` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `le_of_lt` `Real.exp_pos` `Nat.cast_nonneg` `mul_le_mul_of_nonneg_left` `Behrend.roth_lower_bound` `rothNumberNat_le_ruzsaSzemerediNumberNat'`
`ruzsaSzemerediNumberNat_mono` 📖	mathematical	—	`Monotone` `Nat.instPreorder` `ruzsaSzemerediNumberNat`	—	`ruzsaSzemerediNumber_mono`
`ruzsaSzemerediNumberNat_one` 📖	mathematical	—	`ruzsaSzemerediNumberNat`	—	`le_zero_iff` `ruzsaSzemerediNumberNat_le`
`ruzsaSzemerediNumberNat_two` 📖	mathematical	—	`ruzsaSzemerediNumberNat`	—	`le_zero_iff` `ruzsaSzemerediNumberNat_le`
`ruzsaSzemerediNumberNat_zero` 📖	mathematical	—	`ruzsaSzemerediNumberNat`	—	`le_zero_iff` `ruzsaSzemerediNumberNat_le`
`ruzsaSzemerediNumber_congr` 📖	mathematical	—	`ruzsaSzemerediNumber`	—	`LE.le.antisymm` `ruzsaSzemerediNumber_mono`
`ruzsaSzemerediNumber_le` 📖	mathematical	—	`ruzsaSzemerediNumber` `Nat.choose` `Fintype.card`	—	`Nat.findGreatest_le`
`ruzsaSzemerediNumber_mono` 📖	mathematical	—	`ruzsaSzemerediNumber`	—	`Nat.findGreatest_mono` `Finset.map_injective` `Finset.card_map` `SimpleGraph.cliqueFinset_map` `SimpleGraph.LocallyLinear.map` `Nat.choose_mono` `Fintype.card_le_of_embedding`
`ruzsaSzemerediNumber_spec` 📖	mathematical	—	`Finset.card` `Finset` `SimpleGraph.cliqueFinset` `ruzsaSzemerediNumber` `SimpleGraph.LocallyLinear`	—	`Nat.findGreatest_spec` `SimpleGraph.locallyLinear_bot`

---

← Back to Index