Lemmas to be Ported to Mathlib

This file gives a centralized location to add lemmas that belong better in general mathlib than in the project itself.

theorem mul_abs_of_nonneg {G : Type u_1} [CommRing G] [LinearOrder G] [IsStrictOrderedRing G] {a b : G} (h : 0 ≤ a) : a * |b| = |a * b|

theorem abs_mul_of_nonneg {G : Type u_1} [CommRing G] [LinearOrder G] [IsStrictOrderedRing G] {a b : G} (h : 0 ≤ b) : |a| * b = |a * b|

theorem mul_abs_of_nonpos {G : Type u_1} [CommRing G] [LinearOrder G] [IsStrictOrderedRing G] {a b : G} (h : a < 0) : a * |b| = -|a * b|

theorem abs_mul_of_nonpos {G : Type u_1} [CommRing G] [LinearOrder G] [IsStrictOrderedRing G] {a b : G} (h : b < 0) : |a| * b = -|a * b|

theorem Fintype.sum_inv_card (α : Type u_1) [Fintype α] [Nonempty α] : ∑ x : α, (↑(card α))⁻¹ = 1

@[simp]

theorem vector_eq_nil {α : Type u_1} (xs : List.Vector α 0) : xs = List.Vector.nil

theorem List.injective2_cons {α : Type u_1} : Function.Injective2 cons

theorem Vector.injective2_cons {α : Type u_1} {n : ℕ} : Function.Injective2 List.Vector.cons

@[simp]

theorem Vector.getElem_eq_get {α : Type u_1} {n : ℕ} (xs : List.Vector α n) (i : ℕ) (h : i < n) : xs[i] = xs.get ⟨i, h⟩

theorem Prod.mk.injective2 {α : Type u_1} {β : Type u_2} : Function.Injective2 mk

theorem Function.injective2_swap_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) : Injective2 (swap f) ↔ Injective2 f

@[simp]

theorem Finset.image_const_univ {α : Type u_1} {β : Type u_2} [DecidableEq β] [Fintype α] [Nonempty α] (b : β) : image (fun (x : α) => b) univ = {b}

theorem List.countP_eq_sum_fin_ite {α : Type u_1} (xs : List α) (p : α → Bool) : (∑ i : Fin xs.length, if p xs[i] = true then 1 else 0) = countP p xs

Summing 1 over list indices that satisfy a predicate is just countP applied to p.

theorem List.card_filter_getElem_eq {α : Type u_1} [DecidableEq α] (xs : List α) (x : α) : {i : Fin xs.length | xs[i] = x}.card = count x xs

@[simp]

theorem Finset.sum_boole' {ι : Type u_1} {β : Type u_2} [AddCommMonoid β] (r : β) (p : ι → Prop) [DecidablePred p] (s : Finset ι) : (∑ x ∈ s, if p x then r else 0) = (filter p s).card • r

@[simp]

theorem Finset.count_toList {α : Type u_1} [DecidableEq α] (x : α) (s : Finset α) : List.count x s.toList = if x ∈ s then 1 else 0

theorem BitVec.toFin_bijective (n : ℕ) : Function.Bijective toFin

instance instFintypeBitVec_toMathlib (n : ℕ) : Fintype (BitVec n)

Equations

• instFintypeBitVec_toMathlib n = Fintype.ofBijective (fun (x : Fin (2 ^ n)) => { toFin := x }) ⋯

@[simp]

theorem card_bitVec (n : ℕ) : Fintype.card (BitVec n) = 2 ^ n

@[simp]

theorem BitVec.xor_self_xor {n : ℕ} (x y : BitVec n) : x ^^^ (x ^^^ y) = y

instance instInhabitedSubtypeForallBijective_toMathlib (α : Type) [Inhabited α] : Inhabited { f : α → α // Function.Bijective f }

Equations

• instInhabitedSubtypeForallBijective_toMathlib α = { default := ⟨id, ⋯⟩ }

@[simp]

theorem Vector.heq_of_toArray_eq_of_size_eq {α : Type u_1} {m n : ℕ} {a : Vector α m} {b : Vector α n} (h : a.toArray = b.toArray) (h' : m = n) : a ≍ b

def Vector.cases {α : Type u_2} {motive : {n : ℕ} → Vector α n → Sort u_1} (v_empty : motive { toArray := #[], size_toArray := ⋯ }) (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → motive (tl.insertIdx 0 hd ⋯)) {m : ℕ} (v : Vector α m) : motive v

Equations

• One or more equations did not get rendered due to their size.
• Vector.cases v_empty v_insert = fun (v : Vector α 0) => match v with | { toArray := { toList := [] }, size_toArray := ⋯ } => v_empty

def Vector.induction {α : Type u_2} {motive : {n : ℕ} → Vector α n → Sort u_1} (v_empty : motive { toArray := #[], size_toArray := ⋯ }) (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → motive tl → motive (tl.insertIdx 0 hd ⋯)) {m : ℕ} (v : Vector α m) : motive v

Equations

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

def Vector.cases₂ {α : Type u_2} {β : Type u_3} {motive : {n : ℕ} → Vector α n → Vector β n → Sort u_1} (v_empty : motive { toArray := #[], size_toArray := ⋯ } { toArray := #[], size_toArray := ⋯ }) (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → (hd' : β) → (tl' : Vector β n) → motive (tl.insertIdx 0 hd ⋯) (tl'.insertIdx 0 hd' ⋯)) {m : ℕ} (v : Vector α m) (v' : Vector β m) : motive v v'

Equations

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

def Vector.induction₂ {α : Type u_2} {β : Type u_3} {motive : {n : ℕ} → Vector α n → Vector β n → Sort u_1} (v_empty : motive { toArray := #[], size_toArray := ⋯ } { toArray := #[], size_toArray := ⋯ }) (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → (hd' : β) → (tl' : Vector β n) → motive tl tl' → motive (tl.insertIdx 0 hd ⋯) (tl'.insertIdx 0 hd' ⋯)) {m : ℕ} (v : Vector α m) (v' : Vector β m) : motive v v'

Equations

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

instance Vector.instAdd_toMathlib {α : Type} {n : ℕ} [Add α] : Add (Vector α n)

Equations

• Vector.instAdd_toMathlib = { add := fun (v1 v2 : Vector α n) => Vector.ofFn (v1.get + v2.get) }

instance Vector.instZero_toMathlib {α : Type} {n : ℕ} [Zero α] : Zero (Vector α n)

Equations

• Vector.instZero_toMathlib = { zero := Vector.ofFn 0 }

@[simp]

theorem Vector.vectorofFn_get {α : Type} {n : ℕ} (v : Fin n → α) : (ofFn v).get = v

@[simp]

theorem Vector.vectorAdd_get {α : Type} {n : ℕ} [Add α] [Zero α] (vx vy : Vector α n) : (vx + vy).get = vx.get + vy.get

theorem tsum_option {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] [ContinuousAdd α] [T2Space α] (f : Option β → α) (hf : Summable (Function.update f none 0)) : ∑' (x : Option β), f x = f none + ∑' (x : β), f (some x)

@[simp]

theorem PMF.monad_pure_eq_pure {α : Type u} (x : α) : Pure.pure x = pure x

@[simp]

theorem PMF.monad_bind_eq_bind {α β : Type u} (p : PMF α) (q : α → PMF β) : p >>= q = p.bind q

theorem PMF.bind_eq_zero {α β : Type u_1} {p : PMF α} {f : α → PMF β} {b : β} : (p >>= f) b = 0 ↔ ∀ (a : α), p a = 0 ∨ (f a) b = 0

theorem PMF.heq_iff {α β : Type u} {pa : PMF α} {pb : PMF β} (h : α = β) : pa ≍ pb ↔ ∀ (x : α), pa x = pb (cast h x)

theorem Option.cast_eq_some_iff {α β : Type u} {x : Option α} {b : β} (h : α = β) : cast ⋯ x = some b ↔ x = some (cast ⋯ b)

theorem PMF.uniformOfFintype_cast (α β : Type u_1) [ha : Fintype α] [Nonempty α] [hb : Fintype β] [Nonempty β] (h : α = β) : cast ⋯ (uniformOfFintype α) = uniformOfFintype β

theorem tsum_cast {α β : Type u} {f : α → ENNReal} {g : β → ENNReal} (h : α = β) (h' : ∀ (a : α), f a = g (cast h a)) : ∑' (a : α), f a = ∑' (b : β), g b

@[simp]

theorem List.foldlM_range {m : Type u → Type v} [Monad m] [LawfulMonad m] {s : Type u} (n : ℕ) (f : s → Fin n → m s) (init : s) : foldlM f init (finRange n) = Fin.foldlM n f init

theorem list_mapM_loop_eq {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type w} {β : Type u} (xs : List α) (f : α → m β) (ys : List β) : List.mapM.loop f xs ys = (fun (x : List β) => ys.reverse ++ x) <$> List.mapM.loop f xs []