OAI/Probability/InvariantIsing/Haar/HaarDirectionBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Directional control by coordinate-plane derivatives.

  1. lemma OAI.InvariantIsing.plane_functional_abs_bound line 11
  2. lemma OAI.InvariantIsing.matrixPolynomial_direction_bound line 36