OAI/NumberTheory/EgyptianFractions/FejerSampleMean.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.FejerSampleMean.norm_sum_character_translate line 11

   Source documentation

   Translating the samples rotates every Fourier coefficient without changing its norm.

   theorem norm_sum_character_translate {q : ℕ} [NeZero q] {I : Type*}
       [Fintype I] (x : I → ZMod q) (a y : ZMod q) :
       ‖∑ t : I, ZMod.stdAddChar (a * (x t - y))‖ =
         ‖∑ t : I, ZMod.stdAddChar (a * x t)‖ := by
   …

2. theorem OAI.Problem337.FejerSampleMean.norm_sum_character_neg line 20

   Source documentation

   Negating a frequency conjugates its coefficient.

   theorem norm_sum_character_neg {q : ℕ} [NeZero q] {I : Type*}
       [Fintype I] (x : I → ZMod q) (a : ZMod q) :
       ‖∑ t : I, ZMod.stdAddChar ((-a) * x t)‖ =
         ‖∑ t : I, ZMod.stdAddChar (a * x t)‖ := by
   …

3. theorem OAI.Problem337.FejerSampleMean.packet_correlation_bound line 30

   Source documentation

   Off-diagonal correlations of the geometric packet are controlled by the positive low frequencies, with no unmentioned negative-frequency assumption.

   theorem packet_correlation_bound {q h : ℕ} [NeZero q] {I : Type*}
       [Fintype I] (x : I → ZMod q) (y : ZMod q) (E : ℝ)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l < h →
         ‖∑ t : I, ZMod.stdAddChar ((l : ZMod q) * x t)‖ ≤ E)
       (j k : Fin h) (hjk : j ≠ k) :
       ‖∑ t : I, ZMod.stdAddChar ((j.val : ZMod q) * (x t - y)) *
         (starRingEnd ℂ) (ZMod.stdAddChar ((k.val : ZMod q) * (x t - y)))‖ ≤ E := by
   …

4. theorem OAI.Problem337.FejerSampleMean.second_moment_lower line 60

   Source documentation

   Lower counterpart of the finite second-moment bound, using the same honest off-diagonal correlation hypotheses.

   theorem second_moment_lower {α β : Type*}
       (U : Finset α) (T : Finset β) (z : α → β → ℂ) (E : ℝ)
       (hunit : ∀ u ∈ U, ∀ t ∈ T, ‖z u t‖ = 1)
       (hcorr : ∀ t ∈ T, ∀ s ∈ T, t ≠ s →
         ‖∑ u ∈ U, z u t * (starRingEnd ℂ) (z u s)‖ ≤ E) :
       (U.card : ℝ) * T.card - (T.card : ℝ) * (T.card - 1 : ℝ) * E ≤
         ∑ u ∈ U, ‖∑ t ∈ T, z u t‖ ^ 2 := by
   …

5. theorem OAI.Problem337.FejerSampleMean.raw_packet_mean_lower line 103

   Source documentation

   The lower sampled mean of the geometric packet, before identifying the packet with the named kernel.

   theorem raw_packet_mean_lower {q h : ℕ} [NeZero q] {I : Type*}
       [Fintype I] [Nonempty I] (hh : 0 < h)
       (x : I → ZMod q) (y : ZMod q) (ε : ℝ)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l < h →
         ‖∑ t : I, ZMod.stdAddChar ((l : ZMod q) * x t)‖ ≤
           (Fintype.card I : ℝ) * ε) :
       1 - ((h : ℝ) - 1) * ε ≤
         (∑ t : I, ‖∑ j : Fin h,
           ZMod.stdAddChar ((j.val : ZMod q) * (x t - y))‖ ^ 2 / (h : ℝ)) /
           (Fintype.card I : ℝ) := by
   …

6. theorem OAI.Problem337.FejerSampleMean.raw_packet_mean_upper line 130

   Source documentation

   The upper sampled mean, paired with the preceding lower estimate.

   theorem raw_packet_mean_upper {q h : ℕ} [NeZero q] {I : Type*}
       [Fintype I] [Nonempty I] (hh : 0 < h)
       (x : I → ZMod q) (y : ZMod q) (ε : ℝ)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l < h →
         ‖∑ t : I, ZMod.stdAddChar ((l : ZMod q) * x t)‖ ≤
           (Fintype.card I : ℝ) * ε) :
       (∑ t : I, ‖∑ j : Fin h,
         ZMod.stdAddChar ((j.val : ZMod q) * (x t - y))‖ ^ 2 / (h : ℝ)) /
         (Fintype.card I : ℝ) ≤ 1 + ((h : ℝ) - 1) * ε := by
   …

7. theorem OAI.Problem337.FejerSampleMean.packet_eq_kernel line 155
8. theorem OAI.Problem337.FejerSampleMean.fejer_sample_mean_lower line 164

   Source documentation

   Low-frequency cancellation implies the expected lower mass at every center of the named Fejér kernel.

   theorem fejer_sample_mean_lower {q h : ℕ} [NeZero q] {I : Type*}
       [Fintype I] [Nonempty I] (hh : 0 < h)
       (x : I → ZMod q) (y : ZMod q) (ε : ℝ)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l < h →
         ‖∑ t : I, ZMod.stdAddChar ((l : ZMod q) * x t)‖ ≤
           (Fintype.card I : ℝ) * ε) :
       1 - ((h : ℝ) - 1) * ε ≤
         (∑ t : I, GeometricKernel.kernel h (ZMod.stdAddChar (x t - y))) /
           (Fintype.card I : ℝ) := by
   …

   Mentions: OAI.Problem337.GeometricKernel.kernel

9. theorem OAI.Problem337.FejerSampleMean.fejer_sample_mean_error line 176

   Source documentation

   Two-sided sampled mean estimate for the named kernel.

   theorem fejer_sample_mean_error {q h : ℕ} [NeZero q] {I : Type*}
       [Fintype I] [Nonempty I] (hh : 0 < h)
       (x : I → ZMod q) (y : ZMod q) (ε : ℝ)
       (hfourier : ∀ l : ℕ, 1 ≤ l → l < h →
         ‖∑ t : I, ZMod.stdAddChar ((l : ZMod q) * x t)‖ ≤
           (Fintype.card I : ℝ) * ε) :
       |(∑ t : I, GeometricKernel.kernel h (ZMod.stdAddChar (x t - y))) /
           (Fintype.card I : ℝ) - 1| ≤ ((h : ℝ) - 1) * ε := by
   …

   Mentions: OAI.Problem337.GeometricKernel.kernel

10. theorem OAI.Problem337.FejerSampleMean.fejer_sample_mean_error_of_normalized line 190

    Source documentation

    Equivalent input convention phrased as normalized Fourier averages.

    theorem fejer_sample_mean_error_of_normalized {q h : ℕ} [NeZero q] {I : Type*}
        [Fintype I] [Nonempty I] (hh : 0 < h)
        (x : I → ZMod q) (y : ZMod q) (ε : ℝ)
        (hfourier : ∀ l : ℕ, 1 ≤ l → l < h →
          ‖(∑ t : I, ZMod.stdAddChar ((l : ZMod q) * x t)) /
            (Fintype.card I : ℂ)‖ ≤ ε) :
        |(∑ t : I, GeometricKernel.kernel h (ZMod.stdAddChar (x t - y))) /
            (Fintype.card I : ℝ) - 1| ≤ ((h : ℝ) - 1) * ε := by
    …

    Mentions: OAI.Problem337.GeometricKernel.kernel