OAI/NumberTheory/EgyptianFractions/ThreePrimeContinuousFourier.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.ThreePrimeContinuousFourier.phase line 11

   Source documentation

   Positive-sign integral Fourier phase on the unit interval.

   def phase (n : ℤ) (x : ℝ) : ℂ := fourier n (x : AddCircle (1 : ℝ))

2. lemma OAI.Problem337.ThreePrimeContinuousFourier.phase_exp line 13
3. lemma OAI.Problem337.ThreePrimeContinuousFourier.phase_continuous line 17
4. lemma OAI.Problem337.ThreePrimeContinuousFourier.phase_add line 21
5. lemma OAI.Problem337.ThreePrimeContinuousFourier.phase_zero line 24
6. lemma OAI.Problem337.ThreePrimeContinuousFourier.norm_phase line 26
7. lemma OAI.Problem337.ThreePrimeContinuousFourier.phase_neg line 29
8. lemma OAI.Problem337.ThreePrimeContinuousFourier.phase_sub line 32
9. theorem OAI.Problem337.ThreePrimeContinuousFourier.integral_phase line 37

   Source documentation

   Exact integer-frequency orthogonality, with no limiting argument.

   theorem integral_phase (n : ℤ) :
       (∫ x in (0 : ℝ)..1, phase n x) = if n = 0 then 1 else 0 := by
   …

   Mentions: OAI.Problem337.ThreePrimeContinuousFourier.phase

10. lemma OAI.Problem337.ThreePrimeContinuousFourier.phase_sum line 43
11. theorem OAI.Problem337.ThreePrimeContinuousFourier.weighted_power_integral line 52

    Source documentation

    Exact extraction of every weighted coefficient of a finite Fourier power. The formula also covers the empty indexing type and the zeroth power.

    theorem weighted_power_integral {ι : Type*} [Fintype ι]
        (f : ι → ℤ) (w : ι → ℂ) (k : ℕ) (u : ℤ) :
        (∫ x in (0 : ℝ)..1,
          (∑ a : ι, w a * phase (f a) x) ^ k * phase (-u) x) =
        ∑ v : Fin k → ι, if (∑ i, f (v i)) = u then ∏ i, w (v i) else 0 := by
    …

    Mentions: OAI.Problem337.ThreePrimeContinuousFourier.phase, OAI.Problem337.v

12. def OAI.Problem337.ThreePrimeContinuousFourier.tripleEquiv line 77
13. theorem OAI.Problem337.ThreePrimeContinuousFourier.weighted_triple_integral line 85

    Source documentation

    The continuous cubic identity in nested-sum form. Frequencies need not be injective, and arbitrary complex weights are allowed.

    theorem weighted_triple_integral {ι : Type*} [Fintype ι]
        (f : ι → ℤ) (w : ι → ℂ) (u : ℤ) :
        (∫ x in (0 : ℝ)..1,
          (∑ a : ι, w a * phase (f a) x) ^ 3 * phase (-u) x) =
        ∑ a : ι, ∑ b : ι, ∑ c : ι,
          if f a + f b + f c = u then w a * w b * w c else 0 := by
    …

    Mentions: OAI.Problem337.ThreePrimeContinuousFourier.phase

14. theorem OAI.Problem337.ThreePrimeContinuousFourier.weighted_triple_finset_integral line 103

    Source documentation

    Finite-set version of exact continuous cubic coefficient extraction.

    theorem weighted_triple_finset_integral {ι : Type*} (s : Finset ι)
        (f : ι → ℤ) (w : ι → ℂ) (u : ℤ) :
        (∫ x in (0 : ℝ)..1,
          (∑ a ∈ s, w a * phase (f a) x) ^ 3 * phase (-u) x) =
        ∑ a ∈ s, ∑ b ∈ s, ∑ c ∈ s,
          if f a + f b + f c = u then w a * w b * w c else 0 := by
    …

    Mentions: OAI.Problem337.ThreePrimeContinuousFourier.phase