@[reducible, inline]

abbrev SimpleGraph.EdgeColoring {V : Type α} {G : SimpleGraph V} (C : Type) : Type α

An edge coloring maps each member of the graph's edge set to a colour in C -

Equations

• SimpleGraph.EdgeColoring C = (↑G.edgeSet → C)

def SimpleGraph.EdgeColoring.coloredNeighborSet {V : Type α} {G : SimpleGraph V} {C : Type} {EC : EdgeColoring C} (c : C) (v : V) : Set V

EC.coloredNeighborSet c v is the set of vertices that have an edge to v in G which is colored with c under the edge coloring EC.

Equations

• SimpleGraph.EdgeColoring.coloredNeighborSet c v = {w : V | ∃ (p : G.Adj v w), EC ⟨s(v, w), p⟩ = c}

instance SimpleGraph.EdgeColoring.coloredNeighborSetFintype {V : Type α} {G : SimpleGraph V} {C : Type} {c : C} {v : V} [Fintype V] [DecidableRel G.Adj] [DecidableEq C] {EC : EdgeColoring C} : Fintype ↑(coloredNeighborSet c v)

Equations

• SimpleGraph.EdgeColoring.coloredNeighborSetFintype = id (Subtype.fintype fun (w : V) => ∃ (p : G.Adj v w), EC ⟨s(v, w), p⟩ = c)

def SimpleGraph.EdgeColoring.coloredNeighborFinset {V : Type α} {G : SimpleGraph V} {C : Type} {EC : EdgeColoring C} (c : C) (v : V) [Fintype ↑(coloredNeighborSet c v)] : Finset V

EC.coloredNeighborFinset c v is the Finset of vertices that have c-colored edge to v in G under the edge coloring EC, in case the c-colored subgraph of G is locally finite at v.

Equations

• SimpleGraph.EdgeColoring.coloredNeighborFinset c v = (SimpleGraph.EdgeColoring.coloredNeighborSet c v).toFinset

theorem moments {V : Type u_1} {r : ℕ} (X : Type) [Fintype X] [Nonempty X] [MeasurableSpace X] [Fintype V] (σ : Fin r → X → V → ℝ) (l : Fin r → ℕ) (U : MeasureTheory.Measure (X × X)) : 0 ≤ ∫ (x : X × X), (fun (xx : X × X) => ∏ i : Fin r, (σ i xx.1 ⬝ᵥ σ i xx.2) ^ l i) x ∂U

theorem tsum_even_nat {T : Type u_1} [TopologicalSpace T] [AddCommMonoid T] (f : ℕ → T) : ∑' (x : ↑{n : ℕ | Even n}), f ↑x = ∑' (x : ℕ), f (2 * x)

noncomputable def coshsqrt (x : ℝ) : ℝ

Equations

• coshsqrt x = ∑' (n : ℕ), x ^ n / ↑(2 * n).factorial

theorem mew {x : ℝ} (xpos : 0 ≤ x) : Summable fun (n : ℕ) => x ^ n / ↑(2 * n).factorial

theorem lt_coshsqrt (x : ℝ) (xnn : 0 ≤ x) : x < 2 + coshsqrt x

theorem ge_coshsqrt (x : ℝ) (xnn : 0 ≤ x) : 2 + coshsqrt x ≤ 3 * Real.exp √x

theorem icc_coshsqrt_neg (x : ℝ) (xnn : x ≤ 0) : coshsqrt x ∈ Set.Icc (-1) 1

theorem coshsqrt_pos {x : ℝ} (xn : x ≤ 0) : 0 < 2 + coshsqrt x

theorem coshsqrt_nonneg {x : ℝ} : 0 ≤ 2 + coshsqrt x

theorem coshsqrt_mono {x y : ℝ} (xnn : 0 ≤ x) (xly : x ≤ y) : coshsqrt x ≤ coshsqrt y

theorem one_le_coshsqrt (x : ℝ) : 1 ≤ 2 + coshsqrt x

