Advice on PR strategy for Shearer’s Theorem

Stream: graph theory

[Pjotr Buys]

A few months ago I made a post about Shearer's Theorem (the main theorem from this (https://doi.org/10.1016/0012-365X(83)90273-X)). One of my motivations was to formally prove one of my own results (which I have now done https://github.com/Pjotr5/ShearerTriangleFreeInd). Another motivation was to contribute to Mathlib. I would like some advice on how to go about this.

I made PR (https://github.com/leanprover-community/mathlib4/pull/27155) with my formalization of Shearer's Theorem, but I realize now that many parts of it should probably go to different parts of Mathlib and thus that it is probably a better idea to start splitting this thing up in many smaller PRs (which I was already advised to do anyway). This will also make it easier for me to get the code up to Mathlib standards and for reviewers to potentially help me. Some questions.

1. I define the average degree of a graph
   noncomputable def averageDegree {V : Type} [Fintype V] (G : SimpleGraph V) := 𝔼 v, (G.degree v : ℚ)
   This is a fairly common notion in Graph Theory and thus I guess should go to its own place in Mathlib. Should this get its own file in Mathlib and if so, are people happy with this definition?

2. The proof involves the analysis of a specific function:

def F : ℝ → ℝ := fun x ↦
          if x = 1 then 1/2
          else          (x * Real.log x - x + 1) / (x - 1)^2

To analyse thise function I proved some analysis Lemmas that are maybe too specific to go to their own place in Mathlib. For example I proved

lemma frequently_deriv_eq_zero_of_frequently_eq_zero {g g' : ℝ → ℝ}
            (hx : g x = 0)
            (hDer : ∀ᶠ (y : ℝ) in nhds x, HasDerivAt g (g' y) y)
            (hgZero : ∃ᶠ (y : ℝ) in nhdsWithin x {x}ᶜ, g y = 0) :
            ∃ᶠ (y : ℝ) in nhdsWithin x {x}ᶜ, g' y = 0

Or: it was very useful for me to prove a lemma proving the continuity of functions such as F at their removable singularity where the order of the zero in the denominator and numerator is possibly greater than one. I found a following "list" version of repeatedly applying L'Hopital most useful:

lemma lhopital_iterated (n : ℕ) (ns ds : List (ℝ → ℝ))
            (hnslen : ns.length = n + 1) (hdslen : ds.length = n + 1)
            (hnDer : ∀ k (hk : k < n), ∀ᶠ (y : ℝ) in nhds x, HasDerivAt ns[k] (ns[k + 1] y) y)
            (hdDer : ∀ k (hk : k < n), ∀ᶠ (y : ℝ) in nhds x, HasDerivAt ds[k] (ds[k + 1] y) y)
            (hnZero : ∀ k (hk : k < n), ns[k] x = 0)
            (hdZero : ∀ k (hk : k < n), ds[k] x = 0)
            (hnCont : ContinuousAt ns[n] x)
            (hdCont : ContinuousAt ds[n] x)
            (hdFinal : ds[n] x ≠ 0) :
            ContinuousAt
                (fun y ↦ if y = x
                  then (ns[n] x) / (ds[n] x)
                  else (ns[0] y) / (ds[0] y))
                x

Or even more specific something like the following argument came up so many times that I gave it its own name:

    `lemma pos_of_dist_one_lt_one (hx : dist x 1 < 1) : 0 < x`

What should generally be done with lemmas like this?

3. There are definitions that are very specific to this particular problem. For example I define the numerator and its derivatives of the above function F (in a noncomputable section):

def nF₀ : ℝ → ℝ := fun x ↦ x * Real.log x - x + 1
        def nF₁ : ℝ → ℝ := fun x ↦ Real.log x
        def nF₂ : ℝ → ℝ := fun x ↦ 1/x

Is it okay to define things like this in a particular file that are only relevant for the proof of the statement in that file or should something like that be avoided?

Generally I am motivated to work on this but I also find it a bit daunting (having never contributed anything to Mathlib). So any advice where to start would be appreciated.

[Bhavik Mehta]

For 1: for now I think it can go in the same file as minDegree. For 2: it's hard to tell, my guess is that the first one you mentioned could be useful for mathlib in general, but the last one should be private lemma in your file, and the middle one isn't yet clear to me: I suspect something more direct could work here, but I'm not sure. For 3: I think nF0 should be a private def, and the others can be inlined. It's okay to have private def in the particular file, but having too many can get awkward, and since nF1 is exactly the same as Real.log, you might as well just use that.

[Pjotr Buys]

Thanks! I drafted some basic average degree lemmas here. Do you think this looks reasonable?

Some more concepts that I am curious where they would belong in Mathlib (if its not too much of a bother):

1. For Shearer proof I argue a lot about the closed neighborhood of a vertex. I define it as

     `def closedNeighborSet := insert v (G.neighborSet v)`

   It is a common concept so I am wondering if it should get its own place (not just in the local file). The following recursion is central to the Shearer argument:

     `lemma indepSet_insert_bound (v : V) : α(G) ≥ α(G.induce (G.closedNeighborSet v)ᶜ) + 1`

   Here I have scoped notation "α(" G ")" => indepNum G. I guess some form of this lemma does fit in the independence/clique file?

2. I used the concept of the set of edges incident to a set of vertices:

     `noncomputable def EdgeIncidenceFinset (S : Set V) := filter (∃ v ∈ S, v ∈ ·) (edgeFinset G)`

Relevant for Shearer becuase for example:

lemma incident_closedNeighbor_card (hT : G.CliqueFree 3) (v : V) :
        #(G.EdgeIncidenceFinset (G.closedNeighborSet v)) = ∑ u ∈ G.neighborFinset v, G.degree u

Is this a concept that might be useful to get its own place in Mathlib?