Probability makes counting (sometimes) easy

Structure

• Theorem 1
  • proof
• Ramsey Numbers
• Theorem 2
  • proof
• Triangle-free graphs with high chromatic number (TODO)
• Theorem 3
  • proof
• Theorem 4 (TODO : Define crossing number)

def chapter45.two_colorable {α : Type u_1} {X : Finset α} (𝓕 : Finset (Finset { x : α // x ∈ X })) : Prop

𝓕 is a collection of d-sets of X

Equations

• chapter45.two_colorable 𝓕 = ∃ (c : { x : α // x ∈ X } → Fin 2), ∀ A ∈ 𝓕, ∃ (x : { x : { x : α // x ∈ X } // x ∈ A }) (y : { x : { x : α // x ∈ X } // x ∈ A }), c ↑x = 0 ∧ c ↑y = 1

theorem chapter45.remark_1 {d : ℕ} : ∃ (α : Type) (X : Finset α) (𝓕 : Finset (Finset { x : α // x ∈ X })), (∀ A ∈ 𝓕, A.card = d) ∧ ¬two_colorable 𝓕

theorem chapter45.remark_2 {α : Type u_1} [DecidableEq α] {X : Finset α} {𝓕 𝓢 : Finset (Finset { x : α // x ∈ X })} (h₁ : two_colorable 𝓕) (h₂ : 𝓢 ⊆ 𝓕) : two_colorable 𝓢

theorem chapter45.ENNReal.mul_inv_eq_iff_eq_mul {a b c : ENNReal} (h0 : b ≠ 0) (ha : a ≠ ⊤) (hb : b ≠ ⊤) (hc : c ≠ ⊤) : a * b⁻¹ = c ↔ a = c * b

theorem chapter45.MeasureTheory.measure_biUnion_lt_sum_of_inter {α : Type u_2} [DecidableEq α] {β : Type u_1} [MeasurableSpace β] [MeasurableSingletonClass β] [DecidableEq β] {P : MeasureTheory.Measure β} [MeasureTheory.IsFiniteMeasure P] (s : Finset α) (t : α → Finset β) (h : ∃ (i : { x : α // x ∈ s }) (j : { x : α // x ∈ s }), i ≠ j ∧ P (↑(t ↑i) ∩ ↑(t ↑j)) ≠ 0) : P ↑(s.biUnion t) < ∑ x ∈ s, P ↑(t x)

theorem chapter45.theorem_1 {α : Type u_1} [DecidableEq α] {X : Finset α} {d : ℕ} {h_d : d ≥ 2} (𝓕 : Finset (Finset { x : α // x ∈ X })) (H_𝓕 : ∀ A ∈ 𝓕, A.card = d) : 𝓕.card ≤ 2 ^ (d - 1) → two_colorable 𝓕

Ramsey Numbers and Theorem 2

def chapter45.ramsey_property (m n N : ℕ) : Prop

A complete graph G on N vertices has the Ramsey property R(m, n), if for each two-coloring of the edges of G, either there is a complete subgraph on m vertices of the first color, or there is a complete subgraph on n vertices in the second color.

Equations

• One or more equations did not get rendered due to their size.

theorem chapter45.ramsey_exists (m n : ℕ) (h_m : m ≥ 2) (h_n : n ≥ 2) : ∃ (N : ℕ), ramsey_property m n N