MRTSampling.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Sampling a differentiable function at separated points. Unit intervals give a finite Sobolev estimate, which will be applied to the prime-polynomial powers already expanded into Dirichlet coefficients.

lemma OAI.TwoPointCorrelations.mrt_value_le_unit_integral line 17
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSampling.lean:17 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_unit_intervals_disjoint line 52
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSampling.lean:52 (same declaration text).
lemma OAI.TwoPointCorrelations.mrt_sum_unit_integrals_le line 64
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSampling.lean:64 (same declaration text).

theorem OAI.TwoPointCorrelations.mrt_separated_square_samples line 85

Source documentation

A finite separated sample is controlled by the ordinary square integrals of a function and its derivative.

Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSampling.lean:85 (same declaration text).

theorem mrt_separated_square_samples (S : Finset ℝ) (q q' : ℝ → ℂ)
    (hq : Continuous q) (hq' : Continuous q')
    (hd : ∀ t, HasDerivAt q (q' t) t)
    (hsep : ∀ x ∈ S, ∀ y ∈ S, x ≠ y → 1 ≤ |x - y|)
    (a b : ℝ) (hab : a ≤ b) (hS : ∀ x ∈ S, a ≤ x ∧ x + 1 ≤ b) :
    (∑ x ∈ S, ‖q x‖ ^ 2) ≤ ∫ t in a..b, 2 * ‖q t‖ ^ 2 + ‖q' t‖ ^ 2 := by
…

lemma OAI.TwoPointCorrelations.mrt_exponential_polynomial_deriv line 116
Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTSampling.lean:116 (same declaration text).