OAI/Geometry/TamingCompatibility/Functional/FourierCutoff.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TamingCompatibility.CompactKernel.evaluate line 14
  2. lemma OAI.TamingCompatibility.CompactKernel.evaluate_apply line 20
  3. lemma OAI.TamingCompatibility.CompactKernel.norm_evaluate_le line 23
  4. def OAI.TamingCompatibility.CompactKernel.operator line 31
  5. lemma OAI.TamingCompatibility.CompactKernel.operator_apply line 38
  6. theorem OAI.TamingCompatibility.CompactKernel.compact_operator line 41
  7. lemma OAI.TamingCompatibility.FourierCutoff.fourierChar_sub_bound line 79
  8. lemma OAI.TamingCompatibility.FourierCutoff.phase_sub_bound line 96
  9. def OAI.TamingCompatibility.FourierCutoff.phase line 107
  10. lemma OAI.TamingCompatibility.FourierCutoff.phase_norm_le line 113
  11. def OAI.TamingCompatibility.FourierCutoff.modulate line 119
  12. lemma OAI.TamingCompatibility.FourierCutoff.modulate_coe line 122
  13. lemma OAI.TamingCompatibility.FourierCutoff.modulate_norm_le line 130
  14. lemma OAI.TamingCompatibility.FourierCutoff.modulate_sub_norm_le line 136
  15. lemma OAI.TamingCompatibility.FourierCutoff.continuous_modulate line 151
  16. def OAI.TamingCompatibility.FourierCutoff.multiply line 163
  17. def OAI.TamingCompatibility.FourierCutoff.pairing line 171
  18. lemma OAI.TamingCompatibility.FourierCutoff.pairing_norm_le line 174
  19. def OAI.TamingCompatibility.FourierCutoff.pairingCLM line 180