VanDerCorput.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.norm_sum_sq_le_card_mul_sum_norm_sq line 10

Source documentation

Cauchy--Schwarz for the norm of a finite complex sum.

theorem norm_sum_sq_le_card_mul_sum_norm_sq {α : Type*}
    (U : Finset α) (f : α → ℂ) :
    ‖∑ u ∈ U, f u‖ ^ 2 ≤ (U.card : ℝ) * ∑ u ∈ U, ‖f u‖ ^ 2 := by
…

theorem OAI.Problem337.averaged_columns_correlation_bound line 20

Source documentation

Averaging equal column sums and bounding their pairwise correlations. This is the finite algebraic core of van der Corput differencing.

theorem averaged_columns_correlation_bound {α β : Type*}
    (U : Finset α) (T : Finset β) (z : α → β → ℂ)
    (S : ℂ) (D E : ℝ)
    (hcol : ∀ t ∈ T, ∑ u ∈ U, z u t = S)
    (hdiag : ∀ t ∈ T, ∑ u ∈ U, ‖z u t‖ ^ 2 ≤ D)
    (hcorr : ∀ t ∈ T, ∀ s ∈ T, t ≠ s →
      ‖∑ u ∈ U, z u t * conj (z u s)‖ ≤ E) :
    (T.card : ℝ) ^ 2 * ‖S‖ ^ 2 ≤
      (U.card : ℝ) * ((T.card : ℝ) * D +
        (T.card : ℝ) * (T.card - 1 : ℝ) * E) := by
…

Mentions: OAI.Problem337.D

theorem OAI.Problem337.sum_shift_supported line 65

Source documentation

Translation does not change a finite sum once the summation interval contains all translated points in its support.

theorem sum_shift_supported {M : Type*} [AddCommMonoid M]
    (a : ℤ → M) (N H : ℕ) (t : ℤ) (ht0 : 0 ≤ t) (htH : t ≤ H)
    (hsupport : ∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0) :
    (∑ n ∈ Finset.Icc (1 - (H : ℤ)) N, a (n + t)) =
      ∑ n ∈ Finset.Icc (1 : ℤ) N, a n := by
…

theorem OAI.Problem337.van_der_corput_interval_exact line 87

Source documentation

A concrete finite-support shift bound, before using H ≤ N to simplify the two endpoint losses. Correlation assumptions are symmetric in the shift.

theorem van_der_corput_interval_exact
    (a : ℤ → ℂ) (N H : ℕ) (hH : 1 ≤ H) (E : ℝ) (hE : 0 ≤ E)
    (hsupport : ∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0)
    (hnorm : ∀ n : ℤ, ‖a n‖ ≤ 1)
    (hcorr : ∀ h : ℤ, -(H : ℤ) < h → h < H → h ≠ 0 →
      ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a (n + h) * conj (a n)‖ ≤ E) :
    ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a n‖ ^ 2 ≤
      ((N : ℝ) + H) * ((N : ℝ) / H + E) := by
…

theorem OAI.Problem337.interval_correlation_neg line 160

Source documentation

Opposite shifts give conjugate autocorrelations, with zero extension supplying the endpoint cancellation.

theorem interval_correlation_neg (a : ℤ → ℂ) (N : ℕ) (h : ℤ)
    (hsupport : ∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0) :
    (∑ n ∈ Finset.Icc (1 : ℤ) N, a (n + -h) * conj (a n)) =
      conj (∑ n ∈ Finset.Icc (1 : ℤ) N, a (n + h) * conj (a n)) := by
…

theorem OAI.Problem337.van_der_corput_interval line 186

Source documentation

The elementary van der Corput inequality for an interval-supported sequence, in the positive-shift form required for iterated differencing.

theorem van_der_corput_interval
    (a : ℤ → ℂ) (N H : ℕ) (hH : 1 ≤ H) (hHN : H ≤ N)
    (E : ℝ) (hE : 0 ≤ E)
    (hsupport : ∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0)
    (hnorm : ∀ n : ℤ, ‖a n‖ ≤ 1)
    (hcorr : ∀ h : ℤ, 0 < h → h < H →
      ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a (n + h) * conj (a n)‖ ≤ E) :
    ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a n‖ ^ 2 ≤
      2 * (N : ℝ)^2 / H + 2 * (N : ℝ) * E := by
…

theorem OAI.Problem337.van_der_corput_interval_normalized line 218

Source documentation

Normalized van der Corput differencing, with an explicit absolute constant.

theorem van_der_corput_interval_normalized
    (a : ℤ → ℂ) (N H : ℕ) (hH : 1 ≤ H) (hHN : H ≤ N)
    (E : ℝ) (hE : 0 ≤ E)
    (hsupport : ∀ n : ℤ, n ∉ Finset.Icc (1 : ℤ) N → a n = 0)
    (hnorm : ∀ n : ℤ, ‖a n‖ ≤ 1)
    (hcorr : ∀ h : ℤ, 0 < h → h < H →
      ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a (n + h) * conj (a n)‖ ≤ E) :
    ‖∑ n ∈ Finset.Icc (1 : ℤ) N, a n‖ ^ 2 / (N : ℝ)^2 ≤
      2 / (H : ℝ) + 2 * E / N := by
…