OAI/NumberTheory/Ostmann/Arithmetic/BulkLogWeightedIntegrand.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded measurable bulk integrands retaining the initial cutoffs

  1. theorem OAI.Ostmann.continuous_bulkLogCutoffWeight line 12
  2. def OAI.Ostmann.BulkIntegrand.withLogCutoffs line 28