OAI/NumberTheory/TwoPoint/Bounds/PatternResampling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Resample one prime per observed equality class, retaining arbitrary nonnegative events.

  1. def OAI.TwoPointCorrelations.patternClasses line 14
  2. def OAI.TwoPointCorrelations.patternCoordinate line 16
  3. def OAI.TwoPointCorrelations.patternRepresentative line 19
  4. lemma OAI.TwoPointCorrelations.patternRepresentative_value line 22
  5. def OAI.TwoPointCorrelations.patternEncode line 26
  6. def OAI.TwoPointCorrelations.patternResample line 29
  7. lemma OAI.TwoPointCorrelations.patternResample_encode line 32
  8. lemma OAI.TwoPointCorrelations.patternEncode_injOn line 38
  9. lemma OAI.TwoPointCorrelations.patternEncode_weight line 48
  10. theorem OAI.TwoPointCorrelations.same_pattern_resampled_sum line 70

    Source documentation

    Numerical restrictions and outside weights are preserved by the resampling map. They are not discarded before the high-rank estimate.

    theorem same_pattern_resampled_sum [Fintype P]
    (template : τ → P) (F : Finset (τ → P)) (a : P → ℝ) (ha : ∀ p, 0 ≤ a p)
    (potential : (τ → P) → ℝ) (hpotential : ∀ w, 0 ≤ potential w)
    (hpattern : ∀ w ∈ F, ∀ i j, w i = w j ↔ template i = template j) :
    (∑ w ∈ F, (∏ p ∈ univ.image w, a p) * potential w) ≤
      ∑ x : patternClasses template → P,
        (∏ c, a (x c)) * potential (patternResample template x) := by
…

    Mentions: OAI.TwoPointCorrelations.patternClasses, OAI.TwoPointCorrelations.patternResample