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.list_prod_natCast_ne_top {ι : Type u_1} (f : ι → ℕ) (js : List ι) : (List.map (fun (j : ι) => ↑(f j)) js).prod ≠ ⊤

theorem sum_update_succ_count {ι : Type} [Fintype ι] [DecidableEq ι] (counts : ι → ℕ) (i : ι) : ∑ j : ι, Function.update counts i (counts i + 1) j = ∑ j : ι, counts j + 1

Updating one coordinate by +1 increases the total sum by exactly one.

theorem sum_update_pred {ι : Type u_1} [Fintype ι] [DecidableEq ι] {qc : ι → ℕ} {t : ι} (ht : 0 < qc t) : ∑ i : ι, Function.update qc t (qc t - 1) i = ∑ i : ι, qc i - 1

Updating one coordinate of a ℕ-valued function by -1 at a positive-valued coordinate decreases the total sum by exactly one.

theorem sum_filter_update_of_pred_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → Prop} [DecidablePred p] {qc : ι → ℕ} {t : ι} (hpt : p t) (hqt : 0 < qc t) : ∑ i : ι with p i, Function.update qc t (qc t - 1) i = ∑ i : ι with p i, qc i - 1

Filtered sum after updating a ℕ-valued function by -1 at a positive-valued coordinate inside the filter.

theorem sum_filter_update_of_not_pred {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ι → Prop} [DecidablePred p] {qc : ι → ℕ} {t : ι} (hpt : ¬p t) : ∑ i : ι with p i, Function.update qc t (qc t - 1) i = ∑ i : ι with p i, qc i

Updating a ℕ-valued function at an index outside the filter leaves the filtered sum unchanged.

theorem Prod.fst_comp_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} (f : α → γ) (g : β → δ) : fst ∘ map f g = f ∘ fst

theorem Prod.snd_comp_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} (f : α → γ) (g : β → δ) : snd ∘ map f g = g ∘ snd

@[simp]

theorem fst_map_prod_map {m : Type u → Type v} [Functor m] [LawfulFunctor m] {α β γ δ : Type u} (mx : m (α × β)) (f : α → γ) (g : β → δ) : Prod.fst <$> Prod.map f g <$> mx = (f ∘ Prod.fst) <$> mx

@[simp]

theorem snd_map_prod_map {m : Type u → Type v} [Functor m] [LawfulFunctor m] {α β γ δ : Type u} (mx : m (α × β)) (f : α → γ) (g : β → δ) : Prod.snd <$> Prod.map f g <$> mx = (g ∘ Prod.snd) <$> mx

theorem snd_map_prod_map_eq_map {m : Type u → Type v} [Functor m] [LawfulFunctor m] {α β γ δ : Type u} (mx : m (α × β)) (f : α → γ) (g : β → δ) : Prod.snd <$> Prod.map f g <$> mx = g <$> Prod.snd <$> mx

Split form: the second projection after Prod.map equals the mapped projection.

theorem fst_map_prod_map_eq_map {m : Type u → Type v} [Functor m] [LawfulFunctor m] {α β γ δ : Type u} (mx : m (α × β)) (f : α → γ) (g : β → δ) : Prod.fst <$> Prod.map f g <$> mx = f <$> Prod.fst <$> mx

Split form: the first projection after Prod.map equals the mapped projection.

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

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

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

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'

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'

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

theorem bind_eq_of_map_eq {m : Type → Type u_1} [Monad m] [LawfulMonad m] {α₁ α₂ β : Type} {m₁ : m α₁} {m₂ : m α₂} {f₁ : α₁ → m β} {f₂ : α₂ → m β} (proj : α₁ → α₂) (h_first : proj <$> m₁ = m₂) (h_cont : ∀ (a₁ : α₁), f₁ a₁ = f₂ (proj a₁)) : m₁ >>= f₁ = m₂ >>= f₂

If the first steps agree after projection, and continuations agree on matching inputs, then the full bind computations agree. Generalizes bind_congr to different source types.