Research proof index

A uniform distribution on a set with doubling constant K has self Rusza distance at most log K.

If $Z_1, Z_2$ are independent, then $d[Z_1; Z_2]$ is equal to $d[\pi(Z_1);\pi(Z_2)] + d[Z_1|\pi(Z_1); Z_2 |\pi(Z_2)]$ plus $I( Z_1 - Z_2 : (\pi(Z_1), \pi(Z_2)) | \pi(Z_1 - Z_2) ).$

A Ruzsa-distance lower bound for sums of independent copies. Let $X_1',X_2'$ be independent copies of the $\tau$-minimizers $X_1,X_2$, and set $k=d[X_1;X_2]$. Then $d[X_1+X_1';X_2+X_2']\ge k-\frac{\eta}{2}\bigl(d[X_1;X_1]+d[X_2;X_2]\bigr).$

The Marcinkiewicz-Zygmund inequality for real-valued functions, with a slightly easier to bound constant than Real.marcinkiewicz_zygmund'. Note that RCLike.marcinkiewicz_zygmund is another version that works for both ℝ and ℂ at the expense of a slightly worse constant.

The Marcinkiewicz-Zygmund inequality for real-valued functions, with a slightly better constant than Real.marcinkiewicz_zygmund.

The tensor contrMetric is invariant under the action of LorentzGroup d. -/ @[simp] lemma actionT_contrMetric {d} (g : LorentzGroup d) : g • η d = η d := by erw [TensorSpecies.metricTensor_invariant] /- ## There value with respect to a basis