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 ENNReal.one_sub_one_sub_mul_one_sub {x y : ENNReal} (hx : x ≤ 1) (hy : y ≤ 1) : 1 - (1 - x) * (1 - y) = x + y - x * y

theorem ENNReal.list_prod_natCast_ne_top {ι : Type u_1} (f : ι → ℕ) (js : List ι) : (List.map (fun (j : ι) => ↑(f j)) js).prod ≠ ⊤

theorem ENNReal.toReal_sub_le_abs_toReal_sub (a b : ENNReal) : (a - b).toReal ≤ |a.toReal - b.toReal|

Real bridge for truncated ENNReal subtraction: (a - b).toReal is bounded by |a.toReal - b.toReal|.

@[simp]

theorem List.prod_map_const {α : Type u_1} {M : Type u_2} [CommMonoid M] (xs : List α) (c : M) : (map (fun (x : α) => c) xs).prod = c ^ xs.length

@[simp]

theorem tprod_ite_eq' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => b = x] (a : α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] : (∏'[L] (b' : β), if b = b' then a else 1) = a

@[simp]

theorem tsum_ite_eq' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => b = x] (a : α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] : (∑'[L] (b' : β), if b = b' then a else 0) = a

@[simp]

theorem tprod_ite_eq_apply {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => x = b] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] : (∏'[L] (b' : β), if b' = b then f b' else 1) = f b

@[simp]

theorem tsum_ite_eq_apply {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => x = b] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] : (∑'[L] (b' : β), if b' = b then f b' else 0) = f b

@[simp]

