OAI/Probability/InvariantIsing/Arrays/QuantileProductKernel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Quantile form of the ultrametric product kernel, including plateaus.

  1. lemma OAI.InvariantIsing.quantile_product_kernel_eq line 14
  2. lemma OAI.InvariantIsing.intervalIntegrable_of_measurable_abs_le line 32
  3. theorem OAI.InvariantIsing.integral_quantile_product_kernel line 40