OAI/NumberTheory/Ostmann/Construction/PrimeTupleFiber.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.prime_tuple_prior_point_bound line 13

   Source documentation

   This applies simultaneously to the giant, broad-band, and deleted cell marginals: only their already proved reciprocal-prime atom bounds are used.

   theorem prime_tuple_prior_point_bound {n : ℕ} (P : Finset ℕ)
       (hP : ∀ p ∈ P, p.Prime) (μ : Fin n → P → ℝ) (C : Fin n → ℝ)
       (hμ : ∀ i p, 0 ≤ μ i p) (hbound : ∀ i (p : P), (p : ℝ) * μ i p ≤ C i)
       (x : Fin n → P) :
       productPrior μ x ≤ (∏ i, C i) * (∏ i, (x i : ℝ))⁻¹ := by
   …

   Mentions: OAI.Ostmann.productPrior

2. theorem OAI.Ostmann.prime_tuple_prior_product_mass line 24
3. theorem OAI.Ostmann.prime_tuple_prior_frequency_mass line 49

   Source documentation

   A fixed product and a fixed root frequency incur no factor equal to the number of frequencies. All original marginal probabilities are retained.

   theorem prime_tuple_prior_frequency_mass {n : ℕ} (P : Finset ℕ)
       (hP : ∀ p ∈ P, p.Prime) (μ : Fin n → P → ℝ) (C : Fin n → ℝ)
       (hμ : ∀ i p, 0 ≤ μ i p) (hC : ∀ i, 0 ≤ C i)
       (hbound : ∀ i (p : P), (p : ℝ) * μ i p ≤ C i) (V M : ℕ) (s : ℤ) :
       (∑ x : Fin n → P, ∑ v : transferFrequencyRange V,
         if Function.Injective x ∧ (∏ i, (x i : ℕ)) = M ∧ (v : ℤ) = s then
           productPrior μ x else 0) ≤
         (n.factorial : ℝ) * (∏ i, C i) * (M : ℝ)⁻¹ := by
   …

   Mentions: OAI.Ostmann.transferFrequencyRange, OAI.Ostmann.productPrior