def SimpleGraph.EdgeLabelling.coloredNeighborSet {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {EC : G.EdgeLabelling K} (c : K) (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.EdgeLabelling.coloredNeighborSet c v = {w : V | w ∈ G.neighborSet v ∧ ∃ (p : s(v, w) ∈ G.edgeSet), EC ⟨s(v, w), p⟩ = c}

theorem SimpleGraph.EdgeLabelling.coloredNeighborSet_not_mem {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {EC : G.EdgeLabelling K} (c : K) (v : V) : v ∉ coloredNeighborSet c v

instance SimpleGraph.EdgeLabelling.coloredNeighborSetFintype {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {c : K} {EC : G.EdgeLabelling K} {v : V} [Fintype V] [DecidableRel G.Adj] [DecidableEq K] : Fintype ↑(coloredNeighborSet c v)

Equations

• SimpleGraph.EdgeLabelling.coloredNeighborSetFintype = ⋯.mpr (Subtype.fintype fun (w : V) => ∃ (h : G.Adj v w), EC ⟨s(v, w), ⋯⟩ = c)

theorem SimpleGraph.EdgeLabelling.coloredNeighborSet.symm {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {EC : G.EdgeLabelling K} (c : K) (v w : V) : w ∈ coloredNeighborSet c v ↔ v ∈ coloredNeighborSet c w

theorem SimpleGraph.TopEdgeLabelling.monochromaticBetween_neighbors {V : Type u_1} {K : Type u_3} {EC : TopEdgeLabelling V K} {c : K} {y : V} {T : Finset V} (h : ∀ x ∈ T, y ∈ EdgeLabelling.coloredNeighborSet c x) : EdgeLabelling.MonochromaticBetween EC ↑T {y} c

def SimpleGraph.TopEdgeLabelling.MonochromaticBook {V : Type u_1} {K : Type u_3} {EC : TopEdgeLabelling V K} (c : K) (T Y : Finset V) : Prop

EC.monochromatic c T Y if T and Y are disjoint, all edges within T and all edges between T and Yare given color c by EC.

Equations

• SimpleGraph.TopEdgeLabelling.MonochromaticBook c T Y = (Disjoint T Y ∧ SimpleGraph.EdgeLabelling.MonochromaticOf EC (↑T) c ∧ SimpleGraph.EdgeLabelling.MonochromaticBetween EC (↑T) (↑Y) c)

theorem SimpleGraph.TopEdgeLabelling.monochromaticBook_subset {V : Type u_1} {K : Type u_3} {EC : TopEdgeLabelling V K} {i : K} {A B D : Finset V} (b : MonochromaticBook i A B) (s : D ⊆ B) : MonochromaticBook i A D

theorem SimpleGraph.TopEdgeLabelling.monochromaticBook_pullback {V : Type u_1} {V' : Type u_2} {K : Type u_3} {EC : TopEdgeLabelling V K} (f : V' ↪ V) (c : K) (T Y : Finset V') (B : MonochromaticBook c T Y) : MonochromaticBook c (Finset.map f T) (Finset.map f Y)

theorem SimpleGraph.TopEdgeLabelling.monochromaticBook_empty {V : Type u_1} {K : Type u_3} {EC : TopEdgeLabelling V K} {i : K} {A : Finset V} : MonochromaticBook i ∅ A

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

def evenEquivNat : { n : ℕ // Even n } ≃ ℕ

Equations

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

theorem tsum_double_eq_tsum_even {T : Type u_1} [AddCommMonoid T] [TopologicalSpace T] (f : ℕ → T) : ∑' (x : ℕ), f (2 * x) = ∑' (x : ↑{n : ℕ | Even n}), f ↑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_1} {ι : Type u_2} [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)] {β : ℝ} : have 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} : have 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 ^ 3 * ENNReal.ofReal (3 ^ (-(↑r * 4))) * ENNReal.ofReal √3 * ENNReal.ofReal √↑r * 3 ^ r * 3 ≤ 1

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

theorem omg6 {a b : ℝ} (ap : 0 ≤ a) : -a ≤ a * b ↔ -1 ≤ b