OAI/Analysis/Triangular/Schwartz/SpectralCLM.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.AtomicTriangular.Construction.Spectrum line 9
  2. def OAI.AtomicTriangular.Construction.coeffAbs line 11
  3. lemma OAI.AtomicTriangular.Construction.fourierCoeff_norm line 12
  4. def OAI.AtomicTriangular.Construction.pVariation line 13
  5. def OAI.AtomicTriangular.Construction.dVariation line 14
  6. def OAI.AtomicTriangular.Construction.cVariation line 15
  7. lemma OAI.AtomicTriangular.Construction.coeffAbs_nonneg line 16
  8. def OAI.AtomicTriangular.Construction.extend line 18
  9. lemma OAI.AtomicTriangular.Construction.continuous_extend line 19
  10. lemma OAI.AtomicTriangular.Construction.norm_extend_le line 21
  11. lemma OAI.AtomicTriangular.Construction.frequency_mem line 24
  12. def OAI.AtomicTriangular.Construction.spectralC line 29
  13. def OAI.AtomicTriangular.Construction.spectralD line 34
  14. def OAI.AtomicTriangular.Construction.spectralP line 39
  15. lemma OAI.AtomicTriangular.Construction.norm_exp_phase line 42
  16. lemma OAI.AtomicTriangular.Construction.norm_exp_neg_phase line 46
  17. lemma OAI.AtomicTriangular.Construction.norm_first_integral_le line 50
  18. lemma OAI.AtomicTriangular.Construction.norm_second_integral_le line 55
  19. lemma OAI.AtomicTriangular.Construction.spectralP_bound line 91
  20. lemma OAI.AtomicTriangular.Construction.spectralD_bound line 102
  21. lemma OAI.AtomicTriangular.Construction.spectralC_bound line 126
  22. def OAI.AtomicTriangular.Construction.integralLinear line 150
  23. def OAI.AtomicTriangular.Construction.spectralCLinear line 162
  24. def OAI.AtomicTriangular.Construction.spectralDLinear line 167
  25. lemma OAI.AtomicTriangular.Construction.spectralCLinear_apply line 172
  26. lemma OAI.AtomicTriangular.Construction.spectralDLinear_apply line 175
  27. def OAI.AtomicTriangular.Construction.spectralCCLM line 179
  28. def OAI.AtomicTriangular.Construction.spectralDCLM line 182
  29. def OAI.AtomicTriangular.Construction.spectralPCLM line 185
  30. lemma OAI.AtomicTriangular.Construction.spectralCCLM_apply line 188
  31. lemma OAI.AtomicTriangular.Construction.spectralDCLM_apply line 190
  32. lemma OAI.AtomicTriangular.Construction.spectralPCLM_apply line 192
  33. lemma OAI.AtomicTriangular.Construction.spectralCCLM_norm line 195
  34. lemma OAI.AtomicTriangular.Construction.spectralDCLM_norm line 197
  35. lemma OAI.AtomicTriangular.Construction.spectralPCLM_norm line 199
  36. def OAI.AtomicTriangular.Construction.phaseFunction line 205
  37. lemma OAI.AtomicTriangular.Construction.extend_on line 208
  38. lemma OAI.AtomicTriangular.Construction.interval_frequency_subset line 212
  39. lemma OAI.AtomicTriangular.Construction.spectralD_phase line 217
  40. lemma OAI.AtomicTriangular.Construction.spectralC_phase line 232
  41. lemma OAI.AtomicTriangular.Construction.spectralP_phase line 247
  42. lemma OAI.AtomicTriangular.Construction.exponential_apply line 250
  43. def OAI.AtomicTriangular.Construction.frequencyFunction line 256
  44. lemma OAI.AtomicTriangular.Construction.phaseFunction_exp line 258
  45. lemma OAI.AtomicTriangular.Construction.differentiable_phaseFunction line 265