Documentation Verification Report

TuranDensity

📁 Source: Mathlib/Combinatorics/SimpleGraph/Extremal/TuranDensity.lean

Statistics

Metric	Count
Definitions `turanDensity`, `turanDensityConst`	2
Theorems `antitoneOn_extremalNumber_div_choose_two`, `eventually_isContained_of_card_edgeFinset`, `isContained_of_card_edgeFinset`, `isEquivalent_extremalNumber`, `isGLB_turanDensity`, `tendsto_turanDensity`, `turanDensity_eq_csInf`	7
Total	9

SimpleGraph

Definitions

Name	Category	Theorems
`turanDensity` 📖	CompOp	4 math math: `turanDensity_eq_csInf`, `tendsto_turanDensity`, `isGLB_turanDensity`, `isEquivalent_extremalNumber`
`turanDensityConst` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitoneOn_extremalNumber_div_choose_two` 📖	mathematical	—	`AntitoneOn` `Real` `Nat.instPreorder` `Real.instPreorder` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `extremalNumber` `Nat.choose` `Set.Ici`	—	`antitoneOn_nat_Ici_of_succ_le` `Fintype.card_fin` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Nat.choose_pos` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Nat.instAtLeastTwoHAddOfNat` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `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.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `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.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.mul_neg` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Int.instCharZero` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Nat.cast_add` `Nat.cast_one` `extremalNumber_le_iff_of_nonneg` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Nat.cast_nonneg'` `mul_comm` `mul_div_assoc` `le_div_iff₀'` `Nat.cast_choose_two` `CharZero.NeZero.two` `Nat.cast_add_one` `add_sub_cancel_right` `mul_div` `mul_assoc` `mul_le_mul_iff_right₀` `div_pos` `Nat.cast_pos'` `NeZero.charZero_one` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `Real.instNontrivial` `Mathlib.Meta.NormNum.instAtLeastTwo` `Nat.cast_pred` `Nat.cast_mul` `Nat.cast_le` `Finset.card_univ` `Finset.card_nsmul_le_card_nsmul'` `Finset.bipartiteBelow.congr_simp` `Finset.filter_not` `Finset.filter_mem_eq_inter` `Finset.univ_inter` `Finset.card_compl` `card_toFinset_mem_edgeFinset` `edgeFinset_deleteIncidenceSet_eq_filter` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `Nat.instIsOrderedAddMonoid` `card_edgeFinset_deleteIncidenceSet_le_extremalNumber`
`eventually_isContained_of_card_edgeFinset` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Eventually` `Filter.atTop` `Nat.instPreorder`	—	`Eq.ge` `turanDensity_eq_csInf` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_forall_eq` `lt_of_lt_of_le` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `le_csInf` `Set.image.eq_1` `Set.image_nonempty` `Set.nonempty_Ici` `not_nonempty_iff` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_zero` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toCharZero` `Nat.choose_pos` `LE.le.trans` `Fintype.card_fin` `card_edgeFinset_le_extremalNumber` `antitoneOn_extremalNumber_div_choose_two`
`isContained_of_card_edgeFinset` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Fintype.card` `turanDensityConst` `Real.instLE` `Real.instNatCast` `Finset.card` `Sym2` `edgeFinset` `fintypeEdgeSet` `Sym2.instFintype` `Real.instMul` `Real.instAdd` `turanDensity` `Nat.choose`	`IsContained`	—	`Iso.card_edgeFinset_eq` `isContained_congr` `Nat.find_spec` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `eventually_isContained_of_card_edgeFinset`
`isEquivalent_extremalNumber` 📖	mathematical	—	`Asymptotics.IsEquivalent` `Real` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.atTop` `Nat.instPreorder` `Real.instNatCast` `extremalNumber` `Real.instMul` `turanDensity` `Nat.choose`	—	`tendsto_turanDensity` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `Nat.instNoMaxOrder` `Asymptotics.isEquivalent_iff_tendsto_one` `one_mul` `div_mul_div_comm` `one_div_mul_cancel` `Filter.Tendsto.const_mul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal`
`isGLB_turanDensity` 📖	mathematical	—	`IsGLB` `Real` `Real.instLE` `setOf` `Set` `Set.instMembership` `Set.Ici` `Nat.instPreorder` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `extremalNumber` `Nat.choose` `turanDensity`	—	`div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `Real.isGLB_of_tendsto_antitoneOn_bddBelow_nat_Ici` `Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici` `antitoneOn_extremalNumber_div_choose_two` `Filter.Tendsto.limUnder_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`tendsto_turanDensity` 📖	mathematical	—	`Filter.Tendsto` `Real` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `extremalNumber` `Nat.choose` `Filter.atTop` `Nat.instPreorder` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `turanDensity`	—	`Real.tendsto_atTop_csInf_of_antitoneOn_bddBelow_nat_Ici` `antitoneOn_extremalNumber_div_choose_two` `IsGLB.bddBelow` `isGLB_turanDensity` `turanDensity.eq_1` `Filter.Tendsto.limUnder_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Filter.atTop_neBot` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat`
`turanDensity_eq_csInf` 📖	mathematical	—	`turanDensity` `InfSet.sInf` `Real` `Real.instInfSet` `setOf` `Set` `Set.instMembership` `Set.Ici` `Nat.instPreorder` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instNatCast` `extremalNumber` `Nat.choose`	—	`isGLB_turanDensity` `IsGLB.csInf_eq` `IsGLB.nonempty` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instIsOrderedRing` `Real.instNontrivial`

---

← Back to Index