Session Fourier
View
theory dependencies
View
document
View
outline
Theories
Periodic
HOL-Library.Function_Algebras
Ergodic_Theory.SG_Library_Complement
Lp.Functional_Spaces
Lp.Lp
Lspace
Square_Integrable
HOL-Library.BNF_Corec
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML›
HOL-Library.Landau_Symbols
HOL-Real_Asymp.Lazy_Eval
File ‹lazy_eval.ML›
HOL-Real_Asymp.Inst_Existentials
File ‹inst_existentials.ML›
HOL-Real_Asymp.Eventuallize
HOL-Real_Asymp.Multiseries_Expansion
File ‹asymptotic_basis.ML›
File ‹exp_log_expression.ML›
File ‹expansion_interface.ML›
File ‹multiseries_expansion.ML›
File ‹real_asymp.ML›
HOL-Real_Asymp.Multiseries_Expansion_Bounds
File ‹multiseries_expansion_bounds.ML›
HOL-Real_Asymp.Real_Asymp
File ‹real_asymp_diag.ML›
Confine
Fourier_Aux2
Fourier