OAI/NumberTheory/EgyptianFractions/RandomSecondMoment.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.RandomProducts.sampledProduct line 14
2. def OAI.Problem337.RandomProducts.sampledPhase line 18
3. theorem OAI.Problem337.RandomProducts.norm_sampledPhase line 22
4. theorem OAI.Problem337.RandomProducts.sampledPhase_correlation line 26
5. theorem OAI.Problem337.RandomProducts.sampledProduct_split_first line 37
6. theorem OAI.Problem337.RandomProducts.sampledProduct_split_other line 64
7. theorem OAI.Problem337.RandomProducts.sampled_pair_bound_of_good_bad line 77

   Source documentation

   The exact sample-splitting interface for one pair of Boolean words.

   theorem sampled_pair_bound_of_good_bad {m : ℕ} {P : Finset ℕ}
       (hne : P.Nonempty) (I J : Fin m → Bool) (A B : Finset (Fin m))
       (hAB : Disjoint A B) (hA : ∀ i ∈ A, I i ≠ J i) (hB : ∀ i ∈ B, I i ≠ J i)
       (u l : ℕ) [NeZero u] (bad : Finset (ExposedLabel I A B → P))
       (ε δ : ℝ) (hδ : 0 ≤ δ)
       (hbad : (bad.card : ℝ) / Fintype.card (ExposedLabel I A B → P) ≤ ε)
       (hgood : ∀ c, c ∉ bad →
         ‖𝔼 a : selectedLabels I A → P, 𝔼 b : selectedLabels I B → P,
           ZMod.stdAddChar
             (((l * exposedFirstProduct (fun p : P => (p : ℕ)) I A B c *
               (∏ z, (a z : ℕ)) * (∏ z, (b z : ℕ)) : ℕ) : ZMod u) -
               ((l * exposedOtherProduct (fun p : P => (p : ℕ)) I J A B hA hB c : ℕ) : ZMod u))‖ ≤ δ) :
   …

8. theorem OAI.Problem337.RandomProducts.sampled_product_second_moment_of_correlations line 106

   Source documentation

   The actual labelled-prime-product random quantity, reduced to separated-pair correlations. The remaining hypothesis is precisely the output of exposure.

   theorem sampled_product_second_moment_of_correlations {P : Finset ℕ}
       (hne : P.Nonempty) (m u l : ℕ) [NeZero u] (V : ℝ)
       (hlarge : 50 ≤ min (m : ℝ) V)
       (hpair : ∀ I J : Fin m → Bool,
         (m : ℝ) / 4 ≤ (hammingDist I J : ℝ) →
         ‖𝔼 p : (Fin m × Bool) → P,
           ZMod.stdAddChar (((l * sampledProduct p I : ℕ) : ZMod u) -
             ((l * sampledProduct p J : ℕ) : ZMod u))‖ ≤
           Real.exp (-V / 20) + Real.exp (-V / 5)) :
       (𝔼 p : (Fin m × Bool) → P, ‖𝔼 I : Fin m → Bool, sampledPhase u l p I‖ ^ 2) ≤
         Real.exp (-min (m : ℝ) V / 100) := by
   …

   Mentions: OAI.Problem337.RandomProducts.sampledProduct, OAI.Problem337.RandomProducts.sampledPhase

9. theorem OAI.Problem337.RandomProducts.sampled_pair_fresh_blocks line 124

   Source documentation

   The actual Hamming condition supplies the two fresh blocks used by exposure.

   theorem sampled_pair_fresh_blocks {S V : ℝ} (hS : 1 < S)
       (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S)
       (I J : Fin (blockLength S) → Bool)
       (hIJ : (blockLength S : ℝ) / 4 ≤ (hammingDist I J : ℝ)) :
       ∃ A B : Finset (Fin (blockLength S)), Disjoint A B ∧
         A.card = freshLength S V ∧ B.card = freshLength S V ∧
         (∀ i ∈ A, I i ≠ J i) ∧ (∀ i ∈ B, I i ≠ J i) := by
   …

   Mentions: OAI.Problem337.RandomProducts.blockLength, OAI.Problem337.RandomProducts.freshLength

10. theorem OAI.Problem337.RandomProducts.exposed_coordinate_card_le line 137

    Source documentation

    The exposed factor uses at most the full first word's number of coordinates.

    theorem exposed_coordinate_card_le {S : ℝ} (hS : Real.exp 1 ≤ S)
        (A B : Finset (Fin (blockLength S))) :
        (Fintype.card ↥(Finset.univ \ (A ∪ B)) : ℝ) ≤ S := by
    …

    Mentions: OAI.Problem337.RandomProducts.blockLength

