The tau functional for multidistance

Definition of the tau functional and basic facts

Main definitions:

Main results

class MeasureableFinGroup (G : Type u_1) extends AddCommGroup , Fintype , MeasurableSpace , MeasurableSingletonClass : Type u_1

We will frequently be working with finite additive groups with the discrete sigma-algebra.

structure multiRefPackage (G : Type u_1) (Ωₒ : Type u_2) [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] : Type (max u_1 u_2)

A structure that packages all the fixed information in the main argument. See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Problem.20when.20instances.20are.20inside.20a.20structure for more discussion of the design choices here.

• m : ℕ
• hm : self.m ≥ 2
• htorsion : ∀ (x : G), self.m • x = 0
• hprob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
• X₀ : Ωₒ → G
• hmeas : Measurable self.X₀
• η : ℝ
• hη : 0 < self.η

theorem multiRefPackage.hm {G : Type u_1} {Ωₒ : Type u_2} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (self : multiRefPackage G Ωₒ) : self.m ≥ 2

theorem multiRefPackage.htorsion {G : Type u_1} {Ωₒ : Type u_2} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (self : multiRefPackage G Ωₒ) (x : G) : self.m • x = 0

theorem multiRefPackage.hprob {G : Type u_1} {Ωₒ : Type u_2} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (self : multiRefPackage G Ωₒ) : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem multiRefPackage.hmeas {G : Type u_1} {Ωₒ : Type u_2} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (self : multiRefPackage G Ωₒ) : Measurable self.X₀

theorem multiRefPackage.hη {G : Type u_1} {Ωₒ : Type u_2} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (self : multiRefPackage G Ωₒ) : 0 < self.η

noncomputable def multiTau {G : Type u_1} {Ωₒ : Type u_2} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u_3) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) : ℝ

If $(X_i){1 \leq i \leq m}$ is a tuple, we define its $\tau$-functional $$ \tau[ (X_i){1 \leq i \leq m}] := D[(X_i){1 \leq i \leq m}] + \eta \sum{i=1}^m d[X_i; X^0].$$

Equations

• multiTau p Ω hΩ X = D[X ; hΩ] + p.η * Finset.univ.sum fun (i : Fin p.m) => d[X i # p.X₀]

def multiTauMinimizes {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) : Prop

A $\tau$-minimizer is a tuple $(X_i)_{1 \leq i \leq m}$ that minimizes the $\tau$-functional among all tuples of $G$-valued random variables.

Equations

• multiTauMinimizes p Ω hΩ X = ∀ (Ω' : Fin p.m → Type u) (hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)) (X' : (i : Fin p.m) → Ω' i → G), multiTau p Ω hΩ X ≤ multiTau p Ω' hΩ' X'

theorem multiTau_continuous {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [TopologicalSpace G] [DiscreteTopology G] [BorelSpace G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) : Continuous fun (μ : Fin p.m → MeasureTheory.ProbabilityMeasure G) => multiTau p (fun (x : Fin p.m) => G) (fun (i : Fin p.m) => MeasureTheory.MeasureSpace.mk ↑(μ i)) fun (x : Fin p.m) => id

If $G$ is finite, then a $\tau$ is continuous.

theorem multiTau_min_exists {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) : ∃ (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G), multiTauMinimizes p Ω hΩ X

If $G$ is finite, then a $\tau$-minimizer exists.

theorem multiTau_min_sum_le {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (hmin : multiTauMinimizes p Ω hΩ X) : (Finset.univ.sum fun (i : Fin p.m) => d[X i # p.X₀]) ≤ 2 * ↑p.m * p.η⁻¹ * d[p.X₀ # p.X₀]

If $(X_i){1 \leq i \leq m}$ is a $\tau$-minimizer, then $\sum{i=1}^m d[X_i; X^0] \leq \frac{2m}{\eta} d[X^0; X^0]$.

theorem sub_multiDistance_le {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (hmin : multiTauMinimizes p Ω hΩ X) (Ω' : Fin p.m → Type u) (hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)) (X' : (i : Fin p.m) → Ω' i → G) : D[X ; hΩ] - D[X' ; hΩ'] ≤ p.η * Finset.univ.sum fun (i : Fin p.m) => d[X i # X' i]

If $(X_i){1 \leq i \leq m}$ is a $\tau$-minimizer, and $k := D[(X_i){1 \leq i \leq m}]$, then for any other tuple $(X'i){1 \leq i \leq m}$, one has $$ k - D[(X'i){1 \leq i \leq m}] \leq \eta \sum_{i=1}^m d[X_i; X'_i].$$

theorem sub_condMultiDistance_le {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (hmin : multiTauMinimizes p Ω hΩ X) (Ω' : Fin p.m → Type u) (hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)) (hf : ∀ (i : Fin p.m), MeasureTheory.IsFiniteMeasure MeasureTheory.volume) (X' : (i : Fin p.m) → Ω' i → G) {S : Type u} [MeasurableSpace S] (Y : (i : Fin p.m) → Ω' i → S) : D[X ; hΩ] - D[X' | Y ; hΩ'] ≤ p.η * Finset.univ.sum fun (i : Fin p.m) => d[X i # X' i | Y i]

If $(X_i){1 \leq i \leq m}$ is a $\tau$-minimizer, and $k := D[(X_i){1 \leq i \leq m}]$, then for any other tuples $(X'i){1 \leq i \leq m}$ and $(Y_i){1 \leq i \leq m}$ with the $X'i$ $G$-valued, one has $$ k - D[(X'i){1 \leq i \leq m} | (Y_i){1 \leq i \leq m}] \leq \eta \sum{i=1}^m d[X_i; X'_i|Y_i].$$

theorem sub_condMultiDistance_le' {G : Type u} {Ωₒ : Type u} [MeasureableFinGroup G] [MeasureTheory.MeasureSpace Ωₒ] (p : multiRefPackage G Ωₒ) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (X : (i : Fin p.m) → Ω i → G) (hmin : multiTauMinimizes p Ω hΩ X) (Ω' : Fin p.m → Type u) (hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)) (hf : ∀ (i : Fin p.m), MeasureTheory.IsFiniteMeasure MeasureTheory.volume) (X' : (i : Fin p.m) → Ω' i → G) {S : Type u} [MeasurableSpace S] (Y : (i : Fin p.m) → Ω' i → S) (φ : Equiv.Perm (Fin p.m)) : D[X ; hΩ] - D[X' | Y ; hΩ'] ≤ p.η * Finset.univ.sum fun (i : Fin p.m) => d[X (φ i) # X' i | Y i]

With the notation of the previous lemma, we have \begin{equation}\label{5.3-conv} k - D[ X'{[m]} | Y{[m]} ] \leq \eta \sum_{i=1}^m d[X_{\sigma(i)};X'_i|Y_i] \end{equation} for any permutation $\sigma : {1,\dots,m} \rightarrow {1,\dots,m}$.