OAI/Analysis/FiniteFactor/Sampling/Smoothing.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.FiniteFactor.samplingCharacter_sub_argument line 10
2. theorem OAI.FiniteFactor.samplingCharacter_fract line 18
3. theorem OAI.FiniteFactor.samplingKernel_fract line 22
4. theorem OAI.FiniteFactor.samplingKernel_shift_integral line 26
5. def OAI.FiniteFactor.samplingSmooth line 38
6. def OAI.FiniteFactor.samplingIntervalCoefficient line 41
7. theorem OAI.FiniteFactor.samplingSmooth_bounds line 44
8. theorem OAI.FiniteFactor.samplingIntervalCoefficient_zero line 57
9. theorem OAI.FiniteFactor.samplingIntervalCoefficient_norm line 61
10. theorem OAI.FiniteFactor.samplingSmooth_expansion line 74

    Source documentation

    An actual finite Fourier expansion of the smoothed interval indicator. Keeping the two kernel indices avoids assuming a coefficient formula.

    theorem samplingSmooth_expansion (H : ℕ) (E : Set ℝ) (t : ℝ) :
        (samplingSmooth H E t : ℂ) = (H : ℂ)⁻¹ *
          ∑ r ∈ Finset.range H, ∑ q ∈ Finset.range H,
            samplingCharacter ((r : ℤ)-(q : ℤ)) t *
              samplingIntervalCoefficient E ((r : ℤ)-(q : ℤ)) := by
    …

    Mentions: OAI.FiniteFactor.samplingSmooth, OAI.FiniteFactor.samplingCharacter, OAI.FiniteFactor.samplingIntervalCoefficient

11. theorem OAI.FiniteFactor.samplingSmooth_continuous line 87