The tau functional for multidistance

Definition of the tau functional and basic facts

Main definitions:

Main results

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

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

• add : G → G → G
• add_assoc (a b c : G) : a + b + c = a + (b + c)
• zero : G
• zero_add (a : G) : 0 + a = a
• add_zero (a : G) : a + 0 = a
• nsmul : ℕ → G → G
• nsmul_zero (x : G) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : G) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : G → G
• sub : G → G → G
• sub_eq_add_neg (a b : G) : a - b = a + -b
• zsmul : ℤ → G → G
• zsmul_zero' (a : G) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : G) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : G) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : G) : -a + a = 0
• add_comm (a b : G) : a + b = b + a
• elems : Finset G
• complete (x : G) : x ∈ elems
• MeasurableSet' : Set G → Prop
• measurableSet_empty : MeasurableSet' self.toMeasurableSpace ∅
• measurableSet_compl (s : Set G) : MeasurableSet' self.toMeasurableSpace s → MeasurableSet' self.toMeasurableSpace sᶜ
• measurableSet_iUnion (f : ℕ → Set G) : (∀ (i : ℕ), MeasurableSet' self.toMeasurableSpace (f i)) → MeasurableSet' self.toMeasurableSpace (⋃ (i : ℕ), f i)
• measurableSet_singleton (x : G) : MeasurableSet {x}

structure multiRefPackage (G Ω₀ : Type u) [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ω₀] : Type u

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 : ℕ

  The torsion index of the group we are considering.

• hm : self.m ≥ 2
• htorsion (x : G) : self.m • x = 0
• hprob : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
• X₀ : Ω₀ → G

  The random variable

• hmeas : Measurable self.X₀
• η : ℝ

  A small constant. The argument will only work for suitably small η.

• hη : 0 < self.η
• hη' : self.η ≤ 1

noncomputable def multiTau {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) (Ω : Fin p.m → Type u_1) (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.η * ∑ i : Fin p.m, d[X i # p.X₀]

theorem multiTau_of_ident {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) {Ω₁ : Fin p.m → Type u_1} {Ω₂ : Fin p.m → Type u_2} (hΩ₁ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω₁ i)) (hΩ₂ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω₂ i)) {X₁ : (i : Fin p.m) → Ω₁ i → G} {X₂ : (i : Fin p.m) → Ω₂ i → G} (h_ident : ∀ (i : Fin p.m), ProbabilityTheory.IdentDistrib (X₁ i) (X₂ i) MeasureTheory.volume MeasureTheory.volume) : multiTau p Ω₁ hΩ₁ X₁ = multiTau p Ω₂ hΩ₂ X₂

def multiTauMinimizes {G Ω₀ : Type u} [MeasurableFinGroup 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

• One or more equations did not get rendered due to their size.

theorem multiTauMinimizes_of_ident {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) {Ω₁ Ω₂ : Fin p.m → Type u} (hΩ₁ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω₁ i)) (hΩ₂ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω₂ i)) {X₁ : (i : Fin p.m) → Ω₁ i → G} {X₂ : (i : Fin p.m) → Ω₂ i → G} (h_ident : ∀ (i : Fin p.m), ProbabilityTheory.IdentDistrib (X₁ i) (X₂ i) MeasureTheory.volume MeasureTheory.volume) (hmin : multiTauMinimizes p Ω₁ hΩ₁ X₁) : multiTauMinimizes p Ω₂ hΩ₂ X₂

theorem multiTau_continuous {G Ω₀ : Type u} [MeasurableFinGroup 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) => { toMeasurableSpace := inst✝.toMeasurableSpace, volume := ↑(μ i) }) fun (x : Fin p.m) => id

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

