OAI/NumberTheory/TwoPoint/Bounds/ResidueRestriction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Restriction of a product law to selected prime coordinates. The coordinate laws may depend on the prime; no common-modulus uniformity is assumed.

  1. lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_reindex line 17
  2. lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_restrict line 35
  3. lemma OAI.TwoPointCorrelations.FiniteLaw.independent_average_embedding line 45

    Source documentation

    Independent coordinates retain their individual laws under an injective change of the index set.

    lemma independent_average_embedding {ι κ A : Type*} [Fintype ι] [Fintype κ]
    [DecidableEq ι] [DecidableEq κ] [Fintype A]
    (e : κ → ι) (he : Function.Injective e) (μ : ι → FiniteLaw A)
    (f : (κ → A) → ℝ) :
    (independent μ).average (fun x => f (fun k => x (e k))) =
      (independent (fun k => μ (e k))).average f := by
…

    Mentions: OAI.TwoPointCorrelations.FiniteLaw, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.FiniteLaw.average

  4. def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.paddingCoordinate line 75
  5. def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.paddingRestriction line 78
  6. def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.paddingResidueLaw line 81
  7. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residue_average_padding line 87
  8. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.exists_padding_residue_origin line 98
  9. def OAI.TwoPointCorrelations.ProhibitedPrimeFamily.paddingResidueOrigin line 106
  10. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.paddingResidueOrigin_spec line 109
  11. lemma OAI.TwoPointCorrelations.ProhibitedPrimeFamily.residue_average_padding_shift line 115

    Source documentation

    Padding-periodic observables at the full CRT lift depend only on the independent padding coordinates, including after a fixed integer shift.

    lemma residue_average_padding_shift (hB : ∀ p ∈ data.P ∪ data.Q, p ≤ B)
    (site : ℤ) (f : ℤ → ℝ)
    (hf : ∀ n m : ℤ, (∀ q ∈ data.Q, (n : ZMod q) = (m : ZMod q)) → f n = f m) :
    (data.residueLaw B hB).average (fun x => f (data.residueOrigin x + site)) =
      (data.paddingResidueLaw B hB).average (fun x =>
        f (data.paddingResidueOrigin x + site)) := by
…