OAI/NumberTheory/TwoPoint/Bounds/FiniteAverages.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.uniformAverage line 12

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:12 (same declaration text).

2. lemma OAI.TwoPointCorrelations.uniformAverage_const line 15

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:15 (same declaration text).

3. lemma OAI.TwoPointCorrelations.uniformAverage_equiv line 18

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:18 (same declaration text).

4. lemma OAI.TwoPointCorrelations.uniformAverage_prod line 23

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:23 (same declaration text).

5. lemma OAI.TwoPointCorrelations.uniformAverage_restrict line 35

   Source documentation

   A uniform independent family restricted to selected coordinates remains uniform; coordinates outside the selection integrate out exactly.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:35 (same declaration text).

   lemma uniformAverage_restrict {ι : Type*} [Fintype ι] [DecidableEq ι]
       (β : ι → Type*) [∀ i, Fintype (β i)] [∀ i, Nonempty (β i)] (S : Finset ι)
       (f : (∀ i : S, β i) → ℝ) :
       uniformAverage (fun x : ∀ i, β i => f (fun i : S => x i)) = uniformAverage f := by
   …

   Mentions: OAI.TwoPointCorrelations.uniformAverage

6. lemma OAI.TwoPointCorrelations.abs_uniformAverage_le_one line 48

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:48 (same declaration text).

7. lemma OAI.TwoPointCorrelations.crtJointProbability_expectation line 62

   Source documentation

   Grouping an interval average by its actual CRT residue vector.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:62 (same declaration text).

   lemma crtJointProbability_expectation {ι : Type*} [Fintype ι] [DecidableEq ι]
       (s : ι → ℕ) [∀ i, NeZero (s i)]
       (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
       (A : ZMod (∏ i, s i)) (N : ℕ) (F : (∀ i, ZMod (s i)) → ℝ) :
       (∑ r, crtJointProbability s hcop A N r * F r) =
         uniformAverage (fun j : Fin N =>
           F (ZMod.prodEquivPi s hcop (A + (j.val : ZMod (∏ i, s i))))) := by
   …

   Mentions: OAI.TwoPointCorrelations.crtJointProbability, OAI.TwoPointCorrelations.uniformAverage

8. lemma OAI.TwoPointCorrelations.crtUniform_expectation line 78

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:78 (same declaration text).

9. theorem OAI.TwoPointCorrelations.crt_observable_difference line 88

   Source documentation

   Uniform translated interval averages of any bounded observable of the selected residue coordinates differ from the product law by at most D/N.

   Also declared: OAI/NumberTheory/TwoPointCorrelations/FiniteAverages.lean:88 (same declaration text).

   theorem crt_observable_difference {ι : Type*} [Fintype ι] [DecidableEq ι]
       (s : ι → ℕ) [∀ i, NeZero (s i)]
       (hcop : Pairwise (fun i j => (s i).Coprime (s j)))
       (A : ZMod (∏ i, s i)) (N : ℕ) (hN : 0 < N)
       (F : (∀ i, ZMod (s i)) → ℝ) (hF : ∀ r, |F r| ≤ 1) :
       |uniformAverage (fun j : Fin N =>
           F (ZMod.prodEquivPi s hcop (A + (j.val : ZMod (∏ i, s i))))) -
         uniformAverage F| ≤ (∏ i, s i : ℕ) / (N : ℝ) := by
   …

   Mentions: OAI.TwoPointCorrelations.uniformAverage