theorem Finset.one_le_prod''' {R : Type u_2} {ι : Type u_1} [CommMonoidWithZero R] [PartialOrder R] [ZeroLEOneClass R] [PosMulMono R] {f : ι → R} {s : Finset ι} (h : ∀ i ∈ s, 1 ≤ f i) : 1 ≤ ∏ i ∈ s, f i

noncomputable def f {r : ℕ} (x : Fin r → ℝ) : ℝ

Equations

• f x = ∑ j : Fin r, x j * (1 / (2 + coshsqrt (x j))) * ∏ i : Fin r, (2 + coshsqrt (x i))

theorem specialFunctionE {r : ℕ} (x : Fin r → ℝ) : f x ≤ 3 ^ r * ↑r * Real.exp (∑ i : Fin r, √(x i + 3 * ↑r))

theorem specialFunctionEc {r : ℕ} (rpos : 0 < r) (x : Fin r → ℝ) (h : ∃ (i : Fin r), x i < -3 * ↑r) : f x ≤ -1

theorem Fintype.exists_mul_of_sum_bound {X : Type u_1} {Y : Type u_2} [Nonempty X] [Fintype X] [AddCommMonoid Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (g : X → Y) : ∃ (j : X), ∑ i : X, g i ≤ card X • g j

theorem Finset.exists_mul_of_sum_bound {X : Type u_1} {Y : Type u_2} [Nonempty X] [Fintype X] [AddCommMonoid Y] [LinearOrder Y] [IsOrderedAddMonoid Y] (s : Finset X) (g : X → Y) (ns : s.Nonempty) : ∃ j ∈ s, ∑ i ∈ s, g i ≤ s.card • g j

theorem Finset.exists_le_expect {ι : Type u_1} {α : Type u_2} [AddCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] [Module ℚ≥0 α] [PosSMulMono ℚ≥0 α] {s : Finset ι} {f : ι → α} (hs : s.Nonempty) : ∃ x ∈ s, s.expect f ≤ f x

theorem Fin.exists_mul_of_sum_bound {r : ℕ} [Nonempty (Fin r)] (g : Fin r → ENNReal) : ∃ (j : Fin r), ∑ i : Fin r, g i ≤ ↑r * g j

theorem probabilistic_method {X : Type} [Fintype X] [MeasurableSpace X] (U : MeasureTheory.Measure X) (p : X → X → Prop) [(i j : X) → Decidable (p j i)] : 0 < (U.prod U) {x : X × X | p x.1 x.2} → ∃ (x : X) (x' : X), p x x'

theorem pidgeon_sum {X Y : Type} [nenx : Nonempty X] [fin : Fintype X] [nen : Nonempty Y] [fin✝ : Fintype Y] (p : X → Y → Prop) [(i : X) → (j : Y) → Decidable (p i j)] {β : ℝ} : β ≤ ↑(Fintype.card ↑{x : X × Y | p x.1 x.2}) / ↑(Fintype.card (X × Y)) → ∃ (x : X) (Y' : Finset Y), β * ↑(Fintype.card Y) ≤ ↑Y'.card ∧ ∀ y ∈ Y', p x y

theorem pidgeon_thing {X Y : Type} [Nonempty X] [Fintype X] [Nonempty Y] [Fintype Y] [MeasurableSpace (X × Y)] [MeasurableSingletonClass (X × Y)] (p : X × Y → Prop) [(i : X × Y) → Decidable (p i)] {β : ℝ} : let U := (PMF.uniformOfFintype (X × Y)).toMeasure; ENNReal.ofReal β ≤ U {x : X × Y | p x} → ∃ (x : X) (Y' : Finset Y), β * ↑(Fintype.card Y) ≤ ↑Y'.card ∧ ∀ y ∈ Y', p (x, y)

theorem prod_set_eq_union {X Y : Type} (f : X × Y → Prop) : {a : X × Y | f a} = ⋃ (x : X), {x} ×ˢ {y : Y | f (x, y)}

theorem Fintype.argmax' {X Y : Type} [Fintype X] [Nonempty X] (f : X → Y) [LinearOrder Y] : ∃ (x : X), ∀ (y : X), f y ≤ f x

theorem maxUnion {Λ : ℝ} {X Y : Type} [Fintype X] [Nonempty X] [LinearOrder X] (τ : Y → X → ℝ) (nen : ∀ (x : Y), (Finset.image (τ x) Finset.univ).Nonempty) : {x : Y | Λ ≤ (Finset.image (τ x) Finset.univ).max' ⋯} = ⋃ (i : X), {x : Y | Λ ≤ τ x i}

theorem sum_sqrt_le {r : ℕ} {X : Type u_1} [Fintype X] [nenr : Nonempty (Fin r)] {τ : X → Fin r → ℝ} {x : X} : let M := fun (x : X) => (Finset.image (τ x) Finset.univ).max' ⋯; ∑ i : Fin r, √(3 * ↑r * τ x i + 3 * ↑r) ≤ ↑r * (√3 * √↑r) * √(M x + 1)

theorem three_ineq_ENN {r : ℕ} (rpos : 0 < r) : ↑r * ENNReal.ofReal (3 ^ (-(↑r * 4))) * 3 ^ r * 3 + ↑r ^ 2 * ENNReal.ofReal (3 ^ (-(↑r * 4))) * ENNReal.ofReal (↑r * √3 * √↑r) * 3 ^ r * 3 ≤ 1

theorem omg {a b : ℝ} (p : b ≠ 0) : a = a / b * b

theorem omg2 {a b c : ℝ} (p : b ≠ 0) : a ≤ c ↔ a / b ≤ c / b

theorem omg3 {a b : ℝ} (p : b ≠ 0) : a = a * b / b

theorem omg4 {a b c : ℝ} (bnn : 0 ≤ b) : a ≤ c ↔ a * b ≤ c * b

theorem omg5 {a b c : ENNReal} : b ≤ c ↔ a * b ≤ a * c

theorem omg6 {a b : ℝ} : -a ≤ a * b ↔ -1 ≤ b

theorem omg7 (a b c : ENNReal) (ab : a < b) (ac : a < c) (bc : b < c) : c - b < c - a