FormalConjectures/ErdosProblems/65.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

2 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 65

References:

Imports (1)
  1. theorem Erdos65.erdos_65.parts.i Let $G$ be a graph with $n$ vertices and $kn$ edges, and $a_10$ and $k>0$ sorry line 44 source

    Source documentation

    Let $G$ be a graph with $n$ vertices and $kn$ edges, and $a_1<a_2<\cdots$ be the lengths of cycles in $G$. Assume $n>0$ and $k>0$. Is it true that $$\sum\frac{1}{a_i}\gg \log k?$$

    Gyárfás, Komlós, and Szemerédi [GKS84] have proved that this sum is $\gg \log k$, so that only the second question remains.

    L4DEL explanation

    Let $G$ be a graph with $n$ vertices and $kn$ edges, and $a_10$ and $k>0$. Is it true that $$\sum\frac{1}{a_i}\gg \log k?$$ Gyárfás, Komlós, and Szemerédi [GKS84] have proved that this sum is $\gg \log k$, so that only the second question remains.

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Real, And, GT.gt, OfNat.ofNat, LT.lt, Nat, Fintype, SimpleGraph, Eq, Fintype.card, Set.ncard, Sym2, SimpleGraph.edgeSet, HMul.hMul, GE.ge, finsum, Membership.mem and 4 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_65.parts.i : answer(True) ↔
    ∃ c > (0 : ℝ), ∀ (k : ℝ) (hk : 0 < k),
      ∀ (n : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V),
        0 < n →
        Fintype.card V = n →
        (G.edgeSet.ncard : ℝ) = k * n →
        (∑ᶠ a ∈ G.cycleLengths, (1 : ℝ) / a) ≥ c * Real.log k := by
…

    Mentions: c

  2. theorem Erdos65.erdos_65.parts.ii Is the sum $\sum\frac{1}{a_i}$ minimised when $G$ is a complete bipartite graph? sorry line 59 source

    Source documentation

    Is the sum $\sum\frac{1}{a_i}$ minimised when $G$ is a complete bipartite graph?

    This problem is #65 in Extremal Graph Theory in the graphs problem collection.

    depends on sorry what this means

    Statement uses: Iff, True, Real, LT.lt, OfNat.ofNat, Nat, Fintype, SimpleGraph, Eq, Fintype.card, Set.ncard, Sym2, SimpleGraph.edgeSet, HMul.hMul, Sum, completeBipartiteGraph, LE.le, finsum, Membership.mem, Set and 2 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_65.parts.ii : answer(sorry) ↔
    ∀ (k : ℝ) (hk : 0 < k),
      ∀ (n : ℕ) (V : Type) [Fintype V] (G : SimpleGraph V),
        0 < n →
        Fintype.card V = n →
        (G.edgeSet.ncard : ℝ) = k * n →
        ∀ (A B : Type) [Fintype A] [Fintype B],
          Fintype.card (A ⊕ B) = n →
          ((completeBipartiteGraph A B).edgeSet.ncard : ℝ) = k * n →
          (∑ᶠ a ∈ (completeBipartiteGraph A B).cycleLengths, (1 : ℝ) / a) ≤
            (∑ᶠ a ∈ G.cycleLengths, (1 : ℝ) / a) := by
…