OAI/Probability/InvariantIsing/Haar/HaarContinuousDerivative.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact domination for continuous derivatives along actual Haar rotations.

  1. lemma OAI.InvariantIsing.continuous_haar_integrable line 10
  2. lemma OAI.InvariantIsing.integral_haar_continuous_derivative line 16