OAI/GroupTheory/SimpleAmenable/RandomFields/AffineGeneratorIntegrability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.affineNoiseGenerator_integrable_square line 16
  2. theorem OAI.SimpleAmenable.affineNoiseRootDerivative_integrable_square line 42
  3. def OAI.SimpleAmenable.noiseInterpolationRoot line 56
  4. def OAI.SimpleAmenable.noiseInterpolationDerivative line 60
  5. theorem OAI.SimpleAmenable.covarianceSegment_hasDerivAt line 65
  6. theorem OAI.SimpleAmenable.noiseInterpolation_hasDerivAt line 72
  7. theorem OAI.SimpleAmenable.noiseInterpolationDerivative_measurable line 89
  8. theorem OAI.SimpleAmenable.noiseInterpolationDerivative_continuousOn line 122
  9. theorem OAI.SimpleAmenable.noiseInterpolationDerivative_energy line 144