OAI/Analysis/Cotype/TimedShiftScalars.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Cotype.exists_powerGapSectorSlope line 11
  2. theorem OAI.Cotype.complex_exp_negative_half_period line 19
  3. theorem OAI.Cotype.norm_half_period_shift line 50
  4. theorem OAI.Cotype.exp_time_interval_le line 59
  5. theorem OAI.Cotype.timed_shift_imaginary_data line 67
  6. theorem OAI.Cotype.timed_shift_negative_data line 101
  7. theorem OAI.Cotype.exists_sector_timed_shift line 144