PaddingPrimeOscillation.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The fixed-modulus prime input implies the padding oscillation and the reciprocal-scale small-ball bound for the actual independent padding law.

lemma OAI.TwoPointCorrelations.oscillatory_log_substitution line 15
lemma OAI.TwoPointCorrelations.modFivePrimeBand_oscillation line 46
lemma OAI.TwoPointCorrelations.padding_band_subset line 62
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.padding_oscillation line 71
lemma OAI.TwoPointCorrelations.paddingPrimeSupply_prime line 96
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.padding_small_ball line 102
Source documentation
The precise padding difference law has O_E(1/L) mass in every unit interval centered at zero. Its bound is uniform in all centered tuples.
```
theorem ModFiveThetaInput.padding_small_ball (hP : ModFiveThetaInput) (E : Finset ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ L : ℝ, 1 ≤ L →
      (paddingDifferenceLaw (paddingPrimeSupply E L)
        (fun _ hp => (paddingPrimeSupply_prime hp).two_le)).probability
          (fun x => |paddingDifferenceValue (paddingPrimeSupply E L) x| ≤ 1) ≤ C / L := by
…
```
Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.paddingDifferenceLaw, OAI.TwoPointCorrelations.paddingPrimeSupply, OAI.TwoPointCorrelations.paddingPrimeSupply_prime, OAI.TwoPointCorrelations.paddingDifferenceValue