DisjointCoordinates.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Exact coordinate splitting for the high-rank lit equations.

def OAI.TwoPointCorrelations.outsideCoordinates line 14
def OAI.TwoPointCorrelations.splitAssignment line 19
Source documentation
Replace the two disjoint selected coordinate families, keeping all other coordinates fixed.
```
noncomputable def splitAssignment (control pivot : ρ → α) (base : α → ℤ)
    (c y : ρ → ℤ) : α → ℤ :=
…
```
lemma OAI.TwoPointCorrelations.splitAssignment_control line 24
lemma OAI.TwoPointCorrelations.splitAssignment_pivot line 30
lemma OAI.TwoPointCorrelations.splitAssignment_outside line 39
lemma OAI.TwoPointCorrelations.sum_disjoint_coordinates line 51

theorem OAI.TwoPointCorrelations.row_splitAssignment line 76

Source documentation

The complete integral row is exactly its minor part, its controlling part, and its fixed outside part.

theorem row_splitAssignment (w : ρ → α → ℤ) (control pivot : ρ → α)
    (hc : Function.Injective control) (hp : Function.Injective pivot)
    (hdisjoint : ∀ i j, pivot i ≠ control j) (base : α → ℤ) (c y : ρ → ℤ) (i : ρ) :
    (∑ z, w i z * splitAssignment control pivot base c y z) =
      ((fun i j => w i (pivot j)) *ᵥ y +
        (fun i j => w i (control j)) *ᵥ c +
        (fun i => ∑ z ∈ outsideCoordinates control pivot, w i z * base z)) i := by
…

Mentions: OAI.TwoPointCorrelations.splitAssignment, OAI.TwoPointCorrelations.outsideCoordinates

theorem OAI.TwoPointCorrelations.split_coordinate_prime_rank_bound line 94

Source documentation

After fixing the outside variables, the actual selected rows satisfy the previously proved random-prime rank bound.

theorem split_coordinate_prime_rank_bound
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime) (μ : FiniteLaw P)
    (w : ρ → α → ℤ) (control pivot : ρ → α)
    (hc : Function.Injective control) (hp : Function.Injective pivot)
    (hdisjoint : ∀ i j, pivot i ≠ control j)
    (hdet : (Matrix.of fun i j => w i (pivot j)).det ≠ 0)
    (base : α → ℤ) (M : ℕ) (a : ℝ) (ha : 0 ≤ a)
    (hatom : ∀ p, μ.weight p ≤ a)
    (hsize : ∀ y z : ρ → P, ∀ i,
      (primeDifference P (fun i j => w i (pivot j)) y z i).natAbs ≤ M) :
    let ν := FiniteLaw.independent (fun _ : ρ => μ)
…

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