OAI/NumberTheory/DirichletL/Dictionary/InverseMarkedPadding.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.radialMajorant line 16
  2. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.radialMajorant_compact line 19
  3. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.radialMajorant_nonneg line 22
  4. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.radialMajorant_one line 25
  5. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.compact_radial_summable line 28
  6. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.radialMajorant_summable line 47
  7. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.finite_source_le_smoothed line 51
  8. def OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.selectedSource line 77
  9. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.selectedSource_norm line 90
  10. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.selectedSource_summable line 102
  11. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.selectedSource_energy line 110
  12. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.fiber_physical_le_padded_smoothed line 123
  13. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.fiber_inverse_le_padded_smoothed line 147
  14. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.fixed_padding_margins line 162
  15. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.fiber_padding_margins line 174
  16. theorem OAI.SevenEighths.DetectorDictionaryInverseMarkedPadding.padded_output_budget line 184