PrimeFamilyGraph.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The weighted-row lemma for concrete prime-family graph operators

This constructs the operators, rather than assuming a coordinate formula. Arbitrary prime residue offsets cover both models. The symmetric gate can include the progression test and any further edge deletions. The cutoff uses the explicitly defined padding density.

def OAI.TwoPointCorrelations.primeFamilyGraphOperator line 23
theorem OAI.TwoPointCorrelations.primeFamilyGraphOperator_selfAdjoint line 34

theorem OAI.TwoPointCorrelations.primeFamilyGraphOperator_norm_le line 48

Source documentation

The single-operator assertion of manuscript q:weighted-rows.

theorem primeFamilyGraphOperator_norm_le
    (value : (i : α) → P i → ℕ) (hprime : ∀ i p, (value i p).Prime)
    (offset : (i : α) → P i → ℤ) (site : ι → ℤ) (hinj : Function.Injective site)
    (Q : Finset ℕ) (u : ℕ → ℝ) (eligible : ℕ → ℕ → Prop)
    (g : ℤ → ℝ) (L K : ℝ) (extra : ℕ → ℤ → Prop) (h : ℕ)
    (gate : ℕ → ι → ι → Prop) (hgate : ∀ d i j, gate d i j ↔ gate d j i)
    (hL : 0 < L) (hK : 0 ≤ K) (hu : ∀ q ∈ Q, 0 ≤ u q) (hg : ∀ n, 0 < g n)
    (x : (i : α) → P i) :
    ‖primeFamilyGraphOperator value offset site Q u eligible g L K extra h gate x‖ ≤ 2 * K := by
…

Mentions: OAI.TwoPointCorrelations.primeFamilyGraphOperator

theorem OAI.TwoPointCorrelations.primeFamilyGraphOperator_square_sum line 74

Source documentation

The square-function assertion of manuscript q:weighted-rows, with its exact 4 K² (8W)^J constant and the degree projection's support condition.

theorem primeFamilyGraphOperator_square_sum
    (value : (i : α) → P i → ℕ) (hprime : ∀ i p, (value i p).Prime)
    (offset : (i : α) → P i → ℤ) (site : ι → ℤ) (hinj : Function.Injective site)
    (Q : Finset ℕ) (u : ℕ → ℝ) (eligible : ℕ → ℕ → Prop)
    (g : ℤ → ℝ) (L K W : ℝ) (extra : ℕ → ℤ → Prop) (h : ℕ)
    (gate : ℕ → ι → ι → Prop) (hgate : ∀ d i j, gate d i j ↔ gate d j i)
    (hL : 0 < L) (hK : 0 ≤ K) (hu : ∀ q ∈ Q, 0 ≤ u q) (hg : ∀ n, 0 < g n)
    (hV : ∀ i, ∑ p, (value i p : ℝ)⁻¹ ≤ 2 * W)
    (v : EuclideanSpace ℂ ι)
    (hdegree : ∀ k, v k ≠ 0 →
      (∑ i, ∑ p : P i, if (value i p : ℤ) ∣ offset i p + site k then (1 : ℝ) else 0) ≤
        6 * W * Fintype.card α) :
…