OAI/NumberTheory/TwoPoint/Bounds/PrimeSupplyGeometry.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Actual disjoint prime supplies at geometric logarithmic scales. Their mass follows from the published fixed-modulus input through the proved partial-summation chain, and all support assertions are finite identities.

  1. def OAI.TwoPointCorrelations.primeSupplyEndpoint line 14
  2. def OAI.TwoPointCorrelations.centeredPrimeSupply line 17
  3. def OAI.TwoPointCorrelations.paddingPrimeSupply line 21
  4. lemma OAI.TwoPointCorrelations.primeSupplyEndpoint_zero line 24
  5. lemma OAI.TwoPointCorrelations.primeSupplyEndpoint_succ line 27
  6. lemma OAI.TwoPointCorrelations.primeSupplyEndpoint_mono line 33
  7. lemma OAI.TwoPointCorrelations.centeredPrimeSupply_mem line 41
  8. lemma OAI.TwoPointCorrelations.centeredPrimeSupply_pairwise_disjoint line 53
  9. lemma OAI.TwoPointCorrelations.centered_padding_disjoint line 67
  10. lemma OAI.TwoPointCorrelations.centeredPrimeSupply_global_bounds line 75
  11. lemma OAI.TwoPointCorrelations.primeSupplyEndpoint_sum_lt line 91
  12. lemma OAI.TwoPointCorrelations.centeredPrimeSupply_tuple_log_bound line 105
  13. theorem OAI.TwoPointCorrelations.ModFiveThetaInput.centered_supplies line 124

    Source documentation

    Every centered supply is nonempty and has the required reciprocal mass. The threshold is independent of the number of supplies and their indices.

    theorem ModFiveThetaInput.centered_supplies (hP : ModFiveThetaInput)
    (E : Finset ℕ) (W : ℝ) (hW : 0 < W) :
    ∃ A₀ : ℝ, 1 ≤ A₀ ∧ ∀ A : ℝ, A₀ ≤ A → ∀ i : ℕ,
      (centeredPrimeSupply E A W i).Nonempty ∧
      W ≤ (∑ p ∈ centeredPrimeSupply E A W i, 1 / (p : ℝ)) ∧
      (∑ p ∈ centeredPrimeSupply E A W i, 1 / (p : ℝ)) ≤ 2 * W := by
…

    Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.centeredPrimeSupply