OAI/NumberTheory/TwoPointCorrelations/MRTBoundaryMean.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.mrtBoundarySet line 12

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBoundaryMean.lean:12 (same declaration text).

2. lemma OAI.TwoPointCorrelations.mrt_mem_boundary_iff line 15

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBoundaryMean.lean:15 (same declaration text).

3. lemma OAI.TwoPointCorrelations.mrt_boundary_strip_card line 24

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBoundaryMean.lean:24 (same declaration text).

4. theorem OAI.TwoPointCorrelations.mrt_boundary_card line 33

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBoundaryMean.lean:33 (same declaration text).

5. lemma OAI.TwoPointCorrelations.mrt_boundary_range line 46

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBoundaryMean.lean:46 (same declaration text).

6. theorem OAI.TwoPointCorrelations.mrt_boundary_mean_square line 63

   Source documentation

   Arbitrary bounded coefficients on the two bin-boundary strips have mean-square cost proportional to their multiplicative width.

   Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTBoundaryMean.lean:63 (same declaration text).

   theorem mrt_boundary_mean_square (b : ℕ → ℂ) {N : ℕ} (hN : 0 < N)
       {δ : ℝ} (hδ : 1 ≤ δ) (hδ2 : δ ≤ 2)
       (hb : ∀ n ∈ mrtBoundarySet N δ, ‖b n‖ ≤ 1)
       {T : ℝ} (hT : 0 < T) :
       (∫ t in -T..T, ‖mrtExponentialPolynomial (mrtBoundarySet N δ)
         (fun n => b n / (n : ℂ)) (fun n => -Real.log (n : ℝ)) t‖ ^ 2) ≤
         96 * Real.exp 1 * (T / (N : ℝ) + 1) * (δ - 1) := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtBoundarySet, OAI.TwoPointCorrelations.mrtExponentialPolynomial