11. theorem OAI.Problem337.RandomProducts.random_min_large line 148

    Source documentation

    The parameter range guarantees the fixed numeric threshold for error absorption.

    theorem random_min_large {S V : ℝ} (hS : 2 ≤ S)
        (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S) :
        50 ≤ min (blockLength S : ℝ) V := by
    …

    Mentions: OAI.Problem337.RandomProducts.blockLength

12. theorem OAI.Problem337.RandomProducts.exposed_bad_gcd_fraction line 162

    Source documentation

    The actual exposed first-word factor has an exponentially small bad-gcd event. Unused exposed labels are eliminated by the exact uniform-coordinate marginal law.

    theorem exposed_bad_gcd_fraction (S V : ℝ) (hS : 3 ≤ S)
        (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S)
        (P : Finset ℕ) (hP : P.Nonempty) (hprime : ∀ p ∈ P, Nat.Prime p)
        (hinterval : ∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101)
        (hsize : S ^ 99 ≤ (P.card : ℝ)) (u l : ℕ)
        (huexp : (u : ℝ) = Real.exp V) (hl : 0 < l)
        (hlbound : (l : ℝ) ≤ Real.exp (V / 200))
        (I : Fin (blockLength S) → Bool) (A B : Finset (Fin (blockLength S))) :
        ((Finset.univ.filter (fun c : ExposedLabel I A B → P =>
          ((u / Nat.gcd (l * exposedFirstProduct (fun p : P => (p : ℕ)) I A B c) u : ℕ) : ℝ)
            < Real.exp (9 * V / 10))).card : ℝ) /
          Fintype.card (ExposedLabel I A B → P) ≤ Real.exp (-V / 20) := by
    …

    Mentions: OAI.Problem337.RandomProducts.blockLength

13. theorem OAI.Problem337.RandomProducts.sampled_product_second_moment_bound line 194

    Source documentation

    The complete random-product second-moment estimate for labelled independent prime samples, including Hamming exceptions, bad gcds, and bilinear cancellation.

    theorem sampled_product_second_moment_bound
        (S V : ℝ) (hS : 3 ≤ S) (hV : 100000 * Real.log S ≤ V) (hVS : V ≤ S)
        (P : Finset ℕ) (hprime : ∀ p ∈ P, Nat.Prime p)
        (hinterval : ∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101)
        (hsize : S ^ 99 ≤ (P.card : ℝ)) (u l : ℕ) [NeZero u]
        (huexp : (u : ℝ) = Real.exp V) (hl : 0 < l)
        (hlbound : (l : ℝ) ≤ Real.exp (V / 200)) :
        (𝔼 p : (Fin (blockLength S) × Bool) → P,
          ‖𝔼 I : Fin (blockLength S) → Bool, sampledPhase u l p I‖ ^ 2) ≤
            Real.exp (-min (blockLength S : ℝ) V / 100) := by
    …

    Mentions: OAI.Problem337.RandomProducts.blockLength, OAI.Problem337.RandomProducts.sampledPhase

14. theorem OAI.Problem337.RandomProducts.sampled_product_second_moment_log_bound line 240

    Source documentation

    Logarithmic form with V = log u and the smaller common frequency range.

    theorem sampled_product_second_moment_log_bound
        (S : ℝ) (hS : 3 ≤ S) (P : Finset ℕ)
        (hprime : ∀ p ∈ P, Nat.Prime p)
        (hinterval : ∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101)
        (hsize : S ^ 99 ≤ (P.card : ℝ)) (u l : ℕ) [NeZero u]
        (hV : 100000 * Real.log S ≤ Real.log (u : ℝ))
        (hVS : Real.log (u : ℝ) ≤ S) (hl : 0 < l)
        (hlbound : (l : ℝ) ≤ Real.exp (min (blockLength S : ℝ) (Real.log (u : ℝ)) / 200)) :
        (𝔼 p : (Fin (blockLength S) × Bool) → P,
          ‖𝔼 I : Fin (blockLength S) → Bool, sampledPhase u l p I‖ ^ 2) ≤
            Real.exp (-min (blockLength S : ℝ) (Real.log (u : ℝ)) / 100) := by
    …

    Mentions: OAI.Problem337.RandomProducts.blockLength, OAI.Problem337.RandomProducts.sampledPhase