CencovPetz.PermutationInvariantBilinForm

Lemmas about bilinear forms on the finite simplex tangent space that are invariant under permutations (equivalences) of the underlying finite type.

This is a technical step towards the finite Čencov uniqueness theorem.

@[reducible, inline]

abbrev LeanPool.CencovPetz.TangentFin.V (n : ℕ) : Type

The tangent space to the finite simplex on Fin n.

Equations

• LeanPool.CencovPetz.TangentFin.V n = ↥(LeanPool.CencovPetz.tangentSpace (Fin n))

noncomputable def LeanPool.CencovPetz.TangentFin.Basis.e {n : ℕ} (i : Fin n) : Fin n → ℝ

The coordinate basis vector on Fin n.

Equations

• LeanPool.CencovPetz.TangentFin.Basis.e i = Pi.single i 1

theorem LeanPool.CencovPetz.TangentFin.Basis.sum_e {n : ℕ} (i : Fin n) : ∑ k : Fin n, e i k = 1

theorem LeanPool.CencovPetz.TangentFin.Basis.sum_sub_e {n : ℕ} (i j : Fin n) : ∑ k : Fin n, (e i k - e j k) = 0

noncomputable def LeanPool.CencovPetz.TangentFin.Basis.dij {n : ℕ} (i j : Fin n) : V n

The tangent vector e_i - e_j (sum-zero).

Equations

• LeanPool.CencovPetz.TangentFin.Basis.dij i j = ⟨fun (k : Fin n) => LeanPool.CencovPetz.TangentFin.Basis.e i k - LeanPool.CencovPetz.TangentFin.Basis.e j k, ⋯⟩

@[simp]

theorem LeanPool.CencovPetz.TangentFin.Basis.dij_coe {n : ℕ} (i j k : Fin n) : ↑(dij i j) k = e i k - e j k

@[simp]

theorem LeanPool.CencovPetz.TangentFin.Basis.dij_self {n : ℕ} (i : Fin n) : dij i i = 0

theorem LeanPool.CencovPetz.TangentFin.Basis.dij_neg {n : ℕ} (i j : Fin n) : dij i j = -dij j i

theorem LeanPool.CencovPetz.TangentFin.Basis.dij_add {n : ℕ} (i j k : Fin n) : dij i k = dij i j + dij j k

@[reducible, inline]

noncomputable abbrev LeanPool.CencovPetz.TangentFin.Perm.κ {n : ℕ} (σ : Equiv.Perm (Fin n)) : MarkovMorphism (Fin n) (Fin n)

The deterministic Markov morphism induced by a permutation of Fin n.

Equations

• LeanPool.CencovPetz.TangentFin.Perm.κ σ = LeanPool.CencovPetz.MarkovMorphism.deterministic ⇑σ ⋯

theorem LeanPool.CencovPetz.TangentFin.Perm.κ_tangentPushforward_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (u : V n) (k : Fin n) : ↑((κ σ).tangentPushforward u) k = ↑u ((Equiv.symm σ) k)

theorem LeanPool.CencovPetz.TangentFin.Perm.κ_pushforward_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (p : Simplex (Fin n)) (k : Fin n) : ((κ σ).pushforward p).p k = p.p ((Equiv.symm σ) k)

theorem LeanPool.CencovPetz.TangentFin.Perm.e_apply_symm {n : ℕ} (σ : Equiv.Perm (Fin n)) (i k : Fin n) : Basis.e i ((Equiv.symm σ) k) = Basis.e (σ i) k

theorem LeanPool.CencovPetz.TangentFin.Perm.κ_pushforward_uniform {n : ℕ} [Nonempty (Fin n)] (σ : Equiv.Perm (Fin n)) : (κ σ).pushforward Simplex.uniform = Simplex.uniform

theorem LeanPool.CencovPetz.TangentFin.Perm.κ_tangentPushforward_dij {n : ℕ} (σ : Equiv.Perm (Fin n)) (i j : Fin n) : (κ σ).tangentPushforward (Basis.dij i j) = Basis.dij (σ i) (σ j)

theorem LeanPool.CencovPetz.TangentFin.Perm.metric_uniform_invariant {n : ℕ} (G : MonotoneMetricFamily) [Nonempty (Fin n)] (σ : Equiv.Perm (Fin n)) (u v : V n) : ((G.g Simplex.uniform) ((κ σ).tangentPushforward u)) ((κ σ).tangentPushforward v) = ((G.g Simplex.uniform) u) v

@[reducible, inline]

noncomputable abbrev LeanPool.CencovPetz.TangentFin.Bilin.B {n : ℕ} (G : MonotoneMetricFamily) [Nonempty (Fin n)] : LinearMap.BilinForm ℝ (V n)

The bilinear form at the uniform simplex point on Fin n.

Equations

• LeanPool.CencovPetz.TangentFin.Bilin.B G = G.g LeanPool.CencovPetz.Simplex.uniform

theorem LeanPool.CencovPetz.TangentFin.Bilin.B_symm {n : ℕ} (G : MonotoneMetricFamily) [Nonempty (Fin n)] (u v : V n) : ((B G) u) v = ((B G) v) u

theorem LeanPool.CencovPetz.TangentFin.Bilin.B_invariant {n : ℕ} (G : MonotoneMetricFamily) [Nonempty (Fin n)] (σ : Equiv.Perm (Fin n)) (u v : V n) : ((B G) ((Perm.κ σ).tangentPushforward u)) ((Perm.κ σ).tangentPushforward v) = ((B G) u) v

theorem LeanPool.CencovPetz.TangentFin.Bilin.B_dij_dij_eq_of_perm {n : ℕ} (G : MonotoneMetricFamily) [Nonempty (Fin n)] (σ : Equiv.Perm (Fin n)) (i j k l : Fin n) : ((B G) (Basis.dij (σ i) (σ j))) (Basis.dij (σ k) (σ l)) = ((B G) (Basis.dij i j)) (Basis.dij k l)

theorem LeanPool.CencovPetz.TangentFin.Bilin.B_dij_dij_eq_zero_of_disjoint {n : ℕ} (G : MonotoneMetricFamily) [Nonempty (Fin n)] (i j k l : Fin n) (hik : i ≠ k) (hil : i ≠ l) (hjk : j ≠ k) (hjl : j ≠ l) : ((B G) (Basis.dij i j)) (Basis.dij k l) = 0

theorem LeanPool.CencovPetz.TangentFin.Bilin.B_dij_dij_eq_neg_half_self {n : ℕ} (G : MonotoneMetricFamily) [Nonempty (Fin n)] (i j k : Fin n) (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : ((B G) (Basis.dij i j)) (Basis.dij j k) = -(1 / 2) * ((B G) (Basis.dij i j)) (Basis.dij i j)

theorem LeanPool.CencovPetz.TangentFin.Bilin.B_dij_dij_eq_half_self {n : ℕ} (G : MonotoneMetricFamily) [Nonempty (Fin n)] (i j k : Fin n) (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) : ((B G) (Basis.dij i j)) (Basis.dij i k) = 1 / 2 * ((B G) (Basis.dij i j)) (Basis.dij i j)