OAI/Analysis/FiniteFactor/Sampling/Kernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteFactor.samplingCharacter line 12
2. theorem OAI.FiniteFactor.samplingCharacter_norm line 15
3. theorem OAI.FiniteFactor.samplingCharacter_continuous line 18
4. theorem OAI.FiniteFactor.samplingCharacter_zero line 22
5. theorem OAI.FiniteFactor.samplingCharacter_add line 24
6. theorem OAI.FiniteFactor.samplingCharacter_neg line 32
7. theorem OAI.FiniteFactor.samplingCharacter_sub line 39
8. theorem OAI.FiniteFactor.samplingCharacter_integrable line 43
9. theorem OAI.FiniteFactor.samplingCharacter_integral line 47
10. def OAI.FiniteFactor.samplingKernel line 66

    Source documentation

    The finite Fejer kernel, as a nonnegative real function.

    def samplingKernel (H : ℕ) (t : ℝ) : ℝ :=
    …

11. theorem OAI.FiniteFactor.samplingKernel_nonneg line 69
12. theorem OAI.FiniteFactor.samplingKernel_continuous line 73
13. theorem OAI.FiniteFactor.samplingKernel_expansion line 80
14. theorem OAI.FiniteFactor.samplingKernel_integral line 88