OAI/Analysis/Conductivity/Fourier/FourierMatchingInterpolation.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.fourierMatchingCutoff line 11
  2. lemma OAI.ScalarConductivity.fourierMatchingCutoff_smooth line 13
  3. lemma OAI.ScalarConductivity.fourierMatchingCutoff_left line 16
  4. lemma OAI.ScalarConductivity.fourierMatchingCutoff_right line 19
  5. def OAI.ScalarConductivity.fourierMatchingPair line 22
  6. lemma OAI.ScalarConductivity.fourierMatchingPair_smooth line 27
  7. lemma OAI.ScalarConductivity.fourierMatchingPair_periodic line 39
  8. lemma OAI.ScalarConductivity.fourierMatchingPair_base line 51
  9. lemma OAI.ScalarConductivity.fourierMatchingPair_left_nhds line 57
  10. lemma OAI.ScalarConductivity.fourierMatchingPair_right_nhds line 65
  11. def OAI.ScalarConductivity.fourierResidualCutoff line 81
  12. lemma OAI.ScalarConductivity.fourierResidualCutoff_smooth line 82
  13. lemma OAI.ScalarConductivity.fourierResidualCutoff_one line 85
  14. lemma OAI.ScalarConductivity.fourierResidualCutoff_zero_left line 88
  15. lemma OAI.ScalarConductivity.fourierResidualCutoff_zero_right line 90
  16. def OAI.ScalarConductivity.fourierMatchingResidual line 93
  17. lemma OAI.ScalarConductivity.fourierMatchingResidual_smooth line 98
  18. lemma OAI.ScalarConductivity.fourierMatchingResidual_periodic line 108
  19. lemma OAI.ScalarConductivity.fourierMatchingResidual_support line 119
  20. lemma OAI.ScalarConductivity.flatPurePair_source_zero line 130
  21. lemma OAI.ScalarConductivity.fourierMatchingResidual_base line 145