The tau functional for multidistance #
Definition of the tau functional and basic facts
Main definitions: #
Main results #
We will frequently be working with finite additive groups with the discrete sigma-algebra.
- add : G → G → G
- zero : 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_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
- MeasurableSet' : Set G → Prop
- measurableSet_empty : MeasureableFinGroup.toMeasurableSpace.MeasurableSet' ∅
- measurableSet_compl : ∀ (s : Set G), MeasureableFinGroup.toMeasurableSpace.MeasurableSet' s → MeasureableFinGroup.toMeasurableSpace.MeasurableSet' sᶜ
- measurableSet_iUnion : ∀ (f : ℕ → Set G), (∀ (i : ℕ), MeasureableFinGroup.toMeasurableSpace.MeasurableSet' (f i)) → MeasureableFinGroup.toMeasurableSpace.MeasurableSet' (⋃ (i : ℕ), f i)
- measurableSet_singleton : ∀ (x : G), MeasurableSet {x}
Instances
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
- 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
Instances For
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].$$
Instances For
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.59) (hΩ' : (i : Fin p.m) → MeasureTheory.MeasureSpace (Ω' i)) (X' : (i : Fin p.m) → Ω' i → G), multiTau p Ω hΩ X ≤ multiTau p Ω' hΩ' X'
Instances For
If $G$ is finite, then a $\tau$ is continuous.
If $G$ is finite, then a $\tau$-minimizer exists.
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]$.
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].$$
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].$$
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\}$.