SampledResidueDenominator.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.RandomProducts.residueWordEquiv line 12
Source documentation
Reindex Boolean product words by the two-element finite type used in the auxiliary-denominator construction. No product values are identified.
```
def residueWordEquiv (m : ℕ) : (Fin m → Fin 2) ≃ (Fin m → Bool) :=
…
```
def OAI.Problem337.RandomProducts.residueSamplePairs line 16
Source documentation
The same labelled samples, in the paired-block interface.
```
def residueSamplePairs {m : ℕ} {P : Finset ℕ}
    (f : (Fin m × Bool) → P) : Fin m → Fin 2 → ℕ :=
…
```
theorem OAI.Problem337.RandomProducts.pairedEntry_residueSamplePairs line 20
theorem OAI.Problem337.RandomProducts.sampledProduct_residueWordEquiv_symm line 26
theorem OAI.Problem337.RandomProducts.expect_pairedEntry_eq_sampledProduct line 34
Source documentation
Reindexing preserves every normalized product statistic, including the complex Fourier averages used by the common-realization theorem.
```
theorem expect_pairedEntry_eq_sampledProduct {m : ℕ} {P : Finset ℕ}
    (f : (Fin m × Bool) → P) {A : Type*} [AddCommMonoid A] [Module ℚ≥0 A]
    (g : ℕ → A) :
    (𝔼 I : Fin m → Fin 2, g (ResidueConstruction.pairedEntry (residueSamplePairs f) I)) =
      𝔼 I : Fin m → Bool, g (sampledProduct f I) := by
…
```
Mentions: OAI.Problem337.ResidueConstruction.pairedEntry, OAI.Problem337.RandomProducts.residueSamplePairs, OAI.Problem337.RandomProducts.sampledProduct
theorem OAI.Problem337.RandomProducts.card_pairedEntry_eq_sampledProduct line 45
Source documentation
Exact preservation of filtered list cardinalities retains multiplicities when separate words happen to have equal product values.
```
theorem card_pairedEntry_eq_sampledProduct {m : ℕ} {P : Finset ℕ}
    (f : (Fin m × Bool) → P) (R : ℕ → Prop) [DecidablePred R] :
    (Finset.univ.filter (fun I : Fin m → Fin 2 =>
      R (ResidueConstruction.pairedEntry (residueSamplePairs f) I))).card =
    (Finset.univ.filter (fun I : Fin m → Bool => R (sampledProduct f I))).card := by
…
```
Mentions: OAI.Problem337.ResidueConstruction.pairedEntry, OAI.Problem337.RandomProducts.residueSamplePairs, OAI.Problem337.RandomProducts.sampledProduct

theorem OAI.Problem337.RandomProducts.construct_sampled_residue_denominator line 65

Source documentation

A single denominator simultaneously contains the deterministic subset products and the original Boolean-indexed sampled products. The conclusion is valid for every realization of the prime samples; no probabilistic independence or Fourier hypothesis is needed for this arithmetic construction.

theorem construct_sampled_residue_denominator {m : ℕ} {P : Finset ℕ}
    (p : Fin m → ℕ) (f : Fin 1000 → ((Fin m × Bool) → P)) {S : ℝ}
    (hS : 1 ≤ S) (hlog : 1 ≤ Real.log S) (hlarge : 100 * Real.log S ≤ S)
    (hmLower : S - Real.log S ≤ (m : ℝ) * Real.log S)
    (hmUpper : (m : ℝ) * Real.log S ≤ S)
    (hp : ∀ j, S ^ 100 ≤ (p j : ℝ) ∧ (p j : ℝ) ≤ S ^ 101)
    (hP : ∀ q ∈ P, S ^ 100 ≤ (q : ℝ) ∧ (q : ℝ) ≤ S ^ 101) :
    ∃ M : ℕ, Real.exp S < (M : ℝ) ∧ (M : ℝ) ≤ Real.exp (204204 * S) ∧
      2 ^ ⌈100000 * Real.log S / Real.log 2⌉₊ ∣ M ∧
      (∀ I : Fin m → Fin 2, ResidueConstruction.subsetEntry p I ∣ M ∧
        1 ≤ ResidueConstruction.subsetEntry p I ∧
        (ResidueConstruction.subsetEntry p I : ℝ) ≤ Real.exp (101 * S)) ∧
