Finite weights over a commutative semiring

Finite sums, coordinate products, pushforwards, and independence of disjoint coordinate blocks share the same algebra for real and complex weights. These lemmas require neither positivity nor additive inverses. The original real and complex APIs specialize this common toolkit while retaining their existing weight definitions.

def TriangleInflation.FiniteWeights.pushforward {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [Fintype α] [DecidableEq β] (w : α → R) (F : α → β) : β → R

Pushforward sums a finite weight over each fibre of a map.

Equations

• TriangleInflation.FiniteWeights.pushforward w F b = ∑ a : α, if F a = b then w a else 0

def TriangleInflation.FiniteWeights.prodLaw {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] (w : ι → Bool → R) : (ι → Bool) → R

The product of the weights of a Boolean coordinate configuration.

Equations

• TriangleInflation.FiniteWeights.prodLaw w x = ∏ i : ι, w i (x i)

theorem TriangleInflation.FiniteWeights.sum_pi_prod {R : Type u_1} [CommSemiring R] {κ : Type u_2} [Fintype κ] [DecidableEq κ] {A : κ → Type u_3} [(k : κ) → Fintype (A k)] (f : (k : κ) → A k → R) : ∑ x : (k : κ) → A k, ∏ k : κ, f k (x k) = ∏ k : κ, ∑ a : A k, f k a

A sum over all configurations of a dependent product factorizes.

theorem TriangleInflation.FiniteWeights.ite_funext_prod {R : Type u_1} [CommSemiring R] {κ : Type u_2} [Fintype κ] {B : κ → Type u_3} [(k : κ) → DecidableEq (B k)] (f g : (k : κ) → B k) : (if f = g then 1 else 0) = ∏ k : κ, if f k = g k then 1 else 0

The indicator of an equality of configurations is a product of coordinate indicators.

theorem TriangleInflation.FiniteWeights.sum_dprod_sel {R : Type u_1} [CommSemiring R] {κ : Type u_2} [Fintype κ] [DecidableEq κ] {A : κ → Type u_3} {B : κ → Type u_4} [(k : κ) → Fintype (A k)] [(k : κ) → DecidableEq (B k)] (W : (k : κ) → A k → R) (sel : (k : κ) → A k → B k) (y : (k : κ) → B k) : ∑ x : (k : κ) → A k, (if (fun (k : κ) => sel k (x k)) = y then 1 else 0) * ∏ k : κ, W k (x k) = ∏ k : κ, ∑ a : A k, (if sel k a = y k then 1 else 0) * W k a

A dependent product weight pushed forward along a coordinatewise map.

theorem TriangleInflation.FiniteWeights.sum_sel_coord {R : Type u_1} [CommSemiring R] {B : Type u_2} [Fintype B] [DecidableEq B] {n : Type u_3} [Fintype n] [DecidableEq n] (ρ : B → R) (hρ : ∑ b : B, ρ b = 1) (r₀ : n) (b₀ : B) : ∑ v : n → B, (if v r₀ = b₀ then 1 else 0) * ∏ r : n, ρ (v r) = ρ b₀

A normalized independent family has its original weight at each selected coordinate.

theorem TriangleInflation.FiniteWeights.sum_mul_comp {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] [DecidableEq β] (w : α → R) (F : α → β) (G : β → R) : ∑ a : α, w a * G (F a) = ∑ b : β, pushforward w F b * G b

Integrating against a pushforward is integrating the pullback.

theorem TriangleInflation.FiniteWeights.pushforward_comp_equiv {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [DecidableEq β] [DecidableEq γ] (w : α → R) (F : α → β) (E : β ≃ γ) : (pushforward w fun (a : α) => E (F a)) = fun (c : γ) => pushforward w F (E.symm c)

Postcomposing the read map with a bijection transports the pushforward.

theorem TriangleInflation.FiniteWeights.pushforward_mix {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} [Fintype α] [DecidableEq β] {ι : Type u_5} [Fintype ι] (c : ι → R) (ν : ι → α → R) (F : α → β) : pushforward (fun (a : α) => ∑ i : ι, c i * ν i a) F = fun (b : β) => ∑ i : ι, c i * pushforward (ν i) F b

Pushing forward a finite mixture.

Marginals of a product law along an injective selection

theorem TriangleInflation.FiniteWeights.pushforward_prodLaw_sel {R : Type u_1} [CommSemiring R] {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] {w : ι → Bool → R} (hw : ∀ (i : ι), ∑ b : Bool, w i b = 1) {ν : κ → ι} (hν : Function.Injective ν) : (pushforward (prodLaw w) fun (x : ι → Bool) (k : κ) => x (ν k)) = prodLaw fun (k : κ) => w (ν k)

The marginal of a product weight on an injectively selected set of coordinates is the product weight of the selected coordinates.

Independence of functions of disjoint coordinate blocks, dependent fibres

def TriangleInflation.FiniteWeights.dprod {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] {A : ι → Type u_3} (w : (i : ι) → A i → R) (x : (i : ι) → A i) : R

The product weight of independent coordinates with dependent alphabets.

Equations

• TriangleInflation.FiniteWeights.dprod w x = ∏ i : ι, w i (x i)

theorem TriangleInflation.FiniteWeights.sum_dprod {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : ι → Type u_3} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → R} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) : ∑ x : (i : ι) → A i, dprod w x = 1

