OAI/NumberTheory/JointDickman/Counting/PeriodicWindowIntegral.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Unfolding a compact window across the integer period

  1. def OAI.JointDickman.integerLatticeEquiv line 11
  2. theorem OAI.JointDickman.integral_eq_integer_windows line 25
  3. theorem OAI.JointDickman.periodic_window_integral line 39

    Source documentation

    A window crossing either endpoint of a period is recovered exactly by its integer translates; no arc at zero is omitted or counted twice.

    theorem periodic_window_integral {F : ℝ → ℂ} (hF : Continuous F)
    (hp : Function.Periodic F 1) {L U : ℝ} (hLU : L ≤ U) :
    (∫ x in L..U, F x) =
      ∑' k : ℤ, ∫ x in Ioc (0 : ℝ) 1,
        if L < (k : ℝ)+x ∧ (k : ℝ)+x ≤ U then F x else 0 := by
…