On this page
Tensor packing: the theorem
Imports 3 library modules and 10 external
- GaussianAnalysis.matrix.euclidean
- GaussianAnalysis.matrix.tensor_packing
- GaussianApplications.TensorPackingStatement
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.algebra.matrix, mathcomp.reals.reals, mathcomp.analysis.sequences, mathcomp.analysis.exp, mathcomp.algebra.arithmetic_tactic, mathcomp.algebra.ring_tactic
Target T2 of phase 12. tensor_packing_theorem proves tensor_packing_statement of TensorPackingStatement.v from the library file matrix/tensor_packing.v, which is a Rocq formalization of the credited argument of Theorem 4.1, 'Tensor packing', of 'Pointwise convergence of fourfold ergodic averages for mixing transformations' (family 154 of the OpenAI math collection, revision 1581d4cbd, sections/04-packing.tex). The collection has no Lean version of it.
The constant is C = 30000: the library theorem tensor_packing has the same hypotheses, and writes the exponent C eps^(-2) sqrt d ln (2 + d) as 30000 sqrt d ln (2 + d) / eps^2.
Main results
| Results | Statement |
|---|---|
Proves tensor_packing_statement (T2) with C = 30000: for every R : realType, rows x_1, ..., x_m and y_1, ..., y_m in the unit balls of 'rV[R]_n1 and 'rV[R]_n2, relations Gx and Gy on 'I_m with at most L successors at every vertex that contain every pair a != b with |<x_a, x_b>| > eta (respectively |<y_a, y_b>| > eta), Frobenius-orthonormal A_1, ..., A_r in 'M[R]_(n1, n2) with r <= d, 0 < eps <= 1, d >= 1 and 0 <= eta <= eps^2 / 10^4, the number of indices a with sum_k (x_a A_k y_a^T)^2 >= eps^2 is at most 30000 (1 + L) / eps^2 exp (30000 eps^(-2) sqrt d ln (2 + d)), from tensor_packing of library/. Axioms: three of boolp. |
Declarations1 exported
Proves tensor_packing_statement (T2) with C = 30000: for every R : realType, rows x_1, ..., x_m and y_1, ..., y_m in the unit balls of 'rV[R]_n1 and 'rV[R]_n2, relations Gx and Gy on 'I_m with at most L successors at every vertex that contain every pair a != b with |<x_a, x_b>| > eta (respectively |<y_a, y_b>| > eta), Frobenius-orthonormal A_1, ..., A_r in 'M[R]_(n1, n2) with r <= d, 0 < eps <= 1, d >= 1 and 0 <= eta <= eps^2 / 10^4, the number of indices a with sum_k (x_a A_k y_a^T)^2 >= eps^2 is at most 30000 (1 + L) / eps^2 exp (30000 eps^(-2) sqrt d ln (2 + d)), from tensor_packing of library/. Axioms: three of boolp.
Statement as written in the source
Theorem tensor_packing_theorem : tensor_packing_statement.