OAI/NumberTheory/Ostmann/Construction/HalfPrimeFactorization.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.weighted_tuple_mean_cons line 10
2. def OAI.Ostmann.halfPrimeScalar line 29
3. theorem OAI.Ostmann.halfPrimeMean_cons_scalar line 35

   Source documentation

   At an endpoint all nongiant residue tests have values independent of the endpoint. Their original expectation is therefore one common scalar.

   theorem halfPrimeMean_cons_scalar {n : ℕ} (P : Finset ℕ)
       (μ₀ : P → ℝ) (μ : Fin n → P → ℝ)
       (F₀ : (q : P) → ZMod (q : ℕ) → ℂ)
       (F : Fin n → (q : P) → ZMod (q : ℕ) → ℂ)
       (w : (Fin n → P) → ℝ) (c : Fin n → P → ℝ) (a : ℤ)
       (hc : ∀ i q, F i q (a : ZMod (q : ℕ)) = (c i q : ℂ)) :
       halfPrimeMean P (Fin.cons μ₀ μ) (Fin.cons F₀ F)
         (fun y => (w (Fin.tail y) : ℂ)) a =
         (halfPrimeScalar P μ w c : ℂ) * ∑ q : P, (μ₀ q : ℂ) * F₀ q (a : ZMod (q : ℕ)) := by
   …

   Mentions: OAI.Ostmann.halfPrimeMean, OAI.Ostmann.halfPrimeScalar

4. theorem OAI.Ostmann.halfPrimeScalar_lower line 61

   Source documentation

   The balanced-event mass lower bound becomes the positive scalar used in every endpoint mean, with both cutoff weights kept in the expectation.

   theorem halfPrimeScalar_lower {n : ℕ} (P : Finset ℕ)
       (μ : Fin n → P → ℝ) (w : (Fin n → P) → ℝ) (c : Fin n → P → ℝ)
       (hμ : ∀ i p, 0 ≤ μ i p) (hw : ∀ x, 0 ≤ w x) (hc : ∀ i p, 0 ≤ c i p)
       (S : Finset (Fin n → P)) (β γ : ℝ) (hγ : 0 ≤ γ)
       (hmass : β ≤ ∑ x ∈ S, productPrior μ x * w x)
       (hgood : ∀ x ∈ S, ∀ i, γ ≤ c i (x i)) :
       β * γ ^ n ≤ halfPrimeScalar P μ w c := by
   …

   Mentions: OAI.Ostmann.productPrior, OAI.Ostmann.halfPrimeScalar