OAI/NumberTheory/TwoPoint/Bounds/IntegerEdges.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TwoPointCorrelations.centeredTuple line 12
2. lemma OAI.TwoPointCorrelations.centeredTuple_add line 15
3. lemma OAI.TwoPointCorrelations.centeredTuple_abs line 22
4. def OAI.TwoPointCorrelations.paddingDensity line 27
5. def OAI.TwoPointCorrelations.integerEdgeKeep line 32
6. def OAI.TwoPointCorrelations.directedIntegerEdge line 38

   Source documentation

   The increasing-edge coefficient, including the two endpoint cutoffs. The auxiliary extra predicate carries the remaining vertex deletions.

   noncomputable def directedIntegerEdge (Q : Finset ℕ) (u : ℕ → ℝ)
       (eligible : ℕ → Prop) (g center : ℤ → ℝ) (L K : ℝ)
       (extra : ℤ → Prop) (h d q : ℕ) (n m : ℤ) : ℝ := by
   …

7. def OAI.TwoPointCorrelations.integerEdgeMatrix line 47
8. lemma OAI.TwoPointCorrelations.integerEdgeMatrix_symmetric line 54
9. lemma OAI.TwoPointCorrelations.sum_indicator_site_le line 62
10. lemma OAI.TwoPointCorrelations.padding_dvd_along_edge line 79

    Source documentation

    Divisibility by a padding divisor is unchanged along its integer edge.

    lemma padding_dvd_along_edge (h q d : ℕ) (n m : ℤ)
        (hm : m = n + (h * q * d : ℕ)) : (q : ℤ) ∣ m ↔ (q : ℤ) ∣ n := by
    …

11. def OAI.TwoPointCorrelations.retainedPaddingAtom line 86
12. lemma OAI.TwoPointCorrelations.retainedPaddingAtom_nonneg line 93
13. lemma OAI.TwoPointCorrelations.retainedPaddingAtom_sum_le line 102
14. lemma OAI.TwoPointCorrelations.centeredTuple_padding_periodic line 124
15. lemma OAI.TwoPointCorrelations.centeredTuple_abs_le_one line 131