ActualPaddingResidues.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The proved padding laws applied to the graph's actual integer normalization and bin density at any common lift of the prime residues.

lemma OAI.TwoPointCorrelations.actualPaddingAvailability_lift line 15
lemma OAI.TwoPointCorrelations.actualPaddingWeight_lift line 25
lemma OAI.TwoPointCorrelations.actualPaddingDegree_lift line 31
lemma OAI.TwoPointCorrelations.actualPaddingBin_lift line 39

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.actual_padding_residue_bin_square line 50

Source documentation

The literal graph density, including an arbitrary restriction on the padding-divisor set, has the same squared-bin bound at any residue lift.

theorem ModFiveThetaInput.actual_padding_residue_bin_square (hP : ModFiveThetaInput)
    (E : Finset ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (L η c : ℝ) (B : ℕ) (site : ℤ) (bins : Finset ℤ),
      1 ≤ L → 0 < η → η ≤ 1 →
      ∀ (hQB : ∀ p ∈ paddingPrimeSupply E L, p ≤ B)
        (D : Finset ℕ), D ⊆ retainedPrimeDivisors (paddingPrimeSupply E L) →
      ∀ N : (paddingPrimeSupply E L → Fin B) → ℤ,
      (∀ z (p : paddingPrimeSupply E L),
        (N z : ZMod p.val) = ((z p).val : ZMod p.val) + (site : ZMod p.val)) →
      (FiniteLaw.independent (fun p : paddingPrimeSupply E L =>
        uniformResidueLaw B p.val (paddingPrimeSupply_prime p.property).pos
          (hQB p p.property))).average (fun z =>
…

Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.paddingPrimeSupply, OAI.TwoPointCorrelations.retainedPrimeDivisors, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.paddingPrimeSupply_prime

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_padding_degree_tail line 91

Source documentation

Deleting vertices with more than 400 log L padding primes has the proved weighted probability cost for the literal graph normalization.

theorem ModFiveThetaInput.eventually_actual_padding_degree_tail (hP : ModFiveThetaInput)
    (E : Finset ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (B : ℕ) (site : ℤ)
      (hQB : ∀ p ∈ paddingPrimeSupply E L, p ≤ B)
      (N : (paddingPrimeSupply E L → Fin B) → ℤ),
      (∀ z (p : paddingPrimeSupply E L),
        (N z : ZMod p.val) = ((z p).val : ZMod p.val) + (site : ZMod p.val)) →
      (FiniteLaw.independent (fun p : paddingPrimeSupply E L =>
        uniformResidueLaw B p.val (paddingPrimeSupply_prime p.property).pos
          (hQB p p.property))).average (fun z =>
            (actualPaddingVertex (paddingPrimeSupply E L) (N z)) ^ 2 *
              if ¬actualPaddingDegreeCut (paddingPrimeSupply E L) L (N z) then 1 else 0) /
…

Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.paddingPrimeSupply, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.uniformResidueLaw, OAI.TwoPointCorrelations.paddingPrimeSupply_prime, OAI.TwoPointCorrelations.actualPaddingVertex, OAI.TwoPointCorrelations.actualPaddingDegreeCut