BulkDistinctnessRemoval.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Removing bulk-prime collisions under the original independent priors

theorem OAI.Ostmann.productPrior_pair_collision_le line 13

theorem OAI.Ostmann.productPrior_noninjective_le line 36

Source documentation

Ordered pairs suffice; the harmless square count avoids selecting an ordering of the actual bulk positions.

theorem productPrior_noninjective_le {A : Type*} [Fintype A] {n : ℕ}
    (μ : Fin n → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
    (hmass : ∀ i, ∑ a, μ i a = 1) (α : ℝ) (hα : 0 ≤ α)
    (hmax : ∀ i a, μ i a ≤ α) :
    (∑ x : Fin n → A, productPrior μ x * if Function.Injective x then (0 : ℝ) else 1) ≤
      (n : ℝ) ^ 2 * α := by
…

Mentions: OAI.Ostmann.productPrior

theorem OAI.Ostmann.bulk_distinctness_removal line 76

Source documentation

Removing the distinctness gate costs its original collision probability, even when the complex integrand includes all the retained arithmetic factors.

theorem bulk_distinctness_removal {A : Type*} [Fintype A] {n : ℕ}
    (μ : Fin n → A → ℝ) (hμ : ∀ i a, 0 ≤ μ i a)
    (hmass : ∀ i, ∑ a, μ i a = 1) (α : ℝ) (hα : 0 ≤ α)
    (hmax : ∀ i a, μ i a ≤ α) (F : (Fin n → A) → ℂ)
    (B : ℝ) (hB : 0 ≤ B) (hF : ∀ x, ‖F x‖ ≤ B) :
    ‖(∑ x : Fin n → A, (productPrior μ x : ℂ) *
        (if Function.Injective x then F x else 0)) -
      ∑ x : Fin n → A, (productPrior μ x : ℂ) * F x‖ ≤ B * (n : ℝ) ^ 2 * α := by
…

Mentions: OAI.Ostmann.productPrior

theorem OAI.Ostmann.original_bulk_distinctness_removal line 105

Source documentation

The collision estimate for the literal bulk harmonic cells. The ambient prime set may also contain all nonbulk roles; the lower endpoint is needed only on the support of each bulk prior.

theorem original_bulk_distinctness_removal {n : ℕ}
    (P : Finset ℕ) (Q : Fin n → Finset ℕ) (hQP : ∀ i, Q i ⊆ P)
    (hQ : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹) ≠ 0)
    (H T : ℝ) (hmass : ∀ i, (∑ p ∈ Q i, (p : ℝ)⁻¹)⁻¹ ≤ Real.exp H)
    (hlow : ∀ i p, p ∈ Q i → Real.exp T ≤ (p : ℝ))
    (F : (Fin n → P) → ℂ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ x, ‖F x‖ ≤ B) :
    ‖(∑ x : Fin n → P, (productPrior (fun i => primeSubsetPrior P (Q i)) x : ℂ) *
        (if Function.Injective x then F x else 0)) -
      ∑ x : Fin n → P, (productPrior (fun i => primeSubsetPrior P (Q i)) x : ℂ) * F x‖ ≤
      B * (n : ℝ) ^ 2 * Real.exp (H - T) := by
…

Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.primeSubsetPrior