OAI/NumberTheory/TwoPoint/Bounds/LitConsistency.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Compress all lit tests for one prime into one forced residue, or zero.

  1. def OAI.TwoPointCorrelations.LitConsistent line 14
  2. def OAI.TwoPointCorrelations.litForcedTarget line 17
  3. lemma OAI.TwoPointCorrelations.litForcedTarget_at line 23
  4. lemma OAI.TwoPointCorrelations.lit_indicator_product line 32

    Source documentation

    Repetitions of the same lit residue test contribute just one indicator.

    lemma lit_indicator_product (L : Finset τ) (label : τ → ι) (target : τ → A)
    (base : ι → A) (hL : LitConsistent L label target) (x : ι → A) :
    (∏ t ∈ L, if x (label t) = target t then (1 : ℝ) else 0) =
      ∏ i ∈ L.image label, if x i = litForcedTarget L label target base i then (1 : ℝ) else 0 := by
…

    Mentions: OAI.TwoPointCorrelations.LitConsistent, OAI.TwoPointCorrelations.litForcedTarget

  5. lemma OAI.TwoPointCorrelations.lit_indicator_product_eq_zero line 51

    Source documentation

    Incompatible lit offsets give exactly zero before any estimate.

    lemma lit_indicator_product_eq_zero (L : Finset τ) (label : τ → ι) (target : τ → A)
    (hL : ¬LitConsistent L label target) (x : ι → A) :
    (∏ t ∈ L, if x (label t) = target t then (1 : ℝ) else 0) = 0 := by
…

    Mentions: OAI.TwoPointCorrelations.LitConsistent