OAI/Probability/InvariantIsing/Core/ProductKernelSampling.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Coordinatewise sampling commutes with a finite product of root laws.

  1. lemma OAI.InvariantIsing.product_kernel_comp_general line 13