OAI/NumberTheory/Ostmann/Arithmetic/MovingKernelTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Measure transport for the concrete bounded moving kernel

  1. theorem OAI.Ostmann.measurable_exp_pair_mul line 11
  2. theorem OAI.Ostmann.moving_kernel_pair_transport line 19
  3. theorem OAI.Ostmann.moving_kernel_mixed_transport line 49