OAI/NumberTheory/Ostmann/Arithmetic/BulkCoordinateInsertion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Freeze the nonbulk coordinates and integrate the selected bulk slots

  1. def OAI.Ostmann.bulkCoordinateInsert line 11
  2. theorem OAI.Ostmann.bulkCoordinateInsert_at line 15
  3. theorem OAI.Ostmann.bulkCoordinateInsert_update line 23
  4. def OAI.Ostmann.BulkIntegrand.pullBulk line 40
  5. theorem OAI.Ostmann.BulkIntegrand.pullBulk_average line 53
  6. theorem OAI.Ostmann.BulkIntegrand.pullBulk_averages line 62
  7. theorem OAI.Ostmann.BulkIntegrand.selected_bulk_integral line 71