SupportedInitialLogSum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Initial logarithmic cutoffs on the support of the original priors

theorem OAI.Ostmann.exists_supported_log_sum_center line 12

Source documentation

The score only needs to be bounded where its weight is nonzero. This allows all prime roles to share the same large ambient container.

theorem exists_supported_log_sum_center {A : Type*} [Fintype A]
    (weight score : A → ℝ) (N : ℕ) (β : ℝ)
    (hmass : β ≤ ∑ a, weight a)
    (hscore : ∀ a, weight a ≠ 0 → 0 ≤ score a ∧ score a ≤ N) :
    ∃ c ∈ Finset.Icc (0 : ℤ) N,
      β / (N + 1) ≤ ∑ a, weight a * logCellProfile (score a - c) := by
…

Mentions: OAI.Ostmann.logCellProfile

theorem OAI.Ostmann.exists_supported_balanced_log_sum_center line 33

theorem OAI.Ostmann.exists_supported_prime_log_sum_center line 56

Source documentation

The cutoff remains in the true bulk or spectator range although its prior is represented on a container that also contains the giant primes.

theorem exists_supported_prime_log_sum_center (P : Finset ℕ)
    (hP : ∀ p ∈ P, p.Prime) (n m : ℕ) (T : ℝ)
    (μ : Fin n → P → ℝ) (good : Fin n → P → Prop)
    (hm : 1 ≤ m) (hn : n ≤ m) (hT : T ≤ m)
    (hlog : ∀ i (p : P), μ i p ≠ 0 → Real.log (p : ℝ) ≤ Real.exp T)
    (hmass : ∀ i, (1 / 2 : ℝ) ≤ ∑ p, if good i p then μ i p else 0) :
    ∃ c ∈ Finset.Icc (0 : ℤ) ⌈(n : ℝ) * Real.exp T⌉₊,
      Real.exp (-(Real.log 2 + 2) * m) ≤
        ∑ x ∈ balancedTupleSet n good, productPrior μ x *
          logCellProfile ((∑ i, Real.log (x i : ℝ)) - c) := by
…

Mentions: OAI.Ostmann.balancedTupleSet, OAI.Ostmann.productPrior, OAI.Ostmann.logCellProfile