…

Mentions: OAI.Problem337.ResidueConstruction.subsetEntry

def OAI.Problem337.RandomProducts.residueSubsetProduct line 113
Source documentation
The deterministic subset list on the same Boolean-word index type as the sampled lists. This changes indices only, never the list entries or multiplicities.
```
def residueSubsetProduct {m : ℕ} (p : Fin m → ℕ) (I : Fin m → Bool) : ℕ :=
…
```
theorem OAI.Problem337.RandomProducts.residueSubsetProduct_eq_prod line 117
Source documentation
The reindexed deterministic list has the usual subset-product formula.
```
theorem residueSubsetProduct_eq_prod {m : ℕ} (p : Fin m → ℕ) (I : Fin m → Bool) :
    residueSubsetProduct p I = ∏ j, if I j then p j else 1 := by
…
```
Mentions: OAI.Problem337.RandomProducts.residueSubsetProduct
theorem OAI.Problem337.RandomProducts.residueSubsetProduct_injective line 126
Source documentation
The deterministic Boolean-indexed list remains injective for distinct primes.
```
theorem residueSubsetProduct_injective {m : ℕ} (p : Fin m → ℕ)
    (hp : ∀ j, (p j).Prime) (hinj : Function.Injective p) :
    Function.Injective (residueSubsetProduct p) := by
…
```
Mentions: OAI.Problem337.RandomProducts.residueSubsetProduct

theorem OAI.Problem337.RandomProducts.expect_residueSubsetProduct line 133

Source documentation

Any normalized statistic of the deterministic list is unchanged by reindexing.

theorem expect_residueSubsetProduct {m : ℕ} (p : Fin m → ℕ)
    {A : Type*} [AddCommMonoid A] [Module ℚ≥0 A] (g : ℕ → A) :
    (𝔼 I : Fin m → Bool, g (residueSubsetProduct p I)) =
      𝔼 I : Fin m → Fin 2, g (ResidueConstruction.subsetEntry p I) := by
…

Mentions: OAI.Problem337.RandomProducts.residueSubsetProduct, OAI.Problem337.ResidueConstruction.subsetEntry

theorem OAI.Problem337.RandomProducts.construct_sampled_residue_denominator_common_index line 143

Source documentation

The denominator construction with the single common Boolean-word index used by both high-level deterministic and lower-level sampled residue estimates.

theorem construct_sampled_residue_denominator_common_index {m : ℕ} {P : Finset ℕ}
    (p : Fin m → ℕ) (f : Fin 1000 → ((Fin m × Bool) → P)) {S : ℝ}
    (hS : 1 ≤ S) (hlog : 1 ≤ Real.log S) (hlarge : 100 * Real.log S ≤ S)
    (hmLower : S - Real.log S ≤ (m : ℝ) * Real.log S)
    (hmUpper : (m : ℝ) * Real.log S ≤ S)
    (hp : ∀ j, S ^ 100 ≤ (p j : ℝ) ∧ (p j : ℝ) ≤ S ^ 101)
    (hP : ∀ q ∈ P, S ^ 100 ≤ (q : ℝ) ∧ (q : ℝ) ≤ S ^ 101) :
    ∃ M : ℕ, Real.exp S < (M : ℝ) ∧ (M : ℝ) ≤ Real.exp (204204 * S) ∧
      2 ^ ⌈100000 * Real.log S / Real.log 2⌉₊ ∣ M ∧
      (∀ I : Fin m → Bool, residueSubsetProduct p I ∣ M ∧
        1 ≤ residueSubsetProduct p I ∧
        (residueSubsetProduct p I : ℝ) ≤ Real.exp (101 * S)) ∧
…

Mentions: OAI.Problem337.RandomProducts.residueSubsetProduct