OAI/NumberTheory/EgyptianFractions/RandomProductParameters.lean
21 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Problem337.RandomProducts.freshLengthline 10Source documentation
The short fresh-product length, with the constants used in the random residue construction.
def freshLength (S V : ℝ) : ℕ := ⌊(3 / 4 : ℝ) * V / (100 * Real.log S)⌋₊
- def
OAI.Problem337.RandomProducts.blockLengthline 12 - theorem
OAI.Problem337.RandomProducts.freshLength_boundsline 14 - theorem
OAI.Problem337.RandomProducts.freshLength_eight_le_blockLengthline 33 - theorem
OAI.Problem337.RandomProducts.fresh_product_le_expline 56Source documentation
Every fresh product is shorter than the reduced modulus threshold.
theorem fresh_product_le_exp {S V : ℝ} (hS : 2 ≤ S) (hV : 100000 * Real.log S ≤ V) : (2 * S ^ 100) ^ freshLength S V ≤ Real.exp ((4 / 5 : ℝ) * V) := by … - theorem
OAI.Problem337.RandomProducts.fresh_factorial_atom_le_expline 74Source documentation
The factorial multiplicity bound implies the required small atom bound.
theorem fresh_factorial_atom_le_exp {S V : ℝ} (hS : 2 ≤ S) (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S) : ((freshLength S V).factorial : ℝ) / (S ^ 99) ^ freshLength S V ≤ Real.exp (-(7 / 10 : ℝ) * V) := by … - theorem
OAI.Problem337.RandomProducts.freshLength_posline 108Source documentation
The fresh tuple is nonempty throughout the construction's range.
theorem freshLength_pos {S V : ℝ} (hS : 1 < S) (hV : 100000 * Real.log S ≤ V) : 1 ≤ freshLength S V := by … - theorem
OAI.Problem337.RandomProducts.fresh_factorial_atom_of_cardline 121Source documentation
Atom estimate with the actual cardinality of the prime sampling set.
theorem fresh_factorial_atom_of_card {S V : ℝ} (P : ℕ) (hS : 2 ≤ S) (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S) (hP : S ^ 99 ≤ (P : ℝ)) : ((freshLength S V).factorial : ℝ) / (P : ℝ) ^ freshLength S V ≤ Real.exp (-(7 / 10 : ℝ) * V) := by … - theorem
OAI.Problem337.RandomProducts.fresh_samples_product_le_expline 135Source documentation
Product estimate for individual prime samples, ready for an injective reduction-modulo-modulus argument.
theorem fresh_samples_product_le_exp {S V : ℝ} (hS : 2 ≤ S) (hV : 100000 * Real.log S ≤ V) (p : Fin (freshLength S V) → ℕ) (hp : ∀ i, (p i : ℝ) ≤ 2 * S ^ 100) : ((∏ i, p i : ℕ) : ℝ) ≤ Real.exp ((4 / 5 : ℝ) * V) := by … - def
OAI.Problem337.RandomProducts.badGcdThresholdline 148Source documentation
Hit threshold used when the exposed gcd makes the reduced modulus small.
def badGcdThreshold (S V : ℝ) : ℕ := ⌈(2 / 25 : ℝ) * V / (101 * Real.log S)⌉₊
- theorem
OAI.Problem337.RandomProducts.bad_gcd_implies_many_hitsline 150 - theorem
OAI.Problem337.RandomProducts.hit_tail_parameter_boundline 172Source documentation
The elementary union-bound expression is exponentially small with the specific random-products parameters.
theorem hit_tail_parameter_bound {S V : ℝ} (hS : 1 < S) (hV : 0 ≤ V) (m H P k : ℕ) (hm : (m : ℝ) ≤ S) (hH : (H : ℝ) ≤ S) (hP : S ^ 99 ≤ (P : ℝ)) (hk : badGcdThreshold S V ≤ k) : ((m : ℝ) * (H : ℝ) / (P : ℝ)) ^ k ≤ Real.exp (-(1 / 20 : ℝ) * V) := by … - theorem
OAI.Problem337.RandomProducts.blockLength_le_selfline 199 - theorem
OAI.Problem337.RandomProducts.fresh_samples_product_lt_modulusline 211Source documentation
Small fresh products remain distinct after reduction modulo any good reduced modulus.
theorem fresh_samples_product_lt_modulus {S V : ℝ} (hS : 2 ≤ S) (hV : 100000 * Real.log S ≤ V) (q : ℕ) (hq : Real.exp ((9 / 10 : ℝ) * V) ≤ (q : ℝ)) (p : Fin (freshLength S V) → ℕ) (hp : ∀ i, (p i : ℝ) ≤ 2 * S ^ 100) : (∏ i, p i) < q := by … - theorem
OAI.Problem337.RandomProducts.bilinear_atom_parameter_boundline 228Source documentation
Numerical endgame of the bilinear Fourier estimate.
theorem bilinear_atom_parameter_bound {S V : ℝ} (P q : ℕ) (hS : 2 ≤ S) (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S) (hP : S ^ 99 ≤ (P : ℝ)) (hq : (q : ℝ) ≤ Real.exp V) : Real.sqrt (q : ℝ) * (((freshLength S V).factorial : ℝ) / (P : ℝ) ^ freshLength S V) ≤ Real.exp (-(1 / 5 : ℝ) * V) := by … - theorem
OAI.Problem337.RandomProducts.three_errors_le_final_scaleline 255Source documentation
Combines Hamming exceptions, bad gcd exposures, and good-exposure bilinear cancellation into the final second-moment scale.
theorem three_errors_le_final_scale {m V w : ℝ} (hwm : w ≤ m) (hwV : w ≤ V) (hw : 50 ≤ w) : Real.exp (-m / 16) + Real.exp (-V / 20) + Real.exp (-V / 5) ≤ Real.exp (-w / 100) := by … - theorem
OAI.Problem337.RandomProducts.fresh_samples_powerBound_le_expline 277Source documentation
A version independent of the constant in the prime sampling interval. In particular it applies to
[S^100,4*S^100]onceS≥4.theorem fresh_samples_powerBound_le_exp {S V : ℝ} (hS : 1 < S) (hV : 100000 * Real.log S ≤ V) (p : Fin (freshLength S V) → ℕ) (hp : ∀ i, (p i : ℝ) ≤ S ^ 101) : ((∏ i, p i : ℕ) : ℝ) ≤ Real.exp ((4 / 5 : ℝ) * V) := by … - theorem
OAI.Problem337.RandomProducts.fresh_samples_powerBound_lt_modulusline 298 - theorem
OAI.Problem337.RandomProducts.fresh_coordinates_fitline 315Source documentation
The Hamming-distance condition supplies two disjoint fresh blocks.
theorem fresh_coordinates_fit {S V : ℝ} (hS : 1 < S) (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S) (B : ℕ) (hB : blockLength S ≤ 4 * B) : 2 * freshLength S V ≤ B := by …Mentions: OAI.Problem337.RandomProducts.blockLength, OAI.Problem337.RandomProducts.freshLength
- theorem
OAI.Problem337.RandomProducts.blockLength_largeline 322 - theorem
OAI.Problem337.RandomProducts.random_errors_le_final_scaleline 332Source documentation
The range assumptions automatically make the final scale large enough for absorption of all three error terms.
theorem random_errors_le_final_scale {S V : ℝ} (hS : 2 ≤ S) (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S) : Real.exp (-(blockLength S : ℝ) / 16) + Real.exp (-V / 20) + Real.exp (-V / 5) ≤ Real.exp (-min (blockLength S : ℝ) V / 100) := by …