Auxiliary utilities

This file contains small helper lemmas. These are all generic -- they are not specific to this repository's main objects, so they are collected separately here.

@[reducible, inline]

noncomputable abbrev LeanPool.DemazureProduct.Utils.oneIf (P : Prop) : ℤ

The integer-valued indicator of a proposition: 1 when P holds and 0 otherwise. This is the notation $\delta(P)$ in An extended Demazure product.

Equations

• LeanPool.DemazureProduct.Utils.oneIf P = if P then 1 else 0

theorem LeanPool.DemazureProduct.Utils.oneIf_congr {P Q : Prop} (h : P ↔ Q) : oneIf P = oneIf Q

The indicator $\delta(P)$ depends only on the truth value of $P$.

theorem LeanPool.DemazureProduct.Utils.oneIf_Ico_eq_sub (m n : ℤ) (m_le_n : m ≤ n) (k : ℤ) : oneIf (k ∈ Finset.Ico m n) = oneIf (k < n) - oneIf (k < m)

On an integer interval, membership is the difference of two initial segments.

theorem LeanPool.DemazureProduct.Utils.sum_oneIf_mem_of_subset {ι : Type u_1} {A U : Finset ι} (hAU : A ⊆ U) : ∑ k ∈ U, oneIf (k ∈ A) = ↑A.card

Summing the indicator of membership in A over any finite superset U counts A.

theorem LeanPool.DemazureProduct.Utils.sub_card_eq_sub_card_diff (S T : Finset ℤ) : ↑S.card - ↑T.card = ↑(S \ T).card - ↑(T \ S).card

The difference of the cardinalities of two finite sets is equal to the difference of the cardinalities of their set-theoretic differences.

theorem LeanPool.DemazureProduct.Utils.card_filter_helper (S : Finset ℤ) (f : ℤ → ℤ) (c : ℤ) : {x ∈ S | f x ≥ c}.card + {x ∈ S | f x < c}.card = S.card

theorem LeanPool.DemazureProduct.Utils.min_helper {m n : ℤ} (m_pos : m ≥ 1) (n_pos : n ≥ 1) {S : Set (ℤ × ℤ)} (mem : (m, n) ∈ S) (nmem : (1, 1) ∉ S) : ∃ (m' : ℤ) (n' : ℤ), m' ≥ 1 ∧ n' ≥ 1 ∧ (m', n') ∈ S ∧ ((m' - 1, n') ∉ S ∧ m' ≥ 2 ∨ (m', n' - 1) ∉ S ∧ n' ≥ 2)