RandomCommonRealization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RandomProducts.sampledMean line 11
Source documentation
Total version of the normalized sampled character average.
```
def sampledMean {m : ℕ} {P : Finset ℕ}
    (p : (Fin m × Bool) → P) (u l : ℕ) : ℂ :=
…
```
theorem OAI.Problem337.RandomProducts.sampledMean_eq line 17

theorem OAI.Problem337.RandomProducts.sampledMean_second_moment_bound line 23

Source documentation

The complete random moment theorem in the total normalized-average interface.

theorem sampledMean_second_moment_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 : ℕ) (hu : 0 < 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, ‖sampledMean p u l‖ ^ 2) /
      Fintype.card ((Fin (blockLength S) × Bool) → P) ≤
        Real.exp (-min (blockLength S : ℝ) (Real.log (u : ℝ)) / 100) := by
…

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

theorem OAI.Problem337.RandomProducts.exists_common_sampled_realization line 41

Source documentation

Concrete labelled-prime-product realization. All remaining hypotheses are finite index bounds and explicit numeric ranges, not moment assumptions.

theorem exists_common_sampled_realization :
    ∃ N : ℕ, ∀ (S : ℝ) (P : Finset ℕ) (J : Type)
      (tests : Finset J) (level : J → Finset ℕ) (X : J → ℝ)
      (freq : Finset ℕ) (terminalFreq : ℕ → Finset ℕ) (terminal : Finset ℕ),
      3 ≤ S →
      (∀ p ∈ P, Nat.Prime p) →
      (∀ p ∈ P, S ^ 100 ≤ (p : ℝ) ∧ (p : ℝ) ≤ S ^ 101) →
      S ^ 99 ≤ (P.card : ℝ) →
      500000 ≤ (blockLength S : ℝ) →
      (tests.card : ℝ) ≤ (blockLength S : ℝ) →
      (∀ j ∈ tests, 0 < X j) →
      (∀ j ∈ tests, ((level j).card : ℝ) ≤ X j) →
…

Mentions: OAI.Problem337.RandomProducts.blockLength