theorem tprod_ite_eq_apply' {α : Type u_1} {β : Type u_2} [CommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => b = x] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] : (∏'[L] (b' : β), if b = b' then f b' else 1) = f b

@[simp]

theorem tsum_ite_eq_apply' {α : Type u_1} {β : Type u_2} [AddCommMonoid α] [TopologicalSpace α] (b : β) [DecidablePred fun (x : β) => b = x] (f : β → α) (L : SummationFilter β := SummationFilter.unconditional β) [L.LeAtTop] : (∑'[L] (b' : β), if b = b' then f b' else 0) = f b

theorem Fin.ofNat_Icc_iff {n m : ℕ} (h : n < m) (x : Fin (m + 1)) : Fin.ofNat (m + 1) n ≤ x ∧ x ≤ Fin.ofNat (m + 1) m ↔ n ≤ ↑x

theorem PMF.apply_eq_one_sub_tsum_ite {α : Type u_1} [DecidableEq α] (p : PMF α) (x : α) : p x = 1 - ∑' (y : α), if y = x then 0 else p y

theorem PMF.ext_forall_ne {α : Type u_1} {p q : PMF α} (x : α) (h : ∀ (y : α), y ≠ x → p y = q y) : p = q

Two PMF that agree on all but one point are actually equal.

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 List.Vector.toList_eq_ofFn_get {α : Type} {n : ℕ} (xs : Vector α n) : xs.toList = List.ofFn xs.get

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

theorem List.countP_finRange_getElem {α : Type} (l : List α) (p : α → Bool) : countP (fun (i : Fin l.length) => p l[i]) (finRange l.length) = countP p l

theorem Fin.card_eq_countP_mem {n : ℕ} (s : Finset (Fin n)) : s.card = Fin.countP fun (x : Fin n) => decide (x ∈ s)

theorem Array.card_eq_countP {α : Type} (as : Array α) (p : α → Prop) [DecidablePred p] : {i : Fin as.size | p as[i]}.card = countP (fun (a : α) => decide (p a)) as

theorem Vector.card_eq_countP {α : Type} {n : ℕ} (xs : Vector α n) (p : α → Prop) [DecidablePred p] : {i : Fin n | p xs[i]}.card = countP (fun (a : α) => decide (p a)) xs

theorem Vector.card_eq_count {α : Type} [DecidableEq α] {n : ℕ} (xs : Vector α n) (x : α) : {i : Fin n | x = xs[i]}.card = count x xs

theorem List.Vector.card_eq_countP {α : Type} {n : ℕ} (xs : Vector α n) (p : α → Prop) [DecidablePred p] : {i : Fin n | p (xs.get i)}.card = countP (fun (a : α) => decide (p a)) xs.toList

theorem List.Vector.card_eq_count {α : Type} [DecidableEq α] {n : ℕ} (xs : Vector α n) (x : α) : {i : Fin n | x = xs.get i}.card = count x xs.toList

@[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 #v[]) (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → motive (tl.insertIdx 0 hd ⋯)) {m : ℕ} (v : Vector α m) : motive v

Equations

• Vector.cases v_empty v_insert = fun (v : Vector α 0) => match v with | Vector.mk { toList := [] } ⋯ => v_empty
• Vector.cases v_empty v_insert = fun (v : Vector α (n + 1)) => match hv : v with | Vector.mk { toList := hd :: tl } hSize => ⋯.mp (v_insert hd (Vector.mk { toList := tl } ⋯))

def Vector.induction {α : Type u_2} {motive : {n : ℕ} → Vector α n → Sort u_1} (v_empty : motive #v[]) (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 #v[] #v[]) (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.
• Vector.cases₂ v_empty v_insert = fun (v : Vector α 0) (v' : Vector β 0) => match v, v' with | Vector.mk { toList := [] } ⋯, Vector.mk { toList := [] } ⋯ => v_empty

def Vector.induction₂ {α : Type u_2} {β : Type u_3} {motive : {n : ℕ} → Vector α n → Vector β n → Sort u_1} (v_empty : motive #v[] #v[]) (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 PMF.uniformOfFintype_map_of_bijective {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Nonempty α] [Nonempty β] (f : α → β) (hf : Function.Bijective f) : map f (uniformOfFintype α) = uniformOfFintype β

@[simp]

theorem PMF.some_map_apply_some {α : Type u_1} (p : PMF α) (x : α) : (map some p) (some x) = p x

This doesn't get applied properly without Classical so add with high priority.

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

def Fin.mOfFn {m : Type u → Type v} [Monad m] {α : Type u} (n : ℕ) : (Fin n → m α) → m (Fin n → α)

Monadic analog of Fin.ofFn: given f : Fin n → m α, runs each computation in order and collects the results as a function Fin n → α. This is the Fin n → α counterpart of Mathlib's Vector.mOfFn.

Equations

• Fin.mOfFn 0 x_2 = pure Fin.elim0
• Fin.mOfFn n.succ f = do let a ← f 0 let rest ← Fin.mOfFn n fun (i : Fin n) => f i.succ pure (Fin.cons a rest)

@[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 []

forIn / foldlM bridge for imperative-style loops

Lean's for/let mut syntax desugars to List.forIn with MProd state and ForInStep.yield continuations, while functional-style code uses List.foldlM with Prod state. The lemmas below bridge these two representations.

For a single mutable variable (no MProd wrapper), use Mathlib's List.forIn_yield_eq_foldlM directly.

theorem List.forIn_mprod_yield_eq_foldlM {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type w} {β γ : Type u} (l : List α) (b₀ : β) (c₀ : γ) (f : α → MProd β γ → m (ForInStep (MProd β γ))) (g : β × γ → α → m (β × γ)) (hfg : ∀ (a : α) (b : β) (c : γ), f a ⟨b, c⟩ = do let r ← g (b, c) a pure (ForInStep.yield ⟨r.1, r.2⟩)) : (do let r ← forIn l ⟨b₀, c₀⟩ f pure (r.fst, r.snd)) = foldlM g (b₀, c₀) l

A for/let mut loop with two mutable variables (desugared to forIn over MProd state with ForInStep.yield in every branch) is equivalent to foldlM with Prod state. This bridges two impedance mismatches at once:

1. forIn with yield-only body ↔ foldlM
2. MProd state from let mut desugaring ↔ Prod state