OAI/Probability/InvariantIsing/Haar/HaarDifferentiableCurve.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite-coordinate differentiable curves and their polynomial oscillation bounds.

  1. structure OAI.InvariantIsing.HaarDifferentiableCurve line 11
  2. lemma OAI.InvariantIsing.HaarDifferentiableCurve.continuous_entry line 20
  3. def OAI.InvariantIsing.HaarDifferentiableCurve.constant line 24
  4. def OAI.InvariantIsing.HaarDifferentiableCurve.mul line 30
  5. lemma OAI.InvariantIsing.HaarDifferentiableCurve.polynomial_bound line 49