theorem multiTau_min_exists_measure {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) : ∃ (μ : Fin p.m → MeasureTheory.Measure G), (∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure (μ i)) ∧ ∀ (ν : Fin p.m → MeasureTheory.Measure G), (∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure (ν i)) → (multiTau p (fun (x : Fin p.m) => G) (fun (i : Fin p.m) => { toMeasurableSpace := inst✝.toMeasurableSpace, volume := μ i }) fun (x : Fin p.m) => id) ≤ multiTau p (fun (x : Fin p.m) => G) (fun (i : Fin p.m) => { toMeasurableSpace := inst✝.toMeasurableSpace, volume := ν i }) fun (x : Fin p.m) => id

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

theorem multiTau_min_exists {G Ω₀ : Type u} [MeasurableFinGroup 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), (∀ (i : Fin p.m), Measurable (X i)) ∧ (∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) ∧ multiTauMinimizes p Ω hΩ X

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

theorem multiTau_min_sum_le {G Ω₀ : Type u} [hG : MeasurableFinGroup G] [hΩ₀ : MeasureTheory.MeasureSpace Ω₀] (p : multiRefPackage G Ω₀) (Ω : Fin p.m → Type u) (hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)) (hprobΩ : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) (X : (i : Fin p.m) → Ω i → G) (hX : ∀ (i : Fin p.m), Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X) : ∑ 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} [MeasurableFinGroup G] [hΩ₀ : MeasureTheory.MeasureSpace Ω₀] {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)} (hΩprob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {X : (i : Fin p.m) → Ω i → G} (hmeasX : ∀ (i : Fin p.m), Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X) {Ω' : Fin p.m → Type u} {hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)} (hΩprob' : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {X' : (i : Fin p.m) → Ω' i → G} (hmeasX' : ∀ (i : Fin p.m), Measurable (X' i)) : D[X ; hΩ] - D[X' ; hΩ'] ≤ p.η * ∑ 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_multiDistance_le' {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ω₀] {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)} (hΩprob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {X : (i : Fin p.m) → Ω i → G} (hmeasX : ∀ (i : Fin p.m), Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X) {Ω' : Fin p.m → Type u} {hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)} (hΩ'prob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {X' : (i : Fin p.m) → Ω' i → G} (hmeasX' : ∀ (i : Fin p.m), Measurable (X' i)) (φ : Equiv.Perm (Fin p.m)) : D[X ; hΩ] - D[X' ; hΩ'] ≤ p.η * ∑ i : Fin p.m, d[X (φ i) # X' i]

theorem sub_condMultiDistance_le {G Ω₀ : Type u} [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ω₀] {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)} (hΩprob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {X : (i : Fin p.m) → Ω i → G} (hmeasX : ∀ (i : Fin p.m), Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X) {Ω' : Fin p.m → Type u} {hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)} (hΩ'prob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {X' : (i : Fin p.m) → Ω' i → G} (hmeasX' : ∀ (i : Fin p.m), Measurable (X' i)) {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] {Y : (i : Fin p.m) → Ω' i → S} (hY : ∀ (i : Fin p.m), Measurable (Y i)) : D[X ; hΩ] - D[X' | Y ; hΩ'] ≤ p.η * ∑ 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} [MeasurableFinGroup G] [MeasureTheory.MeasureSpace Ω₀] {p : multiRefPackage G Ω₀} {Ω : Fin p.m → Type u} {hΩ : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω i)} (hΩprob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {X : (i : Fin p.m) → Ω i → G} (hmeasX : ∀ (i : Fin p.m), Measurable (X i)) (h_min : multiTauMinimizes p Ω hΩ X) {Ω' : Fin p.m → Type u} {hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)} (hΩ'prob : ∀ (i : Fin p.m), MeasureTheory.IsProbabilityMeasure MeasureTheory.volume) {X' : (i : Fin p.m) → Ω' i → G} (hmeasX' : ∀ (i : Fin p.m), Measurable (X' i)) {S : Type u} [Fintype S] [MeasurableSpace S] [MeasurableSingletonClass S] {Y : (i : Fin p.m) → Ω' i → S} (hY : ∀ (i : Fin p.m), Measurable (Y i)) (φ : Equiv.Perm (Fin p.m)) : D[X ; hΩ] - D[X' | Y ; hΩ'] ≤ p.η * ∑ 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\}$.