A product of normalized coordinate weights has total mass one.

def TriangleInflation.FiniteWeights.dmix {ι : Type u_2} [DecidableEq ι] {A : ι → Type u_3} (I : Finset ι) (x y : (i : ι) → A i) (i : ι) : A i

dmix I x y takes its I-coordinates from x and the others from y.

Equations

• TriangleInflation.FiniteWeights.dmix I x y i = if i ∈ I then x i else y i

theorem TriangleInflation.FiniteWeights.dmix_mem {ι : Type u_2} [DecidableEq ι] {A : ι → Type u_3} {I : Finset ι} {x y : (i : ι) → A i} {i : ι} (hi : i ∈ I) : dmix I x y i = x i

Mixing retains the first configuration on a selected coordinate.

theorem TriangleInflation.FiniteWeights.dmix_not_mem {ι : Type u_2} [DecidableEq ι] {A : ι → Type u_3} {I : Finset ι} {x y : (i : ι) → A i} {i : ι} (hi : i ∉ I) : dmix I x y i = y i

Mixing retains the second configuration outside the selected coordinates.

theorem TriangleInflation.FiniteWeights.dprod_dmix_mul {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : ι → Type u_3} {w : (i : ι) → A i → R} (I : Finset ι) (x y : (i : ι) → A i) : dprod w (dmix I x y) * dprod w (dmix I y x) = dprod w x * dprod w y

Swapping selected coordinates between two configurations preserves their combined weight.

theorem TriangleInflation.FiniteWeights.sum_dprod_mul_mul {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : ι → Type u_3} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → R} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) {I J : Finset ι} (hIJ : Disjoint I J) {φ ψ : ((i : ι) → A i) → R} (hφ : ∀ (x y : (i : ι) → A i), (∀ i ∈ I, x i = y i) → φ x = φ y) (hψ : ∀ (x y : (i : ι) → A i), (∀ i ∈ J, x i = y i) → ψ x = ψ y) : ∑ x : (i : ι) → A i, dprod w x * (φ x * ψ x) = (∑ x : (i : ι) → A i, dprod w x * φ x) * ∑ x : (i : ι) → A i, dprod w x * ψ x

Functions of disjoint coordinate blocks are uncorrelated under a product weight.

theorem TriangleInflation.FiniteWeights.sum_dprod_prod {R : Type u_1} [CommSemiring R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {A : ι → Type u_3} [(i : ι) → Fintype (A i)] {w : (i : ι) → A i → R} (hw : ∀ (i : ι), ∑ a : A i, w i a = 1) {n : ℕ} (I : Fin n → Finset ι) (χ : Fin n → ((i : ι) → A i) → R) : (∀ (m m' : Fin n), m ≠ m' → Disjoint (I m) (I m')) → (∀ (m : Fin n) (x y : (i : ι) → A i), (∀ i ∈ I m, x i = y i) → χ m x = χ m y) → ∑ x : (i : ι) → A i, dprod w x * ∏ m : Fin n, χ m x = ∏ m : Fin n, ∑ x : (i : ι) → A i, dprod w x * χ m x

Functions of pairwise disjoint coordinate blocks have a product expectation.

theorem TriangleInflation.FiniteWeights.pushforward_comp {R : Type u_1} [CommSemiring R] {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Fintype α] [Fintype β] [DecidableEq β] [DecidableEq γ] (w : α → R) (F : α → β) (G : β → γ) : pushforward (pushforward w F) G = pushforward w fun (a : α) => G (F a)

Successive pushforwards equal the pushforward